begin
set D = Data-Locations ;
begin
theorem Th12:
for
s being
State of
SCM+FSA for
p being
Instruction-Sequence 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,p,s)) . k) . (intloc 0) = 1 &
J is_closed_on (StepTimes (a,J,p,s)) . k,
p +* (times* (a,J)) &
J is_halting_on (StepTimes (a,J,p,s)) . k,
p +* (times* (a,J)) holds
(
((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & (
((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies
((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) )
definition
let p be
Instruction-Sequence of
SCM+FSA;
let s be
State of
SCM+FSA;
let a be
Int-Location;
let I be
Program of
SCM+FSA;
pred ProperTimesBody a,
I,
s,
p means :
Def4:
for
k being
Element of
NAT st
k < s . a holds
(
I is_closed_on (StepTimes (a,I,p,s)) . k,
p +* (times* (a,I)) &
I is_halting_on (StepTimes (a,I,p,s)) . k,
p +* (times* (a,I)) );
end;
::
deftheorem Def4 defines
ProperTimesBody SFMASTR2:def 4 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA holds
( ProperTimesBody a,I,s,p iff for k being Element of NAT st k < s . a holds
( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) ) );
theorem Th20:
for
s being
State of
SCM+FSA for
p being
Instruction-Sequence 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,p,s)) . k) . (intloc 0) = 1 &
J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),
p +* (times* (a,J)) &
J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),
p +* (times* (a,J)) &
((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations)
theorem Th21:
for
s being
State of
SCM+FSA for
p being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
J being
good Program of
SCM+FSA for
k being
Element of
NAT st (
ProperTimesBody a,
J,
s,
p or
J is
parahalting ) &
k < s . a & (
s . (intloc 0) = 1 or
a is
read-write ) holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedIntLoc J) \/ FinSeq-Locations)
begin
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 6 :
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}))))))));