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

assume f in rng (JumpPart I) ; :: thesis: f in JUMP I

then consider k being object such that

A11: k in dom (JumpPart I) and

A12: f = (JumpPart I) . k by FUNCT_1:def 3;

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 proj2 (JumpPart I) or f in JUMP I )
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)

end;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;

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: rng <*k1*> = {k1} by FINSEQ_1:39;

JUMP (SCM-goto k1) = {k1} by Th16;

hence f in rng (JumpPart I) by A1, A3, A4; :: thesis: verum

end;A3: I = SCM-goto k1 by A2;

A4: rng <*k1*> = {k1} by FINSEQ_1:39;

JUMP (SCM-goto k1) = {k1} by Th16;

hence f in rng (JumpPart I) by A1, A3, A4; :: thesis: verum

suppose A5:
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

A6: I = a =0_goto k1 by A5;

A7: rng <*k1*> = {k1} by FINSEQ_1:39;

JUMP (a =0_goto k1) = {k1} by Th18;

hence f in rng (JumpPart I) by A1, A6, A7; :: thesis: verum

end;A6: I = a =0_goto k1 by A5;

A7: rng <*k1*> = {k1} by FINSEQ_1:39;

JUMP (a =0_goto k1) = {k1} by Th18;

hence f in rng (JumpPart I) by A1, A6, A7; :: thesis: verum

suppose A8:
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

A9: I = a >0_goto k1 by A8;

A10: rng <*k1*> = {k1} by FINSEQ_1:39;

JUMP (a >0_goto k1) = {k1} by Th20;

hence f in rng (JumpPart I) by A1, A9, A10; :: thesis: verum

end;A9: I = a >0_goto k1 by A8;

A10: rng <*k1*> = {k1} by FINSEQ_1:39;

JUMP (a >0_goto k1) = {k1} by Th20;

hence f in rng (JumpPart I) by A1, A9, A10; :: thesis: verum

assume f in rng (JumpPart I) ; :: thesis: f in JUMP I

then consider k being object such that

A11: k in dom (JumpPart I) and

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

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

A13: I = a := b ;

k in dom {} by A11, A13;

hence f in JUMP I ; :: thesis: verum

end;A13: I = a := b ;

k in dom {} by A11, A13;

hence f in JUMP I ; :: thesis: verum

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

A14: I = AddTo (a,b) ;

k in dom {} by A11, A14;

hence f in JUMP I ; :: thesis: verum

end;A14: I = AddTo (a,b) ;

k in dom {} by A11, A14;

hence f in JUMP I ; :: thesis: verum

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

A15: I = SubFrom (a,b) ;

k in dom {} by A11, A15;

hence f in JUMP I ; :: thesis: verum

end;A15: I = SubFrom (a,b) ;

k in dom {} by A11, A15;

hence f in JUMP I ; :: thesis: verum

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

A16: I = MultBy (a,b) ;

k in dom {} by A11, A16;

hence f in JUMP I ; :: thesis: verum

end;A16: I = MultBy (a,b) ;

k in dom {} by A11, A16;

hence f in JUMP I ; :: thesis: verum

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

A17: I = Divide (a,b) ;

k in dom {} by A11, A17;

hence f in JUMP I ; :: thesis: verum

end;A17: I = Divide (a,b) ;

k in dom {} by A11, A17;

hence f in JUMP I ; :: thesis: verum

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

then consider k1 being Nat such that

A18: I = SCM-goto k1 ;

A19: JumpPart I = <*k1*> by A18;

then k = 1 by A11, FINSEQ_1:90;

then A20: f = k1 by A19, A12, FINSEQ_1:def 8;

JUMP I = {k1} by A18, Th16;

hence f in JUMP I by A20, TARSKI:def 1; :: thesis: verum

end;A18: I = SCM-goto k1 ;

A19: JumpPart I = <*k1*> by A18;

then k = 1 by A11, FINSEQ_1:90;

then A20: f = k1 by A19, A12, FINSEQ_1:def 8;

JUMP I = {k1} by A18, Th16;

hence f in JUMP I by A20, TARSKI:def 1; :: thesis: verum

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

A21: I = a =0_goto k1 ;

A22: JumpPart I = <*k1*> by A21;

then k = 1 by A11, FINSEQ_1:90;

then A23: f = k1 by A22, A12, FINSEQ_1:40;

JUMP I = {k1} by A21, Th18;

hence f in JUMP I by A23, TARSKI:def 1; :: thesis: verum

end;A21: I = a =0_goto k1 ;

A22: JumpPart I = <*k1*> by A21;

then k = 1 by A11, FINSEQ_1:90;

then A23: f = k1 by A22, A12, FINSEQ_1:40;

JUMP I = {k1} by A21, Th18;

hence f in JUMP I by A23, TARSKI:def 1; :: thesis: verum

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

A24: I = a >0_goto k1 ;

A25: JumpPart I = <*k1*> by A24;

then k = 1 by A11, FINSEQ_1:90;

then A26: f = k1 by A25, A12, FINSEQ_1:40;

JUMP I = {k1} by A24, Th20;

hence f in JUMP I by A26, TARSKI:def 1; :: thesis: verum

end;A24: I = a >0_goto k1 ;

A25: JumpPart I = <*k1*> by A24;

then k = 1 by A11, FINSEQ_1:90;

then A26: f = k1 by A25, A12, FINSEQ_1:40;

JUMP I = {k1} by A24, Th20;

hence f in JUMP I by A26, TARSKI:def 1; :: thesis: verum