let I be Instruction of SCM; AMISTD_2:def 2 I is with_explicit_jumps
thus
JUMP I c= rng (JumpPart I)
AMISTD_2:def 1,XBOOLE_0:def 10 proj2 (JumpPart I) c= JUMP Iproof
let f be
object ;
TARSKI:def 3 ( not f in JUMP I or f in rng (JumpPart I) )
assume A1:
f in JUMP I
;
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;
end;
let f be object ; TARSKI:def 3 ( not f in proj2 (JumpPart I) or f in JUMP I )
assume
f in rng (JumpPart I)
; 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;