let I be Instruction of SCM+FSA; 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 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;
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
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;
end;