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

proof

let I, J be Instruction of SCM+FSA; :: according to COMPOS_1:def 33 :: 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: verum

proof

let I be Instruction of SCM+FSA; :: according to AMISTD_2:def 8 :: thesis: I is with_explicit_jumps
thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def 6,XBOOLE_0:def 10 :: thesis: proj2 (I `2_3) c= JUMP I

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in JUMP I or f in rng (JumpPart I) )
assume A39: f in JUMP I ; :: thesis: f in rng (JumpPart 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 rng (JumpPart I)

hence f in rng (JumpPart I) 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 rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = AddTo (a,b) ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = SubFrom (a,b) ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = MultBy (a,b) ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = Divide (a,b) ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

suppose A40: ex i1 being Element of NAT st I = goto i1 ; :: thesis: f in rng (JumpPart I)

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 rng (JumpPart I) 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 rng (JumpPart I)

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 rng (JumpPart I) 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 rng (JumpPart I)

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 rng (JumpPart I) 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 rng (JumpPart I)

hence f in rng (JumpPart I) 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 rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) 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 rng (JumpPart I)

hence f in rng (JumpPart I) by A39; :: thesis: verum

end;

end;

end;

let f be set ; :: according to TARSKI:def 3 :: 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;

end;