:: Another { \bf times } Macro Instruction
:: by Piotr Rudnicki
::
:: Received June 4, 1998
:: Copyright (c) 1998 Association of Mizar Users
set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At (insloc 0 );
set IL = NAT ;
theorem Th1: :: SFMASTR2:1
theorem :: SFMASTR2:2
theorem Th3: :: SFMASTR2:3
theorem Th4: :: SFMASTR2:4
theorem Th5: :: SFMASTR2:5
theorem Th6: :: SFMASTR2:6
theorem Th7: :: SFMASTR2:7
:: deftheorem defines times SFMASTR2:def 1 :
theorem Th8: :: SFMASTR2:8
theorem :: SFMASTR2:9
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 :: SFMASTR2:def 2
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: :: SFMASTR2:10
theorem Th11: :: SFMASTR2:11
theorem Th12: :: SFMASTR2:12
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: :: SFMASTR2:13
theorem :: SFMASTR2:14
:: deftheorem Def3 defines ProperTimesBody SFMASTR2:def 3 :
theorem Th15: :: SFMASTR2:15
theorem Th16: :: SFMASTR2:16
theorem Th17: :: SFMASTR2:17
theorem Th18: :: SFMASTR2:18
theorem Th19: :: SFMASTR2:19
theorem Th20: :: SFMASTR2:20
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 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: :: SFMASTR2:21
theorem :: SFMASTR2:22
theorem Th23: :: SFMASTR2:23
theorem Th24: :: SFMASTR2:24
:: deftheorem defines triv-times SFMASTR2:def 4 :
theorem :: SFMASTR2:25
theorem :: SFMASTR2:26
definition
let N,
result be
Int-Location ;
func Fib-macro N,
result -> Program of
SCM+FSA equals :: SFMASTR2:def 5
(((((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 :: SFMASTR2:27