:: On the Composition of non-parahalting Macro Instructions :: by Piotr Rudnicki :: :: Received June 3, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin definition let i be Instruction of SCM+FSA; attri is good means :Def1: :: SFMASTR1:def 1 Macro i is good ; end; :: deftheorem Def1 defines good SFMASTR1:def_1_:_ for i being Instruction of SCM+FSA holds ( i is good iff Macro i is good ); registration let a be read-write Int-Location; let b be Int-Location; clustera := b -> good ; coherence a := b is good proofend; cluster AddTo (a,b) -> good ; coherence AddTo (a,b) is good proofend; cluster SubFrom (a,b) -> good ; coherence SubFrom (a,b) is good proofend; cluster MultBy (a,b) -> good ; coherence MultBy (a,b) is good proofend; end; registration cluster parahalting with_explicit_jumps IC-relocable good for Element of the InstructionsF of SCM+FSA; existence ex b1 being Instruction of SCM+FSA st ( b1 is good & b1 is parahalting ) proofend; end; registration let a, b be read-write Int-Location; cluster Divide (a,b) -> good ; coherence Divide (a,b) is good proofend; end; registration let l be Element of NAT ; cluster goto l -> good ; coherence goto l is good proofend; end; registration let a be Int-Location; let l be Element of NAT ; clustera =0_goto l -> good ; coherence a =0_goto l is good proofend; clustera >0_goto l -> good ; coherence a >0_goto l is good proofend; end; registration let a be Int-Location; let f be FinSeq-Location ; let b be read-write Int-Location; clusterb := (f,a) -> good ; coherence b := (f,a) is good proofend; end; registration let f be FinSeq-Location ; let b be read-write Int-Location; clusterb :=len f -> good ; coherence b :=len f is good proofend; end; registration let f be FinSeq-Location ; let a be Int-Location; clusterf :=<0,...,0> a -> good ; coherence f :=<0,...,0> a is good proofend; let b be Int-Location; cluster(f,a) := b -> good ; coherence (f,a) := b is good proofend; end; registration let i be good Instruction of SCM+FSA; cluster Macro i -> good ; coherence Macro i is good by Def1; end; registration let i, j be good Instruction of SCM+FSA; clusteri ";" j -> good ; coherence i ";" j is good ; end; registration let i be good Instruction of SCM+FSA; let I be good Program of SCM+FSA; clusteri ";" I -> good ; coherence i ";" I is good ; clusterI ";" i -> good ; coherence I ";" i is good ; end; registration let a, b be read-write Int-Location; cluster swap (a,b) -> good ; coherence swap (a,b) is good proofend; end; registration let I be good Program of SCM+FSA; let a be read-write Int-Location; cluster Times (a,I) -> good ; coherence Times (a,I) is good proofend; end; theorem Th1: :: SFMASTR1:1 for a being Int-Location for I being Program of SCM+FSA st not a in UsedIntLoc I holds not I destroys a proofend; begin set D = Data-Locations ; set SAt = Start-At (0,SCM+FSA); theorem Th2: :: SFMASTR1:2 for P being Instruction-Sequence of SCM+FSA for S being State of SCM+FSA for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds I ";" J is_closed_on Initialized S,P proofend; theorem Th3: :: SFMASTR1:3 for P being Instruction-Sequence of SCM+FSA for S being State of SCM+FSA for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds I ";" J is_halting_on Initialized S,P proofend; theorem Th4: :: SFMASTR1:4 for p being Instruction-Sequence of SCM+FSA for I, J being Program of SCM+FSA for s being 0 -started State of SCM+FSA st I is_closed_on s,p & I c= p & p halts_on s holds for m being Element of NAT st m <= LifeSpan (p,s) holds Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m) proofend; Lm1: for p being Instruction-Sequence of SCM+FSA 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,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds ( IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I & DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) & ( J is good implies (Result (p,s)) . (intloc 0) = 1 ) ) proofend; theorem Th5: :: SFMASTR1:5 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) proofend; theorem Th6: :: SFMASTR1:6 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds IExec ((Ig ";" J),p,s) = (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA)) proofend; theorem Th7: :: SFMASTR1:7 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for Ig being good Program of SCM+FSA for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds (IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a proofend; theorem Th8: :: SFMASTR1:8 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for Ig being good Program of SCM+FSA for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds (IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f proofend; theorem :: SFMASTR1:9 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s)))) proofend; theorem Th10: :: SFMASTR1:10 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) proofend; theorem Th11: :: SFMASTR1:11 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for Ig being good Program of SCM+FSA for j being parahalting Instruction of SCM+FSA for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds (IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a proofend; theorem Th12: :: SFMASTR1:12 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for Ig being good Program of SCM+FSA for j being parahalting Instruction of SCM+FSA for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds (IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f proofend; theorem :: SFMASTR1:13 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for Ig being good Program of SCM+FSA for j being parahalting Instruction of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s)))) proofend; theorem Th14: :: SFMASTR1:14 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for i being parahalting good Instruction of SCM+FSA for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a proofend; theorem Th15: :: SFMASTR1:15 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for i being parahalting good Instruction of SCM+FSA for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f proofend; theorem :: SFMASTR1:16 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for J being Program of SCM+FSA for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) proofend; begin definition canceled; canceled; let n be Element of NAT ; let p be preProgram of SCM+FSA; funcn -thNotUsed p -> Int-Location equals :: SFMASTR1:def 4 n -thRWNotIn (UsedIntLoc p); correctness coherence n -thRWNotIn (UsedIntLoc p) is Int-Location; ; end; :: deftheorem SFMASTR1:def_2_:_ canceled; :: deftheorem SFMASTR1:def_3_:_ canceled; :: deftheorem defines -thNotUsed SFMASTR1:def_4_:_ for n being Element of NAT for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedIntLoc p); notation let n be Element of NAT ; let p be preProgram of SCM+FSA; synonym n -stNotUsed p for n -thNotUsed p; synonym n -ndNotUsed p for n -thNotUsed p; synonym n -rdNotUsed p for n -thNotUsed p; end; registration let n be Element of NAT ; let p be preProgram of SCM+FSA; clustern -thNotUsed p -> read-write ; coherence not n -thNotUsed p is read-only ; end; begin theorem :: SFMASTR1:17 canceled; theorem :: SFMASTR1:18 canceled; theorem :: SFMASTR1:19 canceled; theorem :: SFMASTR1:20 canceled; theorem :: SFMASTR1:21 canceled; theorem Th22: :: SFMASTR1:22 for a, b being Int-Location holds ( a in UsedIntLoc (swap (a,b)) & b in UsedIntLoc (swap (a,b)) ) proofend; 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})))))); :: set next = 1-stRWNotIn {N, result}; :: local variable :: set aux = 1-stRWNotIn UsedIntLoc swap(result, next); :: for the control variable of Times, must not be changed by swap :: set N_save = 2-ndRWNotIn UsedIntLoc swap(result, next); :: for saving and restoring N :: - requires: N <> result :: - does not change N :: - note: Times allocates no memory theorem :: SFMASTR1:23 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for N, result being read-write Int-Location st N <> result holds for n being Element of NAT st n = s . N holds ( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N ) proofend;