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 12 :: 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:93;

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:93;

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:26, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:96, SCMFSA_2:97; :: 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:18;

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:93;

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:26, SCMFSA_2:96; :: 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:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: 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:19;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:20;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:21;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:22;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:23;

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:93;

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:26, SCMFSA_2:23, SCMFSA_2:96, SCMFSA_2:97; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:24;

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:93;

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:26, SCMFSA_2:24, SCMFSA_2:96, SCMFSA_2:97; :: thesis: verum

end;

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

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:38
.= dom <*i2*> by FINSEQ_1:38
.= 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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:25;

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:93;

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:26, SCMFSA_2:25, SCMFSA_2:96, SCMFSA_2:97; :: thesis: verum

end;

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

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:38
.= dom <*i2*> by FINSEQ_1:38
.= 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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:26;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:27, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:27;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:28, SCMFSA_2:29; :: thesis: verum

end;

end;

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:28;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

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

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:29; :: thesis: verum

end;

end;

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:29;

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:93;

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:26, SCMFSA_2:96; :: thesis: verum

end;

suppose 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)

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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:26, SCMFSA_2:27, SCMFSA_2:28; :: thesis: verum

end;

end;

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 2 :: thesis: I is with_explicit_jumps
thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def 1,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:93;

suppose I = [0,{},{}] ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) by A39, AMI_3:26, SCMFSA_2:96; :: 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;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A39, A41, A42, Th75; :: thesis: verum

end;

suppose A44: 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
A45: I = a =0_goto i1 by A44;
A46: JumpPart (a =0_goto i1) = <*i1*> by Th24;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A39, A45, A46, Th77; :: thesis: verum

end;

suppose A48: 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
A49: I = a >0_goto i1 by A48;
A50: JumpPart (a >0_goto i1) = <*i1*> by Th25;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A39, A49, A50, Th79; :: 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
A52: k in dom (JumpPart I) and
A53: f = (JumpPart I) . k by FUNCT_1:def 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:93;

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

then dom (JumpPart I) = dom {} by RECDEF_2:def 2;
hence f in JUMP I by A52; :: 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
A54: I = a := b ;
k in dom {} by A52, A54, 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
A55: I = AddTo (a,b) ;
k in dom {} by A52, A55, 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
A56: I = SubFrom (a,b) ;
k in dom {} by A52, A56, 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
A57: I = MultBy (a,b) ;
k in dom {} by A52, A57, 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
A58: I = Divide (a,b) ;
k in dom {} by A52, A58, 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
A59: I = goto i1 ;
A60: JumpPart I = <*i1*> by A59, RECDEF_2:def 2;
then k = 1 by A52, FINSEQ_1:90;
then A61: f = i1 by A60, A53, FINSEQ_1:def 8;
JUMP I = {i1} by A59, Th75;
hence f in JUMP I by A61, 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
A62: I = a =0_goto i1 ;
A63: JumpPart I = <*i1*> by A62, Th24;
then k = 1 by A52, FINSEQ_1:90;
then A64: f = i1 by A63, A53, FINSEQ_1:def 8;
JUMP I = {i1} by A62, Th77;
hence f in JUMP I by A64, 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
A65: I = a >0_goto i1 ;
A66: JumpPart I = <*i1*> by A65, Th25;
then k = 1 by A52, FINSEQ_1:90;
then A67: f = i1 by A66, A53, FINSEQ_1:def 8;
JUMP I = {i1} by A65, Th79;
hence f in JUMP I by A67, 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
A68: I = b := (f,a) ;
k in dom {} by A52, A68, 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
A69: I = (f,a) := b ;
k in dom {} by A52, A69, 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
A70: I = a :=len f ;
k in dom {} by A52, A70, 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
A71: I = f :=<0,...,0> a ;
k in dom {} by A52, A71, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

end;

end;