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 (I `2_3 ) = dom (J `2_3 ) )
assume A1: InsCode I = InsCode J ; :: thesis: dom (I `2_3 ) = dom (J `2_3 )
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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 )

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location such that
A5: J = d1 := d2 ;
thus dom (JumpPart I) = dom {} by A3, Th18
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location such that
A8: J = AddTo d1,d2 ;
thus dom (JumpPart I) = dom {} by A6, Th19
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location such that
A11: J = SubFrom d1,d2 ;
thus dom (JumpPart I) = dom {} by A9, Th20
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location such that
A14: J = MultBy d1,d2 ;
thus dom (JumpPart I) = dom {} by A12, Th21
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location such that
A17: J = Divide d1,d2 ;
thus dom (JumpPart I) = dom {} by A15, Th22
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

suppose ex i1 being Element of NAT st I = goto i1 ; :: thesis: dom (I `2_3 ) = dom (J `2_3 )

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider i2 being Element of NAT such that
A20: J = goto i2 ;
thus dom (JumpPart I) = dom <*i1*> by A18, RECDEF_2:def 2
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i2*> by FINSEQ_1:def 8
.= dom (JumpPart J) by A20, RECDEF_2: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 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; :: thesis: dom (I `2_3 ) = dom (J `2_3 )

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1 being Int-Location , i2 being Element of NAT such that
A23: J = d1 =0_goto i2 ;
thus dom (JumpPart I) = dom <*i1*> by A21, Th24
.= Seg 1 by FINSEQ_1:55
.= dom <*i2*> by FINSEQ_1:55
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; :: thesis: dom (I `2_3 ) = dom (J `2_3 )

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1 being Int-Location , i2 being Element of NAT such that
A26: J = d1 >0_goto i2 ;
thus dom (JumpPart I) = dom <*i1*> by A24, Th25
.= Seg 1 by FINSEQ_1:55
.= dom <*i2*> by FINSEQ_1:55
.= dom (JumpPart 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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location , f1 being FinSeq-Location such that
A29: J = d2 := f1,d1 ;
thus dom (JumpPart I) = dom {} by A27, RECDEF_2:def 2
.= dom (JumpPart J) by A29, RECDEF_2: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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1, d2 being Int-Location , f1 being FinSeq-Location such that
A32: J = f1,d1 := d2 ;
thus dom (JumpPart I) = dom {} by A30, RECDEF_2:def 2
.= dom (JumpPart J) by A32, RECDEF_2: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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1 being Int-Location , f1 being FinSeq-Location such that
A35: J = d1 :=len f1 ;
thus dom (JumpPart I) = dom {} by A33, RECDEF_2:def 2
.= dom (JumpPart J) by A35, RECDEF_2: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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: thesis: verum

end;

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

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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (JumpPart I) = dom (JumpPart J)

then consider d1 being Int-Location , f1 being FinSeq-Location such that
A38: J = f1 :=<0,...,0> d1 ;
thus dom (JumpPart I) = dom {} by A36, RECDEF_2:def 2
.= dom (JumpPart J) by A38, RECDEF_2: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 (I `2_3 ) = dom (J `2_3 )

hence dom (I `2_3 ) = dom (J `2_3 ) 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 (I `2_3 ) = dom (J `2_3 ) ; :: 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 TARSKI:def 3,AMISTD_2:def 6 :: thesis: ( not f in JUMP I or f in proj2 (I `2_3 ) )
assume A39: f in JUMP I ; :: thesis: f in proj2 (I `2_3 )

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 proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39, AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = a := b ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = AddTo a,b ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = SubFrom a,b ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = MultBy a,b ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = Divide a,b ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose A40: ex i1 being Element of NAT st I = goto i1 ; :: thesis: f in proj2 (I `2_3 )

consider i1 being Element of NAT such that
A41: I = goto i1 by A40;
A42: JumpPart (goto i1) = <*i1*> by RECDEF_2:def 2;
X: rng <*i1*> = {i1} by FINSEQ_1:56;
JUMP (goto i1) = {i1} by Th75;
then f = i1 by A39, A41, TARSKI:def 1;
hence f in proj2 (I `2_3 ) by A41, A42, X, TARSKI:def 1; :: thesis: verum

end;

suppose A43: ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; :: thesis: f in proj2 (I `2_3 )

consider a being Int-Location , i1 being Element of NAT such that
A44: I = a =0_goto i1 by A43;
A45: JumpPart (a =0_goto i1) = <*i1*> by Th24;
X: rng <*i1*> = {i1} by FINSEQ_1:56;
JUMP (a =0_goto i1) = {i1} by Th77;
then f = i1 by A39, A44, TARSKI:def 1;
hence f in proj2 (I `2_3 ) by A44, A45, X, TARSKI:def 1; :: thesis: verum

end;

suppose A46: ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; :: thesis: f in proj2 (I `2_3 )

consider a being Int-Location , i1 being Element of NAT such that
A47: I = a >0_goto i1 by A46;
A48: JumpPart (a >0_goto i1) = <*i1*> by Th25;
X: rng <*i1*> = {i1} by FINSEQ_1:56;
JUMP (a >0_goto i1) = {i1} by Th79;
then f = i1 by A39, A47, TARSKI:def 1;
hence f in proj2 (I `2_3 ) by A47, A48, X, 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 proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) by A39; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: f in proj2 (I `2_3 )

hence f in proj2 (I `2_3 ) 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 TARSKI:def 3,AMISTD_2:def 7 :: thesis: ( not f in proj2 (I `2_3 ) or f in JUMP I )
assume f in rng (JumpPart I) ; :: thesis: f in JUMP I
then consider k being set such that
A49: k in dom (JumpPart I) and
B49: f = (JumpPart I) . k by FUNCT_1:def 5;

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 (JumpPart I) = dom {} by RECDEF_2: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 {} by A49, A52, Th18;
hence f in JUMP I ; :: 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 {} by A49, A53, Th19;
hence f in JUMP I ; :: 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 {} by A49, A54, Th20;
hence f in JUMP I ; :: 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 {} by A49, A55, Th21;
hence f in JUMP I ; :: 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 {} by A49, A56, Th22;
hence f in JUMP I ; :: 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: JumpPart I = <*i1*> by A57, RECDEF_2:def 2;
then k = 1 by A49, FINSEQ_1:111;
then A59: f = i1 by A58, B49, 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: JumpPart I = <*i1*> by A60, Th24;
then k = 1 by A49, FINSEQ_1:111;
then A62: f = i1 by A61, B49, FINSEQ_1:def 8;
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: JumpPart I = <*i1*> by A63, Th25;
then k = 1 by A49, FINSEQ_1:111;
then A65: f = i1 by A64, B49, FINSEQ_1:def 8;
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 {} by A49, A66, RECDEF_2:def 2;
hence f in JUMP I ; :: 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 {} by A49, A67, RECDEF_2:def 2;
hence f in JUMP I ; :: 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 {} by A49, A68, RECDEF_2:def 2;
hence f in JUMP I ; :: 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 {} by A49, A69, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

end;