:: The Construction and Computation of For-loop Programs for SCMPDS :: by JingChao Chen and Piotr Rudnicki :: :: Received December 27, 1999 :: Copyright (c) 1999-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, SUBSET_1, SCMPDS_2, AMI_1, FSM_1, INT_1, AMI_2, ARYTM_1, COMPLEX1, ARYTM_3, CARD_1, RELAT_1, FUNCT_4, XBOOLE_0, CIRCUIT2, FUNCT_1, NAT_1, TARSKI, TURING_1, VALUED_1, SCMPDS_4, AMISTD_2, XXREAL_0, AMI_3, SCMFSA_7, UNIALG_2, SCMFSA7B, GRAPHSP, MSUALG_1, SCMFSA6B, SCMPDS_5, STRUCT_0, SFMASTR3, SEMI_AF1, SCMP_GCD, FINSEQ_1, CARD_3, FINSEQ_3, SCMPDS_7, PARTFUN1, EXTPRO_1, SCMFSA6C, COMPOS_1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1, NAT_1, FUNCOP_1, AFINSQ_1, VALUED_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, FUNCT_7, SCMPDS_2, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMP_GCD, FINSEQ_1, WSIERP_1; constructors ENUMSET1, XXREAL_0, REAL_1, INT_2, WSIERP_1, SCM_1, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMP_GCD, AMI_2, MEMSTR_0, RELSET_1, NUMBERS; registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMPDS_2, SCMPDS_4, SCMPDS_5, VALUED_0, FINSEQ_1, CARD_1, FUNCT_4, COMPOS_1, AFINSQ_1, EXTPRO_1, MEMSTR_0, COMPOS_0; requirements REAL, NUMERALS, SUBSET, ARITHM; begin :: Preliminaries reserve x for set, m,n for Nat, a,b for Int_position, i,j,k for Instruction of SCMPDS, s,s1,s2 for State of SCMPDS, k1,k2 for Integer, loc,l for Nat, I,J,K for Program of SCMPDS; theorem :: SCMPDS_7:1 ::SCMPDS_6:23 for s being State of SCMPDS,m,n being Nat st IC s= m holds ICplusConst(s,n-m)= n; theorem :: SCMPDS_7:2 i ';' I ';' j ';' k = i ';' (I ';' j ';' k); theorem :: SCMPDS_7:3 Shift(J,card I) c= I ';' J ';' K; theorem :: SCMPDS_7:4 I c= stop (I ';' J); ::$CT 2 theorem :: SCMPDS_7:7 for s being State of SCMPDS, i being Instruction of SCMPDS st InsCode i in {0,4,5,6,14} holds DataPart Exec(i,s) = DataPart s; reserve P,P1,P2,Q for Instruction-Sequence of SCMPDS; theorem :: SCMPDS_7:8 for s1,s2 being State of SCMPDS,I being Program of SCMPDS st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 for k being Nat holds Comput(P1 +* stop I,Initialize s1,k) = Comput(P2 +* stop I,Initialize s2,k) & CurInstr(P1 +* stop I,Comput(P1 +* stop I,Initialize s1,k)) = CurInstr(P2 +* stop I,Comput(P2 +* stop I,Initialize s2,k)); theorem :: SCMPDS_7:9 ::SCMPDS_5:20 for s being 0-started State of SCMPDS for I being Program of SCMPDS st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 for k being Nat holds Comput(P1,s,k) = Comput(P2,s,k) & CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k)); theorem :: SCMPDS_7:10 ::SCMPDS_5:21 for s being 0-started State of SCMPDS for I being Program of SCMPDS st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds LifeSpan(P1,s) = LifeSpan(P2,s) & Result(P1,s) = Result(P2,s); theorem :: SCMPDS_7:11 for s1,s2 being State of SCMPDS,I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds LifeSpan(P1 +* stop I,Initialize s1) = LifeSpan(P2 +* stop I,Initialize s2) & Result(P1 +* stop I,Initialize s1) = Result(P2 +* stop I,Initialize s2); theorem :: SCMPDS_7:12 for s1,s2 being 0-started State of SCMPDS,I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput(P1,s1,k) = s2 holds Result(P1,s1) = Result(P2,s2); theorem :: SCMPDS_7:13 for s being State of SCMPDS,I being Program of SCMPDS, a being Int_position st I is_halting_on s,P holds IExec(I,P,Initialize s).a = Comput(P +* stop I,Initialize s, (LifeSpan(P +* stop I,Initialize s))).a; theorem :: SCMPDS_7:14 for s being State of SCMPDS,I being parahalting Program of SCMPDS, a being Int_position holds IExec(I,P,Initialize s).a = Comput(P +* stop I,Initialize s, (LifeSpan(P +* stop I,Initialize s))).a; theorem :: SCMPDS_7:15 for s being 0-started State of SCMPDS for I being Program of SCMPDS,i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan(P,s) holds IC Comput(P,s,i) in dom I; theorem :: SCMPDS_7:16 for s1 being 0-started State of SCMPDS for I being shiftable Program of SCMPDS st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 for n being Nat st Shift(I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 for i being Nat holds i < LifeSpan(P1,s1) implies IC Comput(P1,s1,i) + n = IC Comput(P2,s2,i) & CurInstr(P1,Comput(P1,s1,i)) = CurInstr(P2,Comput(P2,s2,i)) & DataPart Comput(P1,s1,i) = DataPart Comput(P2,s2,i); theorem :: SCMPDS_7:17 for s being 0-started State of SCMPDS for I being halt-free Program of SCMPDS st stop I c= P & I is_halting_on s,P holds LifeSpan(P,s) > 0; theorem :: SCMPDS_7:18 for s1 being 0-started State of SCMPDS for I being halt-free shiftable Program of SCMPDS st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 for n being Nat st Shift(I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds IC Comput(P2,s2,LifeSpan(P1,s1)) = card I + n & DataPart Comput(P1,s1,LifeSpan(P1,s1)) = DataPart Comput(P2,s2,LifeSpan(P1,s1)); theorem :: SCMPDS_7:19 ::SCMPDS_5:33 for I being Program of SCMPDS,J being Program of SCMPDS, k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan(P +* stop I,Initialize s) holds Comput(P +* stop I,Initialize s,k) = Comput(P+*(I ';' J), Initialize s,k); theorem :: SCMPDS_7:20 ::SCMPDS_5:29 for I,J being Program of SCMPDS,k be Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan(P +* stop I,Initialize s) holds Comput(P +* J, Initialize s,k) = Comput(P +* stop I,Initialize s,k); theorem :: SCMPDS_7:21 for I,J being Program of SCMPDS,k be Nat st k <= LifeSpan(P +* stop I,Initialize s) & I c= J & I is_closed_on s,P & I is_halting_on s,P holds IC Comput(P +* J,Initialize s,k) in dom stop I; theorem :: SCMPDS_7:22 ::SCMPDS_5:31 for I,J being Program of SCMPDS st I c= J & I is_closed_on s,P & I is_halting_on s,P holds CurInstr(P +* J,Comput(P +* J, Initialize s, LifeSpan(P +* stop I,Initialize s))) = halt SCMPDS or IC Comput(P +* J,Initialize s, LifeSpan(P +* stop I,Initialize s)) = card I; theorem :: SCMPDS_7:23 for I,J being Program of SCMPDS st I is_halting_on s,P & J is_closed_on IExec(I,P,Initialize s),P & J is_halting_on IExec(I,P,Initialize s),P holds J is_closed_on Comput(P +* stop I, Initialize s, LifeSpan(P +* stop I,Initialize s)), P +* stop I & J is_halting_on Comput(P +* stop I, Initialize s, LifeSpan(P +* stop I,Initialize s)), P +* stop I; theorem :: SCMPDS_7:24 for I being Program of SCMPDS,J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec(I,P,Initialize s),P & J is_halting_on IExec(I,P,Initialize s),P holds I ';'J is_closed_on s,P & I ';' J is_halting_on s,P; theorem :: SCMPDS_7:25 :: SCMPDS_5:30 for I be halt-free Program of SCMPDS,J be Program of SCMPDS st I c= J & I is_closed_on s,P & I is_halting_on s,P holds IC Comput(P+*J, Initialize s, LifeSpan(P +* stop I,Initialize s)) = card I; theorem :: SCMPDS_7:26 ::SCMPDS_6:42 for I being Program of SCMPDS,s being State of SCMPDS, k being Nat st I is_halting_on s,P & k < LifeSpan(P+*stop I,Initialize s) holds CurInstr(P+*stop I,Comput(P +* stop I,Initialize s,k)) <> halt SCMPDS; theorem :: SCMPDS_7:27 ::SCMPDS_6:42 for I,J being Program of SCMPDS,s being 0-started State of SCMPDS, k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan(P +* stop I,s) holds CurInstr(P+*stop(I ';' J),Comput(P+*stop(I ';' J),s,k)) <> halt SCMPDS; theorem :: SCMPDS_7:28 ::SCMPDS_5:37 for s being 0-started State of SCMPDS for I being halt-free Program of SCMPDS,J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec(I,P,s),P & J is_halting_on IExec(I,P,s),P holds LifeSpan(P+*stop(I ';' J),s) = LifeSpan(P +* stop I,s) + LifeSpan(P +* stop I +* stop J, Initialize Result(P +* stop I,s)); theorem :: SCMPDS_7:29 :: SCMPDS_5:38 for s being 0-started State of SCMPDS for I being halt-free Program of SCMPDS, J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec(I,P,s),P & J is_halting_on IExec(I,P,s),P holds IExec(I ';' J,P,s) = IncIC(IExec(J,P,Initialize IExec(I,P,s)), card I); theorem :: SCMPDS_7:30 ::SCMPDS_5:39 for s being 0-started State of SCMPDS for I being halt-free Program of SCMPDS, J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec(I,P,s),P & J is_halting_on IExec(I,P,s),P holds IExec(I ';' J,P,s).a = IExec(J,P,Initialize IExec(I,P,s)).a; theorem :: SCMPDS_7:31 ::SCMPDS_5:46 for s being 0-started State of SCMPDS for I being halt-free Program of SCMPDS,j being parahalting shiftable Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds IExec(I ';' j,P,s).a = Exec(j, IExec(I,P,s)).a; begin :: The construction of for-up loop program :: while (a,i)<=0 do { I, (a,i)+=n } definition let a be Int_position, i be Integer,n be Nat; let I be Program of SCMPDS; func for-up(a,i,n,I) -> Program of SCMPDS equals :: SCMPDS_7:def 1 (a,i)>=0_goto (card I +3) ';' I ';' AddTo(a,i,n) ';' goto -(card I+2); end; begin :: The computation of for-up loop program theorem :: SCMPDS_7:32 for a be Int_position,i be Integer,n be Nat,I be Program of SCMPDS holds card for-up(a,i,n,I)= card I +3; theorem :: SCMPDS_7:33 for a be Int_position,i be Integer,n,m be Nat, I be Program of SCMPDS holds m < card I+3 iff m in dom for-up(a,i,n,I); theorem :: SCMPDS_7:34 for a be Int_position,i be Integer,n be Nat, I be Program of SCMPDS holds for-up(a,i,n,I). 0=(a,i)>=0_goto (card I +3) & for-up(a,i,n,I). (card I+1)=AddTo(a,i,n) & for-up(a,i,n,I). (card I +2)=goto -(card I+2); theorem :: SCMPDS_7:35 for s being State of SCMPDS,I being Program of SCMPDS,a being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) >= 0 holds for-up(a,i,n,I) is_closed_on s,P & for-up(a,i,n,I) is_halting_on s,P; theorem :: SCMPDS_7:36 for s being State of SCMPDS,I being Program of SCMPDS,a,c being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) >= 0 holds IExec(for-up(a,i,n,I),P,Initialize s) = s +* Start-At((card I+3),SCMPDS); theorem :: SCMPDS_7:37 for s being State of SCMPDS,I being Program of SCMPDS,a being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) >= 0 holds IC IExec(for-up(a,i,n,I),P,Initialize s) = card I + 3; theorem :: SCMPDS_7:38 for s being State of SCMPDS,I being Program of SCMPDS,a,b being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) >= 0 holds IExec(for-up(a,i,n,I),P,Initialize s).b = s.b; theorem :: SCMPDS_7:39 for s being State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a be Int_position, i be Integer,n be Nat,X be set st s.DataLoc(s.a,i) < 0 & not DataLoc(s.a,i) in X & n > 0 & a <> DataLoc(s.a,i) & (for t be State of SCMPDS,Q st (for x be Int_position st x in X holds t.x=s.x) & t.a=s.a holds IExec(I,Q,Initialize t).a=t.a & IExec(I,Q,Initialize t).DataLoc(s.a,i)=t.DataLoc(s.a,i) & I is_closed_on t,Q & I is_halting_on t,Q & for y be Int_position st y in X holds IExec(I,Q,Initialize t).y=t.y) holds for-up(a,i,n,I) is_closed_on s,P & for-up(a,i,n,I) is_halting_on s,P; theorem :: SCMPDS_7:40 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a be Int_position, i be Integer,n be Nat,X be set st s. DataLoc(s.a,i) < 0 & not DataLoc(s.a,i) in X & n > 0 & a <> DataLoc(s.a,i) & (for t be State of SCMPDS,Q st (for x be Int_position st x in X holds t.x=s.x) & t.a=s.a holds IExec(I,Q,Initialize t).a=t.a & IExec(I,Q,Initialize t).DataLoc(s.a,i)=t. DataLoc(s.a,i) & I is_closed_on t,Q & I is_halting_on t,Q & for y be Int_position st y in X holds IExec(I,Q,Initialize t).y=t.y) holds IExec(for-up(a,i,n,I),P,s) = IExec(for-up(a,i,n,I),P, Initialize IExec(I ';' AddTo(a,i,n),P,s)); registration let I be shiftable Program of SCMPDS, a be Int_position,i be Integer,n be Nat; cluster for-up(a,i,n,I) -> shiftable; end; registration let I be halt-free Program of SCMPDS, a be Int_position,i be Integer,n be Nat; cluster for-up(a,i,n,I) -> halt-free; end; begin :: The construction of for-down loop program :: while (a,i)>=0 do { I, (a,i)-=n } definition let a be Int_position, i be Integer,n be Nat; let I be Program of SCMPDS; func for-down(a,i,n,I) -> Program of SCMPDS equals :: SCMPDS_7:def 2 (a,i)<=0_goto (card I +3) ';' I ';' AddTo(a,i,-n) ';' goto -(card I+2); end; begin :: The computation of for-down loop program theorem :: SCMPDS_7:41 for a be Int_position,i be Integer,n be Nat,I be Program of SCMPDS holds card for-down(a,i,n,I)= card I +3; theorem :: SCMPDS_7:42 for a be Int_position,i be Integer,n,m be Nat, I be Program of SCMPDS holds m < card I+3 iff m in dom for-down(a,i,n,I); theorem :: SCMPDS_7:43 for a be Int_position,i be Integer,n be Nat, I be Program of SCMPDS holds for-down(a,i,n,I). 0=(a,i)<=0_goto (card I +3) & for-down(a,i,n,I). (card I+1)=AddTo(a,i,-n) & for-down(a,i,n,I). ( card I+2)=goto -(card I+2); theorem :: SCMPDS_7:44 for s being State of SCMPDS,I being Program of SCMPDS,a being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) <= 0 holds for-down(a,i,n,I) is_closed_on s,P & for-down(a,i,n,I) is_halting_on s,P; theorem :: SCMPDS_7:45 for s being State of SCMPDS,I being Program of SCMPDS,a,c being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) <= 0 holds IExec(for-down(a,i,n,I),P,Initialize s) = s +* Start-At((card I+3),SCMPDS); theorem :: SCMPDS_7:46 for s being State of SCMPDS,I being Program of SCMPDS,a being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) <= 0 holds IC IExec(for-down(a,i,n,I),P,Initialize s) = card I + 3; theorem :: SCMPDS_7:47 for s being State of SCMPDS,I being Program of SCMPDS,a,b being Int_position, i being Integer,n be Nat st s.DataLoc(s.a,i) <= 0 holds IExec(for-down(a,i,n,I),P,Initialize s).b = s.b; theorem :: SCMPDS_7:48 for s being State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a be Int_position, i be Integer,n be Nat,X be set st s.DataLoc(s.a,i) > 0 & not DataLoc(s.a,i) in X & n > 0 & a <> DataLoc(s.a,i) & (for t be 0-started State of SCMPDS,Q st (for x be Int_position st x in X holds t.x=s.x) & t.a=s.a holds IExec(I,Q,t).a=t.a & IExec(I,Q,t).DataLoc(s.a,i)=t.DataLoc(s.a,i) & I is_closed_on t,Q & I is_halting_on t,Q & for y be Int_position st y in X holds IExec(I,Q,t).y=t.y) holds for-down(a,i,n,I) is_closed_on s,P & for-down(a,i,n,I) is_halting_on s,P; theorem :: SCMPDS_7:49 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a be Int_position, i be Integer,n be Nat,X be set st s.DataLoc(s.a,i) > 0 & not DataLoc(s.a,i) in X & n > 0 & a <> DataLoc(s.a,i) & (for t be 0-started State of SCMPDS,Q st (for x be Int_position st x in X holds t.x=s.x) & t.a=s.a holds IExec(I,Q,t).a=t.a & IExec(I,Q,t).DataLoc(s.a,i)=t. DataLoc(s.a,i) & I is_closed_on t,Q & I is_halting_on t,Q & for y be Int_position st y in X holds IExec(I,Q,t).y=t.y) holds IExec(for-down(a,i,n,I),P,s) = IExec(for-down(a,i,n,I),P,Initialize IExec(I ';' AddTo(a,i,-n),P,s)); registration let I be shiftable Program of SCMPDS, a be Int_position,i be Integer,n be Nat; cluster for-down(a,i,n,I) -> shiftable; end; registration let I be halt-free Program of SCMPDS, a be Int_position,i be Integer,n be Nat; cluster for-down(a,i,n,I) -> halt-free; end; begin :: Two Examples for Summing :: n=Sum 1+1+...+1 definition let n be Nat; func sum(n) -> Program of SCMPDS equals :: SCMPDS_7:def 3 (GBP:=0) ';' ((GBP,2):=n) ';' ((GBP, 3):=0) ';' for-down(GBP,2,1, Load AddTo(GBP,3,1)); end; theorem :: SCMPDS_7:50 for s being 0-started State of SCMPDS st s.GBP=0 holds for-down(GBP,2,1, Load AddTo(GBP,3,1)) is_closed_on s,P & for-down(GBP,2,1, Load AddTo(GBP,3,1)) is_halting_on s,P; theorem :: SCMPDS_7:51 for s being 0-started State of SCMPDS,n be Nat st s.GBP=0 & s.intpos 2=n & s.intpos 3=0 holds IExec(for-down(GBP,2,1, Load AddTo(GBP,3,1)),P,s).intpos 3 =n; theorem :: SCMPDS_7:52 for s being 0-started State of SCMPDS,n be Nat holds IExec(sum(n),P,s).intpos 3 =n; :: sum=Sum x1+x2+...+x2 definition let sp,control,result,pp,pData be Nat; func sum(sp,control,result,pp,pData) -> Program of SCMPDS equals :: SCMPDS_7:def 4 ((intpos sp ,result):=0) ';' (intpos pp:=pData) ';' for-down(intpos sp,control,1, AddTo( intpos sp,result,intpos pData,0) ';' AddTo(intpos pp,0,1)); end; theorem :: SCMPDS_7:53 for s being 0-started State of SCMPDS,sp,cv,result,pp,pD be Nat st s.intpos sp > sp & cv < result & s.intpos pp=pD & s.intpos sp+result < pp & pp sp & cv < result & s.intpos pp=pD & s.intpos sp+result < pp & pp sp & cv < result & s.intpos sp+result < pp & pp