:: While Macro Instructions of SCM+FSA :: by Jing-Chao Chen :: :: Received December 10, 1997 :: Copyright (c) 1997-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, AMI_1, SCMFSA_2, CARD_1, SCMFSA8B, SCMFSA8A, AMISTD_2, ARYTM_3, SUBSET_1, FUNCT_4, AMI_3, RELAT_1, TARSKI, XBOOLE_0, NAT_1, SCMFSA6A, FUNCT_1, XXREAL_0, VALUED_1, CARD_3, ARYTM_1, FSM_1, SF_MASTR, SCMFSA7B, CIRCUIT2, GRAPHSP, SCMFSA6B, SCMFSA_9, PBOOLE, PARTFUN1, EXTPRO_1, RELOC, SCMFSA6C, COMPOS_1, MEMSTR_0, AMISTD_1, TURING_1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, AFINSQ_1, FUNCOP_1, FUNCT_4, CARD_3, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, VALUED_1, PBOOLE, NAT_1, NAT_D, AMISTD_1, AMISTD_2, SCMFSA_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA7B, SCMFSA8A, SCMFSA8B, XXREAL_0, SCMFSA_M, SCMFSA_X; constructors XXREAL_0, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA8A, FUNCT_4, SCMFSA8B, AMISTD_2, RELSET_1, PRE_POLY, PBOOLE, SCMFSA7B, DOMAIN_1, AMISTD_1, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X, COMPOS_2, NAT_D; registrations RELSET_1, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SCMFSA6B, SCMFSA7B, SCMFSA8A, ORDINAL1, VALUED_1, FUNCT_4, VALUED_0, AFINSQ_1, FUNCOP_1, COMPOS_1, EXTPRO_1, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M; requirements REAL, NUMERALS, SUBSET, ARITHM; begin reserve P,Q for Instruction-Sequence of SCM+FSA; :: WHILE Statement reserve m, n for Nat; ::$CD 3 ::$CT 17 theorem :: SCMFSA_9:18 for s being State of SCM+FSA, I being MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a <> 0 holds while=0(a,I) is_halting_on s,P; theorem :: SCMFSA_9:19 for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA, s being State of SCM+FSA,k being Nat st I is_halting_on s,P & k < LifeSpan(P +* I,Initialize s) & IC Comput(P +* while=0(a,I),(Initialize s),1+k) = IC Comput(P +* I, (Initialize s),k) + 3 & DataPart Comput(P +* while=0(a,I),(Initialize s),1+k) = DataPart Comput(P +* I,(Initialize s),k) holds IC Comput(P +* while=0(a,I),(Initialize s),1+k+1) = IC Comput(P +* I, (Initialize s),k+1) + 3 & DataPart Comput(P +* while=0(a,I),(Initialize s),1+k+1) = DataPart Comput(P +* I, (Initialize s),k+1); :: Twierdzeinie zmienia znaczenie, jezeli w oryginale mowilo :: ze znajdziemy sie w miejscu "przed powrotem" i wykonujemy Next :: to w tym miejscu jest teraz powrot i wykonujemy goto 0 theorem :: SCMFSA_9:20 for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA, s being State of SCM+FSA st I is_halting_on s,P & IC Comput(P +* while=0(a,I), Initialize s,1 + LifeSpan(P +* I,Initialize s) ) = IC Comput(P +* I,Initialize s,LifeSpan(P +* I,Initialize s) ) + 3 holds CurInstr(P +* while=0(a,I), Comput(P +* while=0(a,I),Initialize s, (1 + LifeSpan(P +* I,Initialize s)))) = goto 0; reserve f for FinSeq-Location, c for Int-Location; ::$CT theorem :: SCMFSA_9:22 for s being State of SCM+FSA, I being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st I is_halting_on s,P & s.a =0 holds IC Comput(P +* while=0(a,I), Initialize s, (LifeSpan(P +* I,Initialize s) + 2)) = 0 & for k being Nat st k <= LifeSpan(P +* I,Initialize s) + 2 holds IC Comput(P +* while=0(a,I), (Initialize s),k) in dom while=0(a,I); reserve s for State of SCM+FSA, I for MacroInstruction of SCM+FSA, a for read-write Int-Location; definition let s,I,a,P; func StepWhile=0(a,I,P,s) -> sequence of product the_Values_of SCM+FSA means :: SCMFSA_9:def 4 it.0 = s & for i being Nat holds it.(i+1)= Comput(P +* while=0(a,I), Initialize(it.i), LifeSpan(P +* while=0(a,I) +* I, Initialize(it.i)) + 2); end; reserve i,k,m,n for Nat; theorem :: SCMFSA_9:23 StepWhile=0(a,I,P,s).(k+1)=StepWhile=0(a,I,P,StepWhile=0(a,I,P,s).k).1; ::$CT theorem :: SCMFSA_9:25 for I being MacroInstruction of SCM+FSA,a being read-write Int-Location, s being State of SCM+FSA holds StepWhile=0(a,I,P,s).1 = Comput(P +* while=0(a,I),Initialize s, LifeSpan(P +* while=0(a,I)+* I,Initialize s) + 2); theorem :: SCMFSA_9:26 for I being MacroInstruction of SCM+FSA,a being read-write Int-Location, s being State of SCM+FSA,k,n being Nat st IC StepWhile=0(a,I,P,s).k = 0 & StepWhile=0(a,I,P,s).k= Comput(P +* while=0(a,I), (Initialize s),n) holds StepWhile=0(a,I,P,s).k = Initialize(StepWhile=0(a,I,P,s).k) & StepWhile=0(a,I,P,s).(k+1)=Comput(P +* while=0(a,I), Initialize s, (n +(LifeSpan(P +* while=0(a,I) +* I, Initialize(StepWhile=0(a,I,P,s).k)) + 2))); theorem :: SCMFSA_9:27 for I being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location, s being State of SCM+FSA st (for k being Nat holds I is_halting_on StepWhile=0(a,I,P,s).k,P+*while=0(a,I)) & ex f being Function of product the_Values_of SCM+FSA,NAT st for k being Nat holds ((f.(StepWhile=0(a,I,P,s).(k+1)) < f.(StepWhile=0(a,I,P,s).k) or f.(StepWhile=0(a,I,P,s).k) = 0) & (f.(StepWhile=0(a,I,P,s).k)=0 iff (StepWhile=0(a,I,P,s).k).a <> 0)) holds while=0(a,I) is_halting_on s,P; theorem :: SCMFSA_9:28 for I being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location, s being State of SCM+FSA st ex f being Function of product the_Values_of SCM+FSA,NAT st for k being Nat holds (f.(StepWhile=0(a,I,P,s).(k+1)) < f.(StepWhile=0(a,I,P,s).k) or f.(StepWhile=0(a,I,P,s).k) = 0) & (f.(StepWhile=0(a,I,P,s).k)=0 iff (StepWhile=0(a,I,P,s).k).a <> 0 ) holds while=0(a,I) is_halting_on s,P; theorem :: SCMFSA_9:29 for I being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st ex f being Function of product the_Values_of SCM+FSA,NAT st (for s being State of SCM+FSA,P holds (f.(StepWhile=0(a,I,P,s).1) < f.s or f.s = 0) & ( f.s =0 iff s.a <> 0 )) holds while=0(a,I) is parahalting; ::$CT theorem :: SCMFSA_9:31 for i being Instruction of SCM+FSA st i does not destroy intloc 0 holds Macro i is good; registration let I,J be good MacroInstruction of SCM+FSA,a be Int-Location; cluster if=0(a,I,J) -> good; end; registration let I be good MacroInstruction of SCM+FSA,a be Int-Location; cluster if=0(a,I) -> good; end; registration let I be good MacroInstruction of SCM+FSA,a be Int-Location; cluster while=0(a,I) -> good; end; :: ----------------------------------------------------------- :: WHILE>0 Statement ::$CT 6 theorem :: SCMFSA_9:38 for s being State of SCM+FSA, I being MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a <= 0 holds while>0(a,I) is_halting_on s,P; theorem :: SCMFSA_9:39 for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA, s being State of SCM+FSA,k being Nat st I is_halting_on s,P & k < LifeSpan(P +* I,Initialize s) & IC Comput(P +* while>0(a,I),(Initialize s),1+k) = IC Comput(P +* I, (Initialize s),k) + 3 & DataPart Comput(P +* while>0(a,I),(Initialize s),1+k) = DataPart Comput(P +* I,(Initialize s),k) holds IC Comput(P +* while>0(a,I),(Initialize s),1+k+1) = IC Comput(P +* I, (Initialize s),k+1) + 3 & DataPart Comput(P +* while>0(a,I),(Initialize s),1+k+1) = DataPart Comput(P +* I, (Initialize s),k+1); theorem :: SCMFSA_9:40 for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA, s being State of SCM+FSA st I is_halting_on s,P & IC Comput(P +* while>0(a,I), Initialize s,1 + LifeSpan(P +* I,Initialize s)) = IC Comput(P +* I,Initialize s,LifeSpan(P +* I,Initialize s) ) + 3 holds CurInstr(P +* while>0(a,I), Comput(P +* while>0(a,I),Initialize s, (1 + LifeSpan(P +* I,Initialize s)))) = goto 0; ::$CT theorem :: SCMFSA_9:42 for s being State of SCM+FSA, I being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st I is_halting_on s,P & s.a >0 holds IC Comput(P +* while>0(a,I), Initialize s, (LifeSpan(P +* I,Initialize s) + 2)) = 0 & for k being Nat st k <= LifeSpan(P +* I,Initialize s) + 2 holds IC Comput(P +* while>0(a,I), (Initialize s),k) in dom while>0(a,I); reserve s for State of SCM+FSA, I for MacroInstruction of SCM+FSA, a for read-write Int-Location; definition let s,I,a,P; func StepWhile>0(a,I,P,s) -> sequence of product the_Values_of SCM+FSA means :: SCMFSA_9:def 5 it.0 = s & for i being Nat holds it.(i+1)= Comput(P +* while>0(a,I), Initialize(it.i), LifeSpan(P +* while>0(a,I) +* I, Initialize(it.i)) + 2); end; theorem :: SCMFSA_9:43 StepWhile>0(a,I,P,s).(k+1)=StepWhile>0(a,I,P,StepWhile>0(a,I,P,s).k).1; theorem :: SCMFSA_9:44 for I being MacroInstruction of SCM+FSA,a being read-write Int-Location, s being State of SCM+FSA holds StepWhile>0(a,I,P,s).1 = Comput(P +* while>0(a,I), Initialize s, LifeSpan(P +* while>0(a,I)+* I,Initialize s) + 2); theorem :: SCMFSA_9:45 for I being MacroInstruction of SCM+FSA,a being read-write Int-Location, s being State of SCM+FSA,k,n being Nat st IC StepWhile>0(a,I,P,s).k = 0 & StepWhile>0(a,I,P,s).k= Comput(P +* while>0(a,I), (Initialize s),n) holds StepWhile>0(a,I,P,s).k = Initialize(StepWhile>0(a,I,P,s).k) & StepWhile>0(a,I,P,s).(k+1)= Comput(P +* while>0(a,I), Initialize s, n +(LifeSpan(P +* while>0(a,I) +* I,Initialize(StepWhile>0(a,I,P,s).k) ) + 2)); theorem :: SCMFSA_9:46 for I being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location, s being State of SCM+FSA st (for k being Nat holds I is_halting_on StepWhile>0(a,I,P,s).k,P+*while>0(a,I)) & ex f being Function of product the_Values_of SCM+FSA,NAT st (for k being Nat holds (f.( StepWhile>0(a,I,P,s).(k+1)) < f.(StepWhile>0(a,I,P,s).k) or f.(StepWhile>0(a,I,P,s).k ) = 0) & ( f.(StepWhile>0(a,I,P,s).k)=0 iff (StepWhile>0(a,I,P,s).k).a <= 0 )) holds while>0(a,I) is_halting_on s,P; theorem :: SCMFSA_9:47 for I being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location, s being State of SCM+FSA st ex f being Function of product the_Values_of SCM+FSA,NAT st (for k being Nat holds (f.(StepWhile>0(a,I,P,s).(k+ 1)) < f.(StepWhile>0(a,I,P,s).k) or f.(StepWhile>0(a,I,P,s).k) = 0) & ( f.( StepWhile>0(a,I,P,s).k)=0 iff (StepWhile>0(a,I,P,s).k).a <= 0 ) ) holds while>0(a,I) is_halting_on s,P; theorem :: SCMFSA_9:48 for I being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st ex f being Function of product the_Values_of SCM+FSA,NAT st (for s being State of SCM+FSA,P holds (f.(StepWhile>0(a,I,P,s).1) < f.s or f.s = 0) & ( f.s =0 iff s.a <= 0 )) holds while>0(a,I) is parahalting; registration let I,J be good MacroInstruction of SCM+FSA,a be Int-Location; cluster if>0(a,I,J) -> good; end; registration let I be good MacroInstruction of SCM+FSA,a be Int-Location; cluster if>0(a,I) -> good; end; registration let I be good MacroInstruction of SCM+FSA,a be Int-Location; cluster while>0(a,I) -> good; end; theorem :: SCMFSA_9:49 for p be preProgram of SCM+FSA,l be Nat, ic be Instruction of SCM+FSA st (ex pc be Instruction of SCM+FSA st pc=p.l & UsedIntLoc pc =UsedIntLoc ic) holds UsedILoc p = UsedILoc(p+*(l,ic)); theorem :: SCMFSA_9:50 for p be preProgram of SCM+FSA,l be Nat, ic be Instruction of SCM+FSA st (ex pc be Instruction of SCM+FSA st pc=p.l & UsedInt*Loc pc=UsedInt*Loc ic) holds UsedI*Loc p = UsedI*Loc (p +*(l,ic));