begin
set A = NAT ;
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
Lm1:
for s being State of SCM+FSA st IC s = 0 holds
for a being Int-Location
for k being Integer st a := k c= s holds
ProgramPart s halts_on s
theorem
Lm2:
for p1, p2, p3, p4 being FinSequence holds ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4)
Lm3:
for p1, p2, p3 being FinSequence holds
( ((len p1) + (len p2)) + (len p3) = len ((p1 ^ p2) ^ p3) & ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )
Lm4:
for s being State of SCM+FSA st IC s = 0 & s . (intloc 0 ) = 1 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
( ProgramPart s halts_on s & (Result (ProgramPart s),s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (ProgramPart s),s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (ProgramPart s),s) . g = s . g ) )
Lm5:
for s being State of SCM+FSA
for c0 being Element of NAT st IC s = c0 holds
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 + 1) = s . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Comput (ProgramPart s),s,i) = c0 + i
Lm6:
for s being State of SCM+FSA st IC s = 0 holds
for a being Int-Location
for k being Integer st Load (aSeq a,k) c= s holds
for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Comput (ProgramPart s),s,i) = i
Lm7:
for s being State of SCM+FSA st IC s = 0 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
ProgramPart s halts_on s
theorem
definition
let i be
Instruction of
SCM+FSA ;
let a be
Int-Location ;
pred i refersrefer 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 refersrefer SCMFSA7B:def 1 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i refersrefer 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 ) );
:: deftheorem defines refersrefer SCMFSA7B:def 2 :
for I being preProgram of SCM+FSA
for a being Int-Location holds
( I refersrefer a iff ex i being Instruction of SCM+FSA st
( i in rng I & i refersrefer a ) );
:: deftheorem Def3 defines destroysdestroy SCMFSA7B:def 3 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i destroysdestroy a iff not for b being Int-Location
for f being FinSeq-Location holds
( a := b <> i & AddTo a,b <> i & SubFrom a,b <> i & MultBy a,b <> i & Divide a,b <> i & Divide b,a <> i & a := f,b <> i & a :=len f <> i ) );
:: deftheorem Def4 defines destroysdestroy SCMFSA7B:def 4 :
for I being FinPartState of SCM+FSA
for a being Int-Location holds
( I destroysdestroy a iff ex i being Instruction of SCM+FSA st
( i in rng I & i destroysdestroy a ) );
:: deftheorem Def5 defines good SCMFSA7B:def 5 :
for I being FinPartState of SCM+FSA holds
( I is good iff not I destroysdestroy intloc 0 );
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem SCMFSA7B:def 6 :
canceled;
:: deftheorem Def7 defines is_closed_on SCMFSA7B:def 7 :
for I being FinPartState of SCM+FSA
for s being State of SCM+FSA holds
( I is_closed_on s iff for k being Element of NAT holds IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I );
:: deftheorem Def8 defines is_halting_on SCMFSA7B:def 8 :
for I being FinPartState of SCM+FSA
for s being State of SCM+FSA holds
( I is_halting_on s iff ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA )) );
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem
canceled;
theorem Th29:
theorem Th30: