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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st I = goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i1 being Element of NAT such that
A18: I = goto i1 ;
A19: InsCode I = 6 by A18, SCMFSA_2:47;

now

per cases ( J = [0 ,{} ] or ex i2 being Element of NAT 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 Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i2 being Element of NAT 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 Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT 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 Element of NAT 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 Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT 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 Element of NAT 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 Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT 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 Element of NAT 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 Element of NAT 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 Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT 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 Element of NAT 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 Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st J = goto i1 or ex i1 being Element of NAT ex a being Int-Location st J = a =0_goto i1 or ex i1 being Element of NAT 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 Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT 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: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39, 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: thesis: verum

end;

suppose A40: ex i1 being Element of NAT 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() )

take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
consider i1 being Element of NAT such that
A41: I = goto i1 by A40;
A42: AddressPart (goto i1) = <*i1*> by Th23;
dom <*i1*> = Seg 1 by FINSEQ_1:def 8;
hence 1 in dom (AddressPart I) by A41, A42, FINSEQ_1:4, TARSKI:def 1; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
JUMP (goto i1) = {i1} by Th75;
then f = i1 by A39, A41, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A41, A42, Th53, FINSEQ_1:def 8; :: thesis: verum

end;

suppose A43: ex i1 being Element of NAT 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() )

take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
consider a being Int-Location , i1 being Element of NAT such that
A44: I = a =0_goto i1 by A43;
A45: 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 A44, A45, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
JUMP (a =0_goto i1) = {i1} by Th77;
then f = i1 by A39, A44, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A44, A45, Th54, FINSEQ_1:61; :: thesis: verum

end;

suppose A46: ex i1 being Element of NAT 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() )

take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
consider a being Int-Location , i1 being Element of NAT such that
A47: I = a >0_goto i1 by A46;
A48: 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 A47, A48, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = K53() )
JUMP (a >0_goto i1) = {i1} by Th79;
then f = i1 by A39, A47, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A47, A48, 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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() )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = K53() ) by A39; :: 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 A49: k in dom (AddressPart I) and
A50: f = (AddressPart I) . k and
A51: (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 Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT 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 A49; :: 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
A52: I = a := b ;
k in dom <*a,b*> by A49, A52, Th18;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A52, 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
A53: I = AddTo a,b ;
k in dom <*a,b*> by A49, A53, Th19;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A53, 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
A54: I = SubFrom a,b ;
k in dom <*a,b*> by A49, A54, Th20;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A54, 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
A55: I = MultBy a,b ;
k in dom <*a,b*> by A49, A55, Th21;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A55, 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
A56: I = Divide a,b ;
k in dom <*a,b*> by A49, A56, Th22;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A56, Th5, Th51, Th52; :: thesis: verum

end;

suppose ex i1 being Element of NAT st I = goto i1 ; :: thesis: f in JUMP I

then consider i1 being Element of NAT such that
A57: I = goto i1 ;
A58: AddressPart I = <*i1*> by A57, Th23;
then k = 1 by A49, Lm1;
then A59: f = i1 by A50, A58, FINSEQ_1:def 8;
JUMP I = {i1} by A57, Th75;
hence f in JUMP I by A59, TARSKI:def 1; :: thesis: verum

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; :: thesis: f in JUMP I

then consider a being Int-Location , i1 being Element of NAT such that
A60: I = a =0_goto i1 ;
A61: AddressPart I = <*i1,a*> by A60, Th24;
then ( k = 1 or k = 2 ) by A49, Lm2;
then A62: f = i1 by A50, A51, A60, A61, Th5, Th55, FINSEQ_1:61;
JUMP I = {i1} by A60, Th77;
hence f in JUMP I by A62, TARSKI:def 1; :: thesis: verum

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; :: thesis: f in JUMP I

then consider a being Int-Location , i1 being Element of NAT such that
A63: I = a >0_goto i1 ;
A64: AddressPart I = <*i1,a*> by A63, Th25;
then ( k = 1 or k = 2 ) by A49, Lm2;
then A65: f = i1 by A50, A51, A63, A64, Th5, Th57, FINSEQ_1:61;
JUMP I = {i1} by A63, Th79;
hence f in JUMP I by A65, 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
A66: I = b := f,a ;
k in dom <*b,f,a*> by A49, A66, MCART_1:def 2;
then ( k = 1 or k = 2 or k = 3 ) by Lm3;
hence f in JUMP I by A51, A66, 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
A67: I = f,a := b ;
k in dom <*b,f,a*> by A49, A67, MCART_1:def 2;
then ( k = 1 or k = 2 or k = 3 ) by Lm3;
hence f in JUMP I by A51, A67, 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
A68: I = a :=len f ;
k in dom <*a,f*> by A49, A68, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A68, 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
A69: I = f :=<0,...,0> a ;
k in dom <*a,f*> by A49, A69, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A51, A69, Th5, Th6, Th66, Th67; :: thesis: verum

end;

end;