begin
:: deftheorem Def1 defines good SFMASTR1:def 1 :
for i being Instruction of SCM+FSA holds
( i is good iff Macro i is good );
theorem Th1:
begin
set D = Int-Locations \/ FinSeq-Locations;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
Lm1:
for I being good Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s & J is_halting_on IExec (I,s) & I is_closed_on s & J is_closed_on IExec (I,s) & Initialized (I ';' J) c= s holds
( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
begin
definition
let d be
Int-Location ;
{redefine func {d} -> Subset of
Int-Locations;
coherence
{d} is Subset of Int-Locations
let e be
Int-Location ;
{redefine func {d,e} -> Subset of
Int-Locations;
coherence
{d,e} is Subset of Int-Locations
let f be
Int-Location ;
{redefine func {d,e,f} -> Subset of
Int-Locations;
coherence
{d,e,f} is Subset of Int-Locations
let g be
Int-Location ;
{redefine func {d,e,f,g} -> Subset of
Int-Locations;
coherence
{d,e,f,g} is Subset of Int-Locations
end;
:: deftheorem Def2 defines RWNotIn-seq SFMASTR1:def 2 :
for L being finite Subset of Int-Locations
for b2 being Function of NAT,(bool NAT) holds
( b2 = RWNotIn-seq L iff ( b2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds not b2 . i is finite ) ) );
theorem Th18:
theorem Th19:
theorem Th20:
:: deftheorem defines -thRWNotIn SFMASTR1:def 3 :
for n being Element of NAT
for L being finite Subset of Int-Locations holds n -thRWNotIn L = intloc (min ((RWNotIn-seq L) . n));
theorem Th21:
theorem Th22:
:: deftheorem defines -thNotUsed SFMASTR1:def 4 :
for n being Element of NAT
for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedIntLoc p);
begin
theorem Th23:
definition
let N,
result be
Int-Location ;
func Fib_macro (
N,
result)
-> Program of
SCM+FSA equals
((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) ';' (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
correctness
coherence
((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) ';' (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is Program of SCM+FSA;
;
end;
:: deftheorem defines Fib_macro SFMASTR1:def 5 :
for N, result being Int-Location holds Fib_macro (N,result) = ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) ';' (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
theorem