begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
set D = Int-Locations \/ FinSeq-Locations;
set SAt = Start-At (0,SCM+FSA);
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
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)))
theorem
theorem
definition
let p be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
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 Object-Kind 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 Object-Kind 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 Th19:
theorem Th20:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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 Th21:
theorem Th22:
theorem Th23:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
I is_closed_on s,
p &
I is_halting_on s,
p &
s . a = 0 holds
DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I))))))
theorem Th24:
theorem Th25:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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
theorem
for
p1,
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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 the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
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))),(s +* (Initialize (while=0 (a,I)))),(LifeSpan ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))))))) = 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))),(s +* (Initialize (while=0 (a,I)))),(LifeSpan ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))))))) = 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))),(s +* (Initialize (while=0 (a,I)))),(LifeSpan ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))))))) = 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))),(s +* (Initialize (while=0 (a,I)))),(LifeSpan ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) holds
b1 = b2
end;
:: deftheorem Def3 defines ExitsAtWhile=0 SCMFSA9A:def 3 :
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))),(s +* (Initialize (while=0 (a,I)))),(LifeSpan ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) );
theorem
theorem
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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)))
theorem
theorem
definition
let p be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
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 Object-Kind 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 Object-Kind 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 Th32:
theorem Th33:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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 Th34:
theorem Th35:
theorem Th36:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
I is_closed_on s,
p &
I is_halting_on s,
p &
s . a > 0 holds
DataPart (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I))))))
theorem Th37:
theorem Th38:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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 Th39:
theorem Th40:
for
p1,
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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 the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
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))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = 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))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = 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))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = 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))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) holds
b1 = b2
end;
:: deftheorem Def6 defines ExitsAtWhile>0 SCMFSA9A:def 6 :
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) );
theorem
theorem Th42:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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))))
theorem Th43:
theorem
Lm7:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 Th45:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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) )
:: deftheorem Def7 defines on_data_only SCMFSA9A:def 7 :
for f being Function of (product the Object-Kind of SCM+FSA),NAT holds
( f is on_data_only iff for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
f . s1 = f . s2 );
theorem Th46:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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 Object-Kind 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 the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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})))))))));
theorem