let I be Instruction of SCM; :: 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 set ; :: 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 Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex k being Nat st I = SCM-goto k or ex a being Data-Location ex k1 being Nat st I = a =0_goto k1 or ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ) by AMI_3:24;

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

hence f in rng (JumpPart I) by A1, AMI_3:26; :: thesis: verum

end;

suppose ex a, b being Data-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 Data-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 Data-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 Data-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 Data-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 k being Nat st I = SCM-goto k ; :: thesis: f in rng (JumpPart I)

consider k1 being Nat such that
A3: I = SCM-goto k1 by A2;
A4: JumpPart (SCM-goto k1) = <*k1*> by RECDEF_2:def 2;
A5: rng <*k1*> = {k1} by FINSEQ_1:39;
JUMP (SCM-goto k1) = {k1} by Th16;
hence f in rng (JumpPart I) by A1, A3, A4, A5; :: thesis: verum

end;

suppose A6: ex a being Data-Location ex k1 being Nat st I = a =0_goto k1 ; :: thesis: f in rng (JumpPart I)

consider a being Data-Location, k1 being Nat such that
A7: I = a =0_goto k1 by A6;
A8: JumpPart (a =0_goto k1) = <*k1*> by RECDEF_2:def 2;
A9: rng <*k1*> = {k1} by FINSEQ_1:39;
JUMP (a =0_goto k1) = {k1} by Th18;
hence f in rng (JumpPart I) by A1, A7, A8, A9; :: thesis: verum

end;

suppose A10: ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ; :: thesis: f in rng (JumpPart I)

consider a being Data-Location, k1 being Nat such that
A11: I = a >0_goto k1 by A10;
A12: JumpPart (a >0_goto k1) = <*k1*> by RECDEF_2:def 2;
A13: rng <*k1*> = {k1} by FINSEQ_1:39;
JUMP (a >0_goto k1) = {k1} by Th20;
hence f in rng (JumpPart I) by A1, A11, A12, A13; :: thesis: verum

end;

end;

end;

let f be set ; :: 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 set such that
A14: k in dom (JumpPart I) and
A15: f = (JumpPart I) . k by FUNCT_1:def 3;

per cases ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex k being Nat st I = SCM-goto k or ex a being Data-Location ex k being Nat st I = a =0_goto k or ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ) by AMI_3:24;

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

then dom (JumpPart I) = dom {} by RECDEF_2:def 2;
hence f in JUMP I by A14; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = a := b ; :: thesis: f in JUMP I

then consider a, b being Data-Location such that
A16: I = a := b ;
k in dom {} by A14, A16, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = AddTo (a,b) ; :: thesis: f in JUMP I

then consider a, b being Data-Location such that
A17: I = AddTo (a,b) ;
k in dom {} by A14, A17, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = SubFrom (a,b) ; :: thesis: f in JUMP I

then consider a, b being Data-Location such that
A18: I = SubFrom (a,b) ;
k in dom {} by A14, A18, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = MultBy (a,b) ; :: thesis: f in JUMP I

then consider a, b being Data-Location such that
A19: I = MultBy (a,b) ;
k in dom {} by A14, A19, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = Divide (a,b) ; :: thesis: f in JUMP I

then consider a, b being Data-Location such that
A20: I = Divide (a,b) ;
k in dom {} by A14, A20, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex k being Nat st I = SCM-goto k ; :: thesis: f in JUMP I

then consider k1 being Nat such that
A21: I = SCM-goto k1 ;
A22: JumpPart I = <*k1*> by A21, RECDEF_2:def 2;
then k = 1 by A14, FINSEQ_1:90;
then A23: f = k1 by A22, A15, FINSEQ_1:def 8;
JUMP I = {k1} by A21, Th16;
hence f in JUMP I by A23, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location ex k being Nat st I = a =0_goto k ; :: thesis: f in JUMP I

then consider a being Data-Location, k1 being Nat such that
A24: I = a =0_goto k1 ;
A25: JumpPart I = <*k1*> by A24, RECDEF_2:def 2;
then k = 1 by A14, FINSEQ_1:90;
then A26: f = k1 by A25, A15, FINSEQ_1:40;
JUMP I = {k1} by A24, Th18;
hence f in JUMP I by A26, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ; :: thesis: f in JUMP I

then consider a being Data-Location, k1 being Nat such that
A27: I = a >0_goto k1 ;
A28: JumpPart I = <*k1*> by A27, RECDEF_2:def 2;
then k = 1 by A14, FINSEQ_1:90;
then A29: f = k1 by A28, A15, FINSEQ_1:40;
JUMP I = {k1} by A27, Th20;
hence f in JUMP I by A29, TARSKI:def 1; :: thesis: verum

end;

end;