:: On the Composition of non-parahalting Macro Instructions
:: by Piotr Rudnicki
::
:: Received June 3, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: deftheorem Def1 defines good SFMASTR1:def 1 :
theorem Th1: :: SFMASTR1:1
set D = Int-Locations \/ FinSeq-Locations ;
theorem Th2: :: SFMASTR1:2
theorem Th3: :: SFMASTR1:3
theorem Th4: :: SFMASTR1:4
theorem Th5: :: SFMASTR1:5
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 (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is good implies (Result s) . (intloc 0 ) = 1 ) )
theorem Th6: :: SFMASTR1:6
theorem Th7: :: SFMASTR1:7
theorem Th8: :: SFMASTR1:8
theorem Th9: :: SFMASTR1:9
theorem :: SFMASTR1:10
theorem Th11: :: SFMASTR1:11
theorem Th12: :: SFMASTR1:12
theorem Th13: :: SFMASTR1:13
theorem :: SFMASTR1:14
theorem Th15: :: SFMASTR1:15
theorem Th16: :: SFMASTR1:16
theorem :: SFMASTR1:17
definition
let d be
Int-Location ;
:: original: {redefine func {d} -> Subset of
Int-Locations ;
coherence
{d} is Subset of Int-Locations
let e be
Int-Location ;
:: original: {redefine func {d,e} -> Subset of
Int-Locations ;
coherence
{d,e} is Subset of Int-Locations
let f be
Int-Location ;
:: original: {redefine func {d,e,f} -> Subset of
Int-Locations ;
coherence
{d,e,f} is Subset of Int-Locations
let g be
Int-Location ;
:: original: {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 :
theorem Th18: :: SFMASTR1:18
theorem Th19: :: SFMASTR1:19
theorem Th20: :: SFMASTR1:20
:: deftheorem defines -thRWNotIn SFMASTR1:def 3 :
theorem Th21: :: SFMASTR1:21
theorem Th22: :: SFMASTR1:22
:: deftheorem defines -thNotUsed SFMASTR1:def 4 :
theorem Th23: :: SFMASTR1:23
definition
let N,
result be
Int-Location ;
func Fib_macro N,
result -> Program of
SCM+FSA equals :: SFMASTR1:def 5
((((((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 :: SFMASTR1:24