begin
set A = NAT ;
Lm1:
for s being State of SCM+FSA st IC s = 0 holds
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st a := k c= P holds
P halts_on s
Lm2:
for p1, p2, p3, p4 being XFinSequence holds ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4)
Lm3:
for c0 being Element of NAT
for s being b1 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
Lm4:
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st aSeq (a,k) c= P holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i
Lm5:
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
P halts_on s
definition
let i be
Instruction of
SCM+FSA;
let a be
Int-Location;
pred i refers a means
not for
b being
Int-Location for
l being
Element of
NAT for
f being
FinSeq-Location holds
(
b := a <> i &
AddTo (
b,
a)
<> i &
SubFrom (
b,
a)
<> i &
MultBy (
b,
a)
<> i &
Divide (
b,
a)
<> i &
Divide (
a,
b)
<> i &
a =0_goto l <> i &
a >0_goto l <> i &
b := (
f,
a)
<> i & (
f,
b)
:= a <> i & (
f,
a)
:= b <> i &
f :=<0,...,0> a <> i );
end;
::
deftheorem defines
refers SCMFSA7B:def 1 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i refers a iff not for b being Int-Location
for l being Element of NAT
for f being FinSeq-Location holds
( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ) );