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 (JumpPart I) c= JUMP I

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in JUMP I or f in rng (JumpPart I) )
assume A1: 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 Nat st I = goto i1 or ex i1 being Nat ex a being Int-Location st I = a =0_goto i1 or ex i1 being 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 A1, 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 A1; :: 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 A1; :: 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 A1; :: 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 A1; :: 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 A1; :: thesis: verum

end;

suppose A2: ex i1 being Nat st I = goto i1 ; :: thesis: f in rng (JumpPart I)

consider i1 being Nat such that
A3: I = goto i1 by A2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A3, Th34; :: thesis: verum

end;

suppose A4: ex i1 being 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 Nat such that
A5: I = a =0_goto i1 by A4;
A6: JumpPart (a =0_goto i1) = <*i1*> by Th15;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A5, A6, Th36; :: thesis: verum

end;

suppose A7: ex i1 being 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 Nat such that
A8: I = a >0_goto i1 by A7;
A9: JumpPart (a >0_goto i1) = <*i1*> by Th16;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A8, A9, Th38; :: 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 A1; :: 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 A1; :: 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 A1; :: 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 A1; :: thesis: verum

end;

end;

end;

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in proj2 (JumpPart I) or f in JUMP I )
assume f in rng (JumpPart I) ; :: thesis: f in JUMP I
then consider k being object such that
A10: k in dom (JumpPart I) and
A11: 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 Nat st I = goto i1 or ex i1 being Nat ex a being Int-Location st I = a =0_goto i1 or ex i1 being 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 {} ;
hence f in JUMP I by A10; :: 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
A12: I = a := b ;
k in dom {} by A10, A12, Th10;
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
A13: I = AddTo (a,b) ;
k in dom {} by A10, A13, Th11;
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
A14: I = SubFrom (a,b) ;
k in dom {} by A10, A14, Th12;
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
A15: I = MultBy (a,b) ;
k in dom {} by A10, A15, Th13;
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
A16: I = Divide (a,b) ;
k in dom {} by A10, A16, Th14;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex i1 being Nat st I = goto i1 ; :: thesis: f in JUMP I

then consider i1 being Nat such that
A17: I = goto i1 ;
A18: JumpPart I = <*i1*> by A17;
then k = 1 by A10, FINSEQ_1:90;
then A19: f = i1 by A18, A11;
JUMP I = {i1} by A17, Th34;
hence f in JUMP I by A19, TARSKI:def 1; :: thesis: verum

end;

suppose ex i1 being 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 Nat such that
A20: I = a =0_goto i1 ;
A21: JumpPart I = <*i1*> by A20, Th15;
then k = 1 by A10, FINSEQ_1:90;
then A22: f = i1 by A21, A11;
JUMP I = {i1} by A20, Th36;
hence f in JUMP I by A22, TARSKI:def 1; :: thesis: verum

end;

suppose ex i1 being 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 Nat such that
A23: I = a >0_goto i1 ;
A24: JumpPart I = <*i1*> by A23, Th16;
then k = 1 by A10, FINSEQ_1:90;
then A25: f = i1 by A24, A11;
JUMP I = {i1} by A23, Th38;
hence f in JUMP I by A25, 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
A26: I = b := (f,a) ;
k in dom {} by A10, A26;
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
A27: I = (f,a) := b ;
k in dom {} by A10, A27;
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
A28: I = a :=len f ;
k in dom {} by A10, A28;
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
A29: I = f :=<0,...,0> a ;
k in dom {} by A10, A29;
hence f in JUMP I ; :: thesis: verum

end;

end;