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

environ

vocabularies HIDDEN, NUMBERS, FSM_1, SCMFSA_2, SF_MASTR, AMI_1, SCMFSA7B, SUBSET_1, XBOOLE_0, CARD_1, SCMFSA6B, FUNCT_1, FUNCT_4, SCMFSA6A, TARSKI, RELAT_1, ARYTM_3, GRAPHSP, MSUALG_1, SFMASTR1, SCMFSA_9, AMI_3, CARD_3, XXREAL_0, ARYTM_1, SCMFSA9A, COMPLEX1, SFMASTR2, NAT_1, EXTPRO_1, SCMFSA6C, COMPOS_1, MEMSTR_0, AMISTD_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_2, XXREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, PBOOLE, CARD_3, FUNCOP_1, STRUCT_0, MEMSTR_0, AMISTD_1, COMPOS_1, EXTPRO_1, SCMFSA_2, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA_9, SFMASTR1, SCMFSA9A, NAT_1, SCMFSA_M, SCMFSA_X;
definitions SCMFSA9A;
theorems TARSKI, ZFMISC_1, ABSVALUE, NAT_1, INT_1, FUNCT_4, SCMFSA_2, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8B, SCMFSA8C, SCMFSA_9, SFMASTR1, SCMFSA9A, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, EXTPRO_1, MEMSTR_0, CARD_3, SCMFSA_M, ORDINAL1, AFINSQ_1, AMISTD_1;
schemes FUNCT_2, NAT_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA_9, SFMASTR1, COMPOS_1, FUNCT_4, MEMSTR_0, AMI_3, SCMFSA_M, SCMFSA6A, SCMFSA8C, SCMFSA9A, SCMFSA10, SCMFSA_X, COMPOS_2;
constructors HIDDEN, XXREAL_0, INT_2, PRE_FF, SCMFSA6A, SCMFSA6B, SCMFSA6C, SCMFSA_9, SFMASTR1, SCMFSA9A, RELSET_1, PRE_POLY, PBOOLE, SCMFSA8A, SCMFSA7B, AMISTD_2, AMISTD_1, SCMFSA_7, FUNCT_4, MEMSTR_0, SCMFSA_1, SCMFSA_M, SF_MASTR, SCMFSA_X, COMPOS_2;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SUBSET_1, SCMFSA6A;
expansions SCMFSA9A;


set D = Data-Locations ;

theorem Th1: :: SFMASTR2:1
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for b being Int-Location
for I being really-closed Program of st I is_halting_on Initialized s,p & not b in UsedILoc 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 Instruction-Sequence of SCM+FSA
for f being FinSeq-Location
for I being really-closed Program of st I is_halting_on Initialized s,p & not f in UsedI*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 Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed Program of st ( I is_halting_on Initialized s,p or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedILoc I holds
(IExec (I,p,s)) . a = s . a
proof end;

theorem :: SFMASTR2:4
canceled;

theorem :: SFMASTR2:5
canceled;

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

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

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

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

registration
let a be Int-Location;
let I be really-closed MacroInstruction of SCM+FSA ;
cluster times* (a,I) -> really-closed ;
coherence
times* (a,I) is really-closed ;
end;

registration
let a be Int-Location;
let I be really-closed MacroInstruction of SCM+FSA ;
cluster times (a,I) -> really-closed ;
coherence
times (a,I) is really-closed ;
end;

theorem :: SFMASTR2:6
canceled;

theorem :: SFMASTR2:7
canceled;

::$CT 2
theorem :: SFMASTR2:8
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds {b} \/ (UsedILoc I) c= UsedILoc (times (b,I))
proof end;

theorem :: SFMASTR2:9
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (times (b,I)) = UsedI*Loc I
proof end;

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

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let I be MacroInstruction of SCM+FSA ;
let a be Int-Location;
func StepTimes (a,I,p,s) -> sequence of (product (the_Values_of SCM+FSA)) equals :: SFMASTR2:def 3
 StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));
correctness
coherence
StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s)))) is sequence of (product (the_Values_of SCM+FSA));
;
end;

:: deftheorem defines StepTimes SFMASTR2:def 3 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));

theorem Th6: :: SFMASTR2:10
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being good MacroInstruction of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1
proof end;

theorem Th7: :: SFMASTR2:11
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being good MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds
((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = s . a
proof end;

theorem Th8: :: SFMASTR2:12
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & 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} \/ (UsedILoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) - 1 ) )
proof end;

theorem Th9: :: SFMASTR2:13
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) 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 Instruction-Sequence of SCM+FSA
for a being Int-Location
for f being FinSeq-Location
for I being MacroInstruction of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA ;
pred ProperTimesBody a,I,s,p means :: SFMASTR2:def 4
 for k being Nat st k < s . a holds
I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I));
end;

:: deftheorem 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 MacroInstruction of SCM+FSA holds
( ProperTimesBody a,I,s,p iff for k being Nat st k < s . a holds
I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) );

theorem Th11: :: SFMASTR2:15
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being MacroInstruction of SCM+FSA st I is parahalting holds
ProperTimesBody a,I,s,p by SCMFSA7B:19;

theorem Th12: :: SFMASTR2:16
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
proof end;

theorem Th13: :: SFMASTR2:17
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
(((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + k = s . a
proof end;

theorem Th14: :: SFMASTR2:18
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds
for k being Nat st k >= s . a holds
( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc 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 Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 holds
((StepTimes (a,I,p,s)) . 0) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)
proof end;

theorem Th16: :: SFMASTR2:20
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA 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)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds
((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
proof end;

theorem :: SFMASTR2:21
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA 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)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)
proof end;

theorem :: SFMASTR2:22
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds
(IExec ((times (a,I)),p,s)) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)
proof end;

theorem Th19: :: SFMASTR2:23
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
proof end;

theorem :: SFMASTR2:24
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
times (a,J) is_halting_on s,p
proof end;

definition
let d be read-write Int-Location;
func triv-times d -> MacroInstruction 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 MacroInstruction 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)))));

registration
let d be read-write Int-Location;
cluster triv-times d -> really-closed ;
coherence
triv-times d is really-closed ;
end;

theorem :: SFMASTR2:25
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for d being read-write Int-Location st s . d <= 0 holds
(IExec ((triv-times d),p,s)) . d = s . d
proof end;

theorem :: SFMASTR2:26
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for d being read-write Int-Location st 0 <= s . d holds
(IExec ((triv-times d),p,s)) . d = 0
proof end;