:: Another { \bf times } Macro Instruction
:: by Piotr Rudnicki
::
:: Received June 4, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users

begin

set D = Data-Locations SCM+FSA;

theorem Th1: :: SFMASTR2:1

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for b being Int-Location
for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not b in UsedIntLoc I holds
(IExec (I,p,s)) . b = (Initialized s) . b

proof end;

theorem :: SFMASTR2:2

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for f being FinSeq-Location
for I being Program of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not f in UsedInt*Loc I holds
(IExec (I,p,s)) . f = (Initialized s) . f

proof end;

theorem :: SFMASTR2:3

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for I being Program of SCM+FSA st ( ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) or I is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) & not a in UsedIntLoc I holds
(IExec (I,p,s)) . a = s . a

proof end;

theorem Th4: :: SFMASTR2:4

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_closed_on s,p iff I is_closed_on Initialized s,p )

proof end;

theorem Th5: :: SFMASTR2:5

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_closed_on s,p & I is_halting_on s,p iff ( I is_closed_on Initialized s,p & I is_halting_on Initialized s,p ) )

proof end;

theorem Th6: :: SFMASTR2:6

for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )

proof end;

theorem Th7: :: SFMASTR2:7

for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )

proof end;

begin

definition

let a be Int-Location ;
let I be Program of SCM+FSA;
func times* (a,I) -> Program of SCM+FSA equals :: SFMASTR2:def 1
while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))));
correctness
coherence
while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))))) is Program of SCM+FSA;
;

end;

:: deftheorem defines times* SFMASTR2:def 1 :
for a being Int-Location
for I being Program of SCM+FSA holds times* (a,I) = while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))));

definition

let a be Int-Location ;
let I be Program of SCM+FSA;
func times (a,I) -> Program of SCM+FSA equals :: SFMASTR2:def 2
((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (times* (a,I));
correctness
coherence
((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (times* (a,I)) is Program of SCM+FSA;
;

end;

:: deftheorem defines times SFMASTR2:def 2 :
for a being Int-Location
for I being Program of SCM+FSA holds times (a,I) = ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (times* (a,I));

notation

let a be Int-Location ;
let I be Program of SCM+FSA;
synonym a times I for times (a,I);

end;

theorem :: SFMASTR2:8

for b being Int-Location
for I being Program of SCM+FSA holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I))

proof end;

theorem :: SFMASTR2:9

for b being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (times (b,I)) = UsedInt*Loc I

proof end;

registration

let I be good Program of SCM+FSA;
let a be Int-Location ;
cluster times (a,I) -> good ;
coherence
times (a,I) is good ;

end;

definition

let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
let s be State of SCM+FSA;
let I be Program of SCM+FSA;
let a be Int-Location ;
func StepTimes (a,I,p,s) -> Function of NAT,(product the Object-Kind of SCM+FSA) equals :: SFMASTR2:def 3
StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))));
correctness
coherence
StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s)))) is Function of NAT,(product the Object-Kind of SCM+FSA);
;

end;

:: deftheorem defines StepTimes SFMASTR2:def 3 :
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialized s))));

theorem :: SFMASTR2:10

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for J being good Program of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1

proof end;

theorem :: SFMASTR2:11

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or not a is read-only ) holds
((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a

proof end;

theorem Th12: :: SFMASTR2:12

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 ) )

proof end;

theorem :: SFMASTR2:13

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for I being Program of SCM+FSA st ( s . (intloc 0) = 1 or not a is read-only ) holds
((StepTimes (a,I,p,s)) . 0) . a = s . a

proof end;

theorem :: SFMASTR2:14

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for f being FinSeq-Location
for I being Program of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f

proof end;

definition

let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
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: :: SFMASTR2:def 4
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 Th15: :: SFMASTR2:15

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for I being Program of SCM+FSA st I is parahalting holds
ProperTimesBody a,I,s,p

proof end;

theorem Th16: :: SFMASTR2:16

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p holds
for k being Element of NAT st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1

proof end;

theorem Th17: :: SFMASTR2:17

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for J being good Program of SCM+FSA st ( s . (intloc 0) = 1 or not a is read-only ) & ProperTimesBody a,J,s,p holds
for k being Element of NAT st k <= s . a holds
(((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a

proof end;

theorem :: SFMASTR2:18

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for J being good Program of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or not a is read-only ) holds
for k being Element of NAT st k >= s . a holds
( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 )

proof end;

theorem :: SFMASTR2:19

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being Int-Location
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
((StepTimes (a,I,p,s)) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations) = s | ((UsedIntLoc I) \/ FinSeq-Locations)

proof end;

theorem Th20: :: SFMASTR2:20

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)

proof end;

theorem :: SFMASTR2:21

for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 not a is read-only ) 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)

proof end;

theorem :: SFMASTR2:22

canceled;

theorem :: SFMASTR2:23

canceled;

theorem :: SFMASTR2:24

canceled;

begin

definition

let d be read-write Int-Location ;
func triv-times d -> Program of SCM+FSA equals :: SFMASTR2:def 5
times (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))));
correctness
coherence
times (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))) is Program of SCM+FSA;
;

end;

:: deftheorem defines triv-times SFMASTR2:def 5 :
for d being read-write Int-Location holds triv-times d = times (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))));

theorem :: SFMASTR2:25

canceled;

theorem :: SFMASTR2:26

canceled;

begin

definition

let N, result be Int-Location ;
func Fib-macro (N,result) -> Program of SCM+FSA equals :: SFMASTR2:def 6
(((((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}))))))));