thus SCM+FSA is homogeneous :: thesis: ( SCM+FSA is with_explicit_jumps & SCM+FSA is without_implicit_jumps )

proof

let I, J be Instruction of SCM+FSA ; :: according to AMISTD_2:def 4 :: thesis: ( not InsCode I = InsCode J or dom (AddressPart I) = dom (AddressPart J) )
assume A1: InsCode I = InsCode J ; :: thesis: dom (AddressPart I) = dom (AddressPart J)
A2: ( J = [0 ,{} ] or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

per cases ( I = [0 ,{} ] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo a,b or ex a, b being Int-Location st I = SubFrom a,b or ex a, b being Int-Location st I = MultBy a,b or ex a, b being Int-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st I = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose I = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A2, AMI_3:71, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:123, SCMFSA_2:124; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = a := b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location such that
A3: I = a := b ;
A4: InsCode I = 1 by A3, SCMFSA_2:42;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A3, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st J = a := b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location such that
A5: J = d1 := d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A3, Th18
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A5, Th18 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A4, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = AddTo a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location such that
A6: I = AddTo a,b ;
A7: InsCode I = 2 by A6, SCMFSA_2:43;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A6, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st J = AddTo a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location such that
A8: J = AddTo d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A6, Th19
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A8, Th19 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A7, SCMFSA_2:42, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = SubFrom a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location such that
A9: I = SubFrom a,b ;
A10: InsCode I = 3 by A9, SCMFSA_2:44;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A9, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st J = SubFrom a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location such that
A11: J = SubFrom d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A9, Th20
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A11, Th20 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A10, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = MultBy a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location such that
A12: I = MultBy a,b ;
A13: InsCode I = 4 by A12, SCMFSA_2:45;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A12, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st J = MultBy a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location such that
A14: J = MultBy d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A12, Th21
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A14, Th21 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A13, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = Divide a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location such that
A15: I = Divide a,b ;
A16: InsCode I = 5 by A15, SCMFSA_2:46;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location st J = Divide a,b or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A15, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st J = Divide a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location such that
A17: J = Divide d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A15, Th22
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A17, Th22 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A16, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA st I = goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i1 being Instruction-Location of SCM+FSA such that
A18: I = goto i1 ;
A19: InsCode I = 6 by A18, SCMFSA_2:47;

now

per cases ( J = [0 ,{} ] or ex i2 being Instruction-Location of SCM+FSA st J = goto i2 or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A18, AMI_3:71, SCMFSA_2:47, SCMFSA_2:123, SCMFSA_2:124; :: thesis: verum

end;

suppose ex i2 being Instruction-Location of SCM+FSA st J = goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i2 being Instruction-Location of SCM+FSA such that
A20: J = goto i2 ;
thus dom (AddressPart I) = dom <*i1*> by A18, Th23
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i2*> by FINSEQ_1:def 8
.= dom (AddressPart J) by A20, Th23 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A19, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A21: I = a =0_goto i1 ;
A22: InsCode I = 7 by A21, SCMFSA_2:48;

now

per cases ( J = [0 ,{} ] or ex i2 being Instruction-Location of SCM+FSA ex d1 being Int-Location st J = d1 =0_goto i2 or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A21, AMI_3:71, SCMFSA_2:48, SCMFSA_2:123, SCMFSA_2:124; :: thesis: verum

end;

suppose ex i2 being Instruction-Location of SCM+FSA ex d1 being Int-Location st J = d1 =0_goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1 being Int-Location , i2 being Instruction-Location of SCM+FSA such that
A23: J = d1 =0_goto i2 ;
thus dom (AddressPart I) = dom <*i1,a*> by A21, Th24
.= Seg 2 by FINSEQ_3:29
.= dom <*i2,d1*> by FINSEQ_3:29
.= dom (AddressPart J) by A23, Th24 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A22, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A24: I = a >0_goto i1 ;
A25: InsCode I = 8 by A24, SCMFSA_2:49;

now

per cases ( J = [0 ,{} ] or ex i2 being Instruction-Location of SCM+FSA ex d1 being Int-Location st J = d1 >0_goto i2 or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A24, AMI_3:71, SCMFSA_2:49, SCMFSA_2:123, SCMFSA_2:124; :: thesis: verum

end;

suppose ex i2 being Instruction-Location of SCM+FSA ex d1 being Int-Location st J = d1 >0_goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1 being Int-Location , i2 being Instruction-Location of SCM+FSA such that
A26: J = d1 >0_goto i2 ;
thus dom (AddressPart I) = dom <*i1,a*> by A24, Th25
.= Seg 2 by FINSEQ_3:29
.= dom <*i2,d1*> by FINSEQ_3:29
.= dom (AddressPart J) by A26, Th25 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex b, a being Int-Location ex f being FinSeq-Location st J = a := f,b or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A25, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location , f being FinSeq-Location such that
A27: I = b := f,a ;
A28: InsCode I = 9 by A27, SCMFSA_2:50;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A27, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location , f1 being FinSeq-Location such that
A29: J = d2 := f1,d1 ;
thus dom (AddressPart I) = dom <*b,f,a*> by A27, MCART_1:def 2
.= Seg 3 by FINSEQ_3:30
.= dom <*d2,f1,d1*> by FINSEQ_3:30
.= dom (AddressPart J) by A29, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A28, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Int-Location , f being FinSeq-Location such that
A30: I = f,a := b ;
A31: InsCode I = 10 by A30, SCMFSA_2:51;

now

per cases ( J = [0 ,{} ] or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A30, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Int-Location , f1 being FinSeq-Location such that
A32: J = f1,d1 := d2 ;
thus dom (AddressPart I) = dom <*b,f,a*> by A30, MCART_1:def 2
.= Seg 3 by FINSEQ_3:30
.= dom <*d2,f1,d1*> by FINSEQ_3:30
.= dom (AddressPart J) by A32, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A31, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:52, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Int-Location , f being FinSeq-Location such that
A33: I = a :=len f ;
A34: InsCode I = 11 by A33, SCMFSA_2:52;

now

per cases ( J = [0 ,{} ] or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A33, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st J = a :=len f ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1 being Int-Location , f1 being FinSeq-Location such that
A35: J = d1 :=len f1 ;
thus dom (AddressPart I) = dom <*a,f*> by A33, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,f1*> by FINSEQ_3:29
.= dom (AddressPart J) by A35, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A34, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:53; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Int-Location , f being FinSeq-Location such that
A36: I = f :=<0,...,0> a ;
A37: InsCode I = 12 by A36, SCMFSA_2:53;

now

per cases ( J = [0 ,{} ] or ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a or ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f ) by SCMFSA_2:120;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A36, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st J = f :=<0,...,0> a ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1 being Int-Location , f1 being FinSeq-Location such that
A38: J = f1 :=<0,...,0> d1 ;
thus dom (AddressPart I) = dom <*a,f*> by A36, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,f1*> by FINSEQ_3:29
.= dom (AddressPart J) by A38, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Int-Location st J = a := b or ex a, b being Int-Location st J = AddTo a,b or ex a, b being Int-Location st J = SubFrom a,b or ex a, b being Int-Location st J = MultBy a,b or ex a, b being Int-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st J = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st J = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st J = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st J = f,a := b or ex a being Int-Location ex f being FinSeq-Location st J = a :=len f ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A37, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

end;

end;

thus SCM+FSA is with_explicit_jumps :: thesis: SCM+FSA is without_implicit_jumps

proof

let I be Instruction of SCM+FSA ; :: according to AMISTD_2:def 8 :: thesis: I is with_explicit_jumps
let f be set ; :: according to AMISTD_2:def 6 :: thesis: ( not f in JUMP I or ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) )
assume A39: f in JUMP I ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

per cases ( I = [0 ,{} ] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo a,b or ex a, b being Int-Location st I = SubFrom a,b or ex a, b being Int-Location st I = MultBy a,b or ex a, b being Int-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st I = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose A40: I = [0 ,{} ] ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A40, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = a := b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location such that
A41: I = a := b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A41; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = AddTo a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location such that
A42: I = AddTo a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A42; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = SubFrom a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location such that
A43: I = SubFrom a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A43; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = MultBy a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location such that
A44: I = MultBy a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A44; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = Divide a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location such that
A45: I = Divide a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A45; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA st I = goto i1 ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider i1 being Instruction-Location of SCM+FSA such that
A46: I = goto i1 ;
JUMP (goto i1) = {i1} by Th75;
then A47: f = i1 by A39, A46, TARSKI:def 1;
take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
A48: AddressPart (goto i1) = <*i1*> by Th23;
dom <*i1*> = Seg 1 by FINSEQ_1:def 8;
hence 1 in dom (AddressPart I) by A46, A48, FINSEQ_1:4, TARSKI:def 1; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
thus ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A46, A47, A48, Th53, FINSEQ_1:def 8; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A49: I = a =0_goto i1 ;
JUMP (a =0_goto i1) = {i1} by Th77;
then A50: f = i1 by A39, A49, TARSKI:def 1;
take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
A51: AddressPart (a =0_goto i1) = <*i1,a*> by Th24;
dom <*i1,a*> = Seg 2 by FINSEQ_3:29;
hence 1 in dom (AddressPart I) by A49, A51, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
thus ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A49, A50, A51, Th54, FINSEQ_1:61; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A52: I = a >0_goto i1 ;
JUMP (a >0_goto i1) = {i1} by Th79;
then A53: f = i1 by A39, A52, TARSKI:def 1;
take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
A54: AddressPart (a >0_goto i1) = <*i1,a*> by Th25;
dom <*i1,a*> = Seg 2 by FINSEQ_3:29;
hence 1 in dom (AddressPart I) by A52, A54, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
thus ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A52, A53, A54, Th56, FINSEQ_1:61; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location , f being FinSeq-Location such that
A55: I = b := f,a ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A55; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a, b being Int-Location , f being FinSeq-Location such that
A56: I = f,a := b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A56; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a being Int-Location , f being FinSeq-Location such that
A57: I = a :=len f ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A57; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

then consider a being Int-Location , f being FinSeq-Location such that
A58: I = f :=<0,...,0> a ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, A58; :: thesis: verum

end;

end;

end;

let I be Instruction of SCM+FSA ; :: according to AMISTD_2:def 9 :: thesis: I is without_implicit_jumps
let f be set ; :: according to AMISTD_2:def 7 :: thesis: ( for b₁ being set holds
( not b₁ in dom (AddressPart I) or not f = (AddressPart I) . b₁ or not (product" (AddressParts (InsCode I))) . b₁ = K53() ) or f in JUMP I )
given k being set such that A59: k in dom (AddressPart I) and
A60: f = (AddressPart I) . k and
A61: (product" (AddressParts (InsCode I))) . k = NAT ; :: thesis: f in JUMP I

per cases ( I = [0 ,{} ] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo a,b or ex a, b being Int-Location st I = SubFrom a,b or ex a, b being Int-Location st I = MultBy a,b or ex a, b being Int-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st I = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose I = [0 ,{} ] ; :: thesis: f in JUMP I

then dom (AddressPart I) = dom {} by MCART_1:def 2;
hence f in JUMP I by A59; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = a := b ; :: thesis: f in JUMP I

then consider a, b being Int-Location such that
A62: I = a := b ;
k in dom <*a,b*> by A59, A62, Th18;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A62, Th5, Th43, Th44; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = AddTo a,b ; :: thesis: f in JUMP I

then consider a, b being Int-Location such that
A63: I = AddTo a,b ;
k in dom <*a,b*> by A59, A63, Th19;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A63, Th5, Th45, Th46; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = SubFrom a,b ; :: thesis: f in JUMP I

then consider a, b being Int-Location such that
A64: I = SubFrom a,b ;
k in dom <*a,b*> by A59, A64, Th20;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A64, Th5, Th47, Th48; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = MultBy a,b ; :: thesis: f in JUMP I

then consider a, b being Int-Location such that
A65: I = MultBy a,b ;
k in dom <*a,b*> by A59, A65, Th21;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A65, Th5, Th49, Th50; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = Divide a,b ; :: thesis: f in JUMP I

then consider a, b being Int-Location such that
A66: I = Divide a,b ;
k in dom <*a,b*> by A59, A66, Th22;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A66, Th5, Th51, Th52; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA st I = goto i1 ; :: thesis: f in JUMP I

then consider i1 being Instruction-Location of SCM+FSA such that
A67: I = goto i1 ;
A68: AddressPart I = <*i1*> by A67, Th23;
then k = 1 by A59, Lm1;
then A69: f = i1 by A60, A68, FINSEQ_1:def 8;
JUMP I = {i1} by A67, Th75;
hence f in JUMP I by A69, TARSKI:def 1; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 ; :: thesis: f in JUMP I

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A70: I = a =0_goto i1 ;
A71: AddressPart I = <*i1,a*> by A70, Th24;
then ( k = 1 or k = 2 ) by A59, Lm2;
then A72: f = i1 by A60, A61, A70, A71, Th5, Th55, FINSEQ_1:61;
JUMP I = {i1} by A70, Th77;
hence f in JUMP I by A72, TARSKI:def 1; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 ; :: thesis: f in JUMP I

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A73: I = a >0_goto i1 ;
A74: AddressPart I = <*i1,a*> by A73, Th25;
then ( k = 1 or k = 2 ) by A59, Lm2;
then A75: f = i1 by A60, A61, A73, A74, Th5, Th57, FINSEQ_1:61;
JUMP I = {i1} by A73, Th79;
hence f in JUMP I by A75, TARSKI:def 1; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a ; :: thesis: f in JUMP I

then consider a, b being Int-Location , f being FinSeq-Location such that
A76: I = b := f,a ;
k in dom <*b,f,a*> by A59, A76, MCART_1:def 2;
then ( k = 1 or k = 2 or k = 3 ) by Lm3;
hence f in JUMP I by A61, A76, Th5, Th6, Th58, Th59, Th60; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b ; :: thesis: f in JUMP I

then consider a, b being Int-Location , f being FinSeq-Location such that
A77: I = f,a := b ;
k in dom <*b,f,a*> by A59, A77, MCART_1:def 2;
then ( k = 1 or k = 2 or k = 3 ) by Lm3;
hence f in JUMP I by A61, A77, Th5, Th6, Th61, Th62, Th63; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: f in JUMP I

then consider a being Int-Location , f being FinSeq-Location such that
A78: I = a :=len f ;
k in dom <*a,f*> by A59, A78, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A78, Th5, Th6, Th64, Th65; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: f in JUMP I

then consider a being Int-Location , f being FinSeq-Location such that
A79: I = f :=<0,...,0> a ;
k in dom <*a,f*> by A59, A79, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A61, A79, Th5, Th6, Th66, Th67; :: thesis: verum

end;

end;