begin
set A = NAT ;
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
Lm1:
for s being State of st IC s = insloc 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 st IC s = insloc 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 s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )
Lm5:
for s being State of
for c0 being Element of NAT st IC s = insloc 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 . (insloc (c0 + c)) ) holds
for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Computation s,i) = insloc (c0 + i)
Lm6:
for s being State of st IC s = insloc 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 (Computation s,i) = insloc i
Lm7:
for s being State of st IC s = insloc 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 ;
let a be
Int-Location ;
pred i does_not_refer a means
for
b being
Int-Location for
l being
Instruction-Location of
SCM+FSA 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 does_not_refer SCMFSA7B:def 1 :
for
i being
Instruction of
for
a being
Int-Location holds
(
i does_not_refer a iff for
b being
Int-Location for
l being
Instruction-Location of
SCM+FSA 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 does_not_refer SCMFSA7B:def 2 :
:: deftheorem Def3 defines does_not_destroy SCMFSA7B:def 3 :
:: deftheorem Def4 defines does_not_destroy SCMFSA7B:def 4 :
:: deftheorem Def5 defines good SCMFSA7B:def 5 :
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 :
:: deftheorem Def8 defines is_halting_on SCMFSA7B:def 8 :
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
Lm8:
Stop SCM+FSA is parahalting
theorem Th29:
theorem Th30: