begin
set D = Int-Locations \/ FinSeq-Locations;
set SAt = Start-At (0,SCM+FSA);
begin
Lm1:
for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) & (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
Lm2:
for a being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = UsedIntLoc ((if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
Lm3:
for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = UsedInt*Loc ((if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
definition
let p be
Instruction-Sequence of
SCM+FSA;
let s be
State of
SCM+FSA;
let a be
read-write Int-Location;
let I be
Program of
SCM+FSA;
pred ProperBodyWhile=0 a,
I,
s,
p means :
Def1:
for
k being
Element of
NAT st
((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds
(
I is_closed_on (StepWhile=0 (a,I,p,s)) . k,
p +* (while=0 (a,I)) &
I is_halting_on (StepWhile=0 (a,I,p,s)) . k,
p +* (while=0 (a,I)) );
pred WithVariantWhile=0 a,
I,
s,
p means :
Def2:
ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Element of
NAT holds
(
f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or
((StepWhile=0 (a,I,p,s)) . k) . a <> 0 );
end;
::
deftheorem Def1 defines
ProperBodyWhile=0 SCMFSA9A:def 1 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA holds
( ProperBodyWhile=0 a,I,s,p iff for k being Element of NAT st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds
( I is_closed_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) ) );
::
deftheorem Def2 defines
WithVariantWhile=0 SCMFSA9A:def 2 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA holds
( WithVariantWhile=0 a,I,s,p iff ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Element of NAT holds
( f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 ) );
theorem Th14:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
ProperBodyWhile=0 a,
I,
s,
p &
WithVariantWhile=0 a,
I,
s,
p holds
(
while=0 (
a,
I)
is_halting_on s,
p &
while=0 (
a,
I)
is_closed_on s,
p )
theorem Th19:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA for
k being
Element of
NAT st ( (
I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),
p +* (while=0 (a,I)) &
I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),
p +* (while=0 (a,I)) ) or
I is
parahalting ) &
((StepWhile=0 (a,I,p,s)) . k) . a = 0 &
((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))
theorem
for
p1,
p2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
ProperBodyWhile=0 a,
I,
s1,
p1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
definition
let p be
Instruction-Sequence of
SCM+FSA;
let s be
State of
SCM+FSA;
let a be
read-write Int-Location;
let I be
Program of
SCM+FSA;
assume that A1:
(
ProperBodyWhile=0 a,
I,
s,
p or
I is
parahalting )
and A2:
WithVariantWhile=0 a,
I,
s,
p
;
func ExitsAtWhile=0 (
a,
I,
p,
s)
-> Element of
NAT means :
Def3:
ex
k being
Element of
NAT st
(
it = k &
((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for
i being
Element of
NAT st
((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) &
DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) );
existence
ex b1, k being Element of NAT st
( b1 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) )
uniqueness
for b1, b2 being Element of NAT st ex k being Element of NAT st
( b1 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) & ex k being Element of NAT st
( b2 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) holds
b1 = b2
end;
::
deftheorem Def3 defines
ExitsAtWhile=0 SCMFSA9A:def 3 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) & WithVariantWhile=0 a,I,s,p holds
for b5 being Element of NAT holds
( b5 = ExitsAtWhile=0 (a,I,p,s) iff ex k being Element of NAT st
( b5 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) );
theorem
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st (
ProperBodyWhile=0 a,
I,
Initialized s,
p or
I is
parahalting ) &
WithVariantWhile=0 a,
I,
Initialized s,
p holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
begin
Lm4:
for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) & (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
Lm5:
for a being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = UsedIntLoc ((if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
Lm6:
for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = UsedInt*Loc ((if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
definition
let p be
Instruction-Sequence of
SCM+FSA;
let s be
State of
SCM+FSA;
let a be
read-write Int-Location;
let I be
Program of
SCM+FSA;
pred ProperBodyWhile>0 a,
I,
s,
p means :
Def4:
for
k being
Element of
NAT st
((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds
(
I is_closed_on (StepWhile>0 (a,I,p,s)) . k,
p +* (while>0 (a,I)) &
I is_halting_on (StepWhile>0 (a,I,p,s)) . k,
p +* (while>0 (a,I)) );
pred WithVariantWhile>0 a,
I,
s,
p means :
Def5:
ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Element of
NAT holds
(
f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or
((StepWhile>0 (a,I,p,s)) . k) . a <= 0 );
end;
::
deftheorem Def4 defines
ProperBodyWhile>0 SCMFSA9A:def 4 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA holds
( ProperBodyWhile>0 a,I,s,p iff for k being Element of NAT st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds
( I is_closed_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) ) );
::
deftheorem Def5 defines
WithVariantWhile>0 SCMFSA9A:def 5 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA holds
( WithVariantWhile>0 a,I,s,p iff ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Element of NAT holds
( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ) );
theorem Th27:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
ProperBodyWhile>0 a,
I,
s,
p &
WithVariantWhile>0 a,
I,
s,
p holds
(
while>0 (
a,
I)
is_halting_on s,
p &
while>0 (
a,
I)
is_closed_on s,
p )
theorem Th32:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA for
k being
Element of
NAT st ( (
I is_halting_on Initialized ((StepWhile>0 (a,I,p,s)) . k),
p +* (while>0 (a,I)) &
I is_closed_on Initialized ((StepWhile>0 (a,I,p,s)) . k),
p +* (while>0 (a,I)) ) or
I is
parahalting ) &
((StepWhile>0 (a,I,p,s)) . k) . a > 0 &
((StepWhile>0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . k)))
theorem Th34:
for
p1,
p2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
ProperBodyWhile>0 a,
I,
s1,
p1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
definition
let p be
Instruction-Sequence of
SCM+FSA;
let s be
State of
SCM+FSA;
let a be
read-write Int-Location;
let I be
Program of
SCM+FSA;
assume that A1:
(
ProperBodyWhile>0 a,
I,
s,
p or
I is
parahalting )
and A2:
WithVariantWhile>0 a,
I,
s,
p
;
func ExitsAtWhile>0 (
a,
I,
p,
s)
-> Element of
NAT means :
Def6:
ex
k being
Element of
NAT st
(
it = k &
((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for
i being
Element of
NAT st
((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) &
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) );
existence
ex b1, k being Element of NAT st
( b1 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )
uniqueness
for b1, b2 being Element of NAT st ex k being Element of NAT st
( b1 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) & ex k being Element of NAT st
( b2 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) holds
b1 = b2
end;
::
deftheorem Def6 defines
ExitsAtWhile>0 SCMFSA9A:def 6 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) & WithVariantWhile>0 a,I,s,p holds
for b5 being Element of NAT holds
( b5 = ExitsAtWhile>0 (a,I,p,s) iff ex k being Element of NAT st
( b5 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) );
theorem Th36:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st (
ProperBodyWhile>0 a,
I,
Initialized s,
p or
I is
parahalting ) &
WithVariantWhile>0 a,
I,
Initialized s,
p holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart ((StepWhile>0 (a,I,p,(Initialized s))) . (ExitsAtWhile>0 (a,I,p,(Initialized s))))
Lm7:
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_closed_on s,p iff I is_closed_on Initialized s,p )
Lm8:
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) )
theorem Th39:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
Ig being
good Program of
SCM+FSA st
s . (intloc 0) = 1 &
ProperBodyWhile>0 a,
Ig,
s,
p &
WithVariantWhile>0 a,
Ig,
s,
p holds
for
i,
j being
Element of
NAT st
i <> j &
i <= ExitsAtWhile>0 (
a,
Ig,
p,
s) &
j <= ExitsAtWhile>0 (
a,
Ig,
p,
s) holds
(
(StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j &
DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
definition
canceled;
end;
theorem Th40:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
Ig being
good Program of
SCM+FSA st
s . (intloc 0) = 1 &
ProperBodyWhile>0 a,
Ig,
s,
p &
WithVariantWhile>0 a,
Ig,
s,
p holds
ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
(
f is
on_data_only & ( for
k being
Element of
NAT holds
(
f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or
((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) ) )
theorem
for
p1,
p2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
a being
read-write Int-Location for
Ig being
good Program of
SCM+FSA st
s1 . (intloc 0) = 1 &
DataPart s1 = DataPart s2 &
ProperBodyWhile>0 a,
Ig,
s1,
p1 &
WithVariantWhile>0 a,
Ig,
s1,
p1 holds
WithVariantWhile>0 a,
Ig,
s2,
p2
begin
definition
let N,
result be
Int-Location;
func Fusc_macro (
N,
result)
-> Program of
SCM+FSA equals
(((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)) ";" (while>0 ((2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" (if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))))));
correctness
coherence
(((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)) ";" (while>0 ((2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" (if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result}))))))))) is Program of SCM+FSA;
;
end;
::
deftheorem defines
Fusc_macro SCMFSA9A:def 8 :
for N, result being Int-Location holds Fusc_macro (N,result) = (((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)) ";" (while>0 ((2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" (if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))))));
:: set aux = 2-ndRWNotIn {N, result};
:: set rem2 = 3-rdRWNotIn {N, result};
:: while and if do not allocate memory, no need to save anything