begin
set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At 0 ,SCM+FSA ;
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem defines times SFMASTR2:def 1 :
for a being Int-Location
for I being Program of SCM+FSA holds times a,I = ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0 ))));
theorem Th8:
theorem
definition
let s be
State of
SCM+FSA ;
let I be
Program of
SCM+FSA ;
let a be
Int-Location ;
func StepTimes a,
I,
s -> Function of
NAT ,
(product the Object-Kind of SCM+FSA ) equals
StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),
(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0 ))),
(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s));
correctness
coherence
StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)) is Function of NAT ,(product the Object-Kind of SCM+FSA );
;
end;
:: deftheorem defines StepTimes SFMASTR2:def 2 :
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location holds StepTimes a,I,s = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s));
theorem Th10:
theorem Th11:
theorem Th12:
for
s being
State of
SCM+FSA for
a being
Int-Location for
J being
good Program of
SCM+FSA for
k being
Element of
NAT st
((StepTimes a,J,s) . k) . (intloc 0 ) = 1 &
J is_closed_on (StepTimes a,J,s) . k &
J is_halting_on (StepTimes a,J,s) . k holds
(
((StepTimes a,J,s) . (k + 1)) . (intloc 0 ) = 1 & (
((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies
((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) )
theorem Th13:
theorem
:: deftheorem Def3 defines ProperTimesBody SFMASTR2:def 3 :
for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA holds
( ProperTimesBody a,I,s iff for k being Element of NAT st k < s . a holds
( I is_closed_on (StepTimes a,I,s) . k & I is_halting_on (StepTimes a,I,s) . k ) );
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
s being
State of
SCM+FSA for
a being
Int-Location for
J being
good Program of
SCM+FSA for
k being
Element of
NAT st
((StepTimes a,J,s) . k) . (intloc 0 ) = 1 &
J is_halting_on Initialized ((StepTimes a,J,s) . k) &
J is_closed_on Initialized ((StepTimes a,J,s) . k) &
((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes a,J,s) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations ) = (IExec J,((StepTimes a,J,s) . k)) | ((UsedIntLoc J) \/ FinSeq-Locations )
theorem Th21:
theorem
theorem Th23:
theorem Th24:
begin
:: deftheorem defines triv-times SFMASTR2:def 4 :
for d being read-write Int-Location holds triv-times d = times d,((while=0 d,(Macro (d := d))) ';' (SubFrom d,(intloc 0 )));
theorem
theorem
begin
definition
let N,
result be
Int-Location ;
func Fib-macro N,
result -> Program of
SCM+FSA equals
(((((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))));
correctness
coherence
(((((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))))) is Program of SCM+FSA ;
;
end;
:: deftheorem defines Fib-macro SFMASTR2:def 5 :
for N, result being Int-Location holds Fib-macro N,result = (((((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))));
theorem