begin
set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At (insloc 0 );
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem defines times SFMASTR2:def 1 :
theorem Th8:
theorem
definition
let s be
State of ;
let I be
Program of ;
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),(Initialize 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),(Initialize s)) is Function of NAT , product the Object-Kind of SCM+FSA ;
;
end;
:: deftheorem defines StepTimes SFMASTR2:def 2 :
theorem Th10:
theorem Th11:
theorem Th12:
for
s being
State of
for
a being
Int-Location for
J being
good Program of
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 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
s being
State of
for
a being
Int-Location for
J being
good Program of
for
k being
Element of
NAT st
((StepTimes a,J,s) . k) . (intloc 0 ) = 1 &
J is_halting_on Initialize ((StepTimes a,J,s) . k) &
J is_closed_on Initialize ((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 :
theorem
theorem
begin
definition
let N,
result be
Int-Location ;
func Fib-macro N,
result -> Program of
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 ;
;
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