let I be Instruction of SCM; :: according to AMISTD_2:def 2 :: thesis:
thus JUMP I c= rng () :: according to AMISTD_2:def 1,XBOOLE_0:def 10 :: thesis: proj2 () c= JUMP I
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in JUMP I or f in rng () )
assume A1: f in JUMP I ; :: thesis: f in rng ()
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 A2: ex k being Nat st I = SCM-goto k ; :: thesis: f in rng ()
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 () by A1, A3, A4; :: thesis: verum
end;
suppose A5: ex a being Data-Location ex k1 being Nat st I = a =0_goto k1 ; :: thesis: f in rng ()
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 () by A1, A6, A7; :: thesis: verum
end;
suppose A8: ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ; :: thesis: f in rng ()
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 () by A1, A9, A10; :: thesis: verum
end;
end;
end;
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in proj2 () or f in JUMP I )
assume f in rng () ; :: thesis: f in JUMP I
then consider k being object such that
A11: k in dom () and
A12: f = () . 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 () = dom {} ;
hence f in JUMP I by A11; :: 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
A13: I = a := b ;
k in dom {} by ;
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
A14: I = AddTo (a,b) ;
k in dom {} by ;
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
A15: I = SubFrom (a,b) ;
k in dom {} by ;
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
A16: I = MultBy (a,b) ;
k in dom {} by ;
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
A17: I = Divide (a,b) ;
k in dom {} by ;
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
A18: I = SCM-goto k1 ;
A19: JumpPart I = <*k1*> by A18;
then k = 1 by ;
then A20: f = k1 by ;
JUMP I = {k1} by ;
hence f in JUMP I by ; :: 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
A21: I = a =0_goto k1 ;
A22: JumpPart I = <*k1*> by A21;
then k = 1 by ;
then A23: f = k1 by ;
JUMP I = {k1} by ;
hence f in JUMP I by ; :: 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
A24: I = a >0_goto k1 ;
A25: JumpPart I = <*k1*> by A24;
then k = 1 by ;
then A26: f = k1 by ;
JUMP I = {k1} by ;
hence f in JUMP I by ; :: thesis: verum
end;
end;