:: Constant assignment macro instructions of SCM+FSA, Part II :: by Noriko Asamoto :: :: Received August 27, 1996 :: Copyright (c) 1996-2019 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, FINSEQ_1, AMI_1, SCMFSA_2, RELAT_1, SCMFSA_7, ARYTM_3, ARYTM_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, CAT_1, NAT_1, CARD_1, FUNCOP_1, SCMFSA6A, ORDINAL4, AMI_3, FUNCT_4, INT_1, GRAPHSP, FSM_1, CIRCUIT2, EXTPRO_1, SCMFSA6B, SF_MASTR, MSUALG_1, XBOOLE_0, PRE_POLY, AMISTD_2, SCMFSA7B, AFINSQ_1, SCMFSA6C, COMPOS_1, AMISTD_1, TURING_1, RELOC, VALUED_1, SCMPDS_4; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2, FUNCOP_1, XXREAL_0, ENUMSET1, NAT_D, PBOOLE, AFINSQ_2, AMISTD_4, SCMFSA_7, COMPOS_2, SCMFSA6A, SF_MASTR, SCMFSA6B, INT_2, PRE_POLY, SCMFSA_M; constructors ENUMSET1, XXREAL_0, REAL_1, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B, NAT_D, RELSET_1, PRE_POLY, DOMAIN_1, AFINSQ_2, PARTFUN3, PBOOLE, AMISTD_1, AMISTD_2, AMI_3, MEMSTR_0, SCMFSA_M, FUNCT_7, COMPOS_2; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6B, ORDINAL1, CARD_1, AFINSQ_1, COMPOS_1, AFINSQ_2, EXTPRO_1, FUNCT_4, STRUCT_0, MEMSTR_0, SCMFSA10, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, COMPOS_2, SCMFSA6C, SCMFSA_4; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, SCMFSA6B, AMISTD_1; equalities FUNCOP_1, SCMFSA6A, SCMFSA6B, COMPOS_1, SCMFSA_7, EXTPRO_1, MEMSTR_0, SCMFSA_M, CARD_1, ORDINAL1, COMPOS_2; expansions TARSKI, AMISTD_1; theorems SCMFSA_7, NAT_1, GRFUNC_1, FUNCT_1, FUNCT_4, FUNCT_7, ENUMSET1, SCMFSA_2, FUNCOP_1, INT_1, RELAT_1, TARSKI, SF_MASTR, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, AFINSQ_1, COMPOS_1, AFINSQ_2, CARD_1, EXTPRO_1, PARTFUN1, MEMSTR_0, SCMFSA_M, ORDINAL1, AMISTD_1, COMPOS_0, VALUED_1; schemes NAT_1, AFINSQ_1; begin reserve m for Nat; reserve P for Instruction-Sequence of SCM+FSA; set A = NAT; theorem for i being Instruction of SCM+FSA holds (i = halt SCM+FSA implies ( Directed Macro i). 0 = goto 2) & (i <> halt SCM+FSA implies ( Directed Macro i). 0 = i) proof A1: dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA; let i be Instruction of SCM+FSA; A2: (Macro i). 0 = i by COMPOS_1:58; 0 in { 0, 1} by TARSKI:def 2; then A3: 0 in dom Macro i by COMPOS_1:61; A4: card Macro i = 2 by COMPOS_1:56; hereby A5: dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA; assume A6: i = halt SCM+FSA; A7: i in dom (halt SCM+FSA .--> goto 2) by A6,TARSKI:def 1; rng Macro i c= the InstructionsF of SCM+FSA by RELAT_1:def 19; hence (Directed Macro i). 0 = (((id the InstructionsF of SCM+FSA) +* ( halt SCM+FSA, goto 2))*Macro i). 0 by A4,FUNCT_7:116 .= (((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2))*Macro i). 0 by A5,FUNCT_7:def 3 .= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2)).i by A3,A2,FUNCT_1:13 .= (halt SCM+FSA .--> goto 2).i by A7,FUNCT_4:13 .= goto 2 by A6,FUNCOP_1:72; end; assume i <> halt SCM+FSA; then A9: not i in dom (halt SCM+FSA .--> goto 2) by TARSKI:def 1; rng Macro i c= the InstructionsF of SCM+FSA by RELAT_1:def 19; hence (Directed Macro i). 0 = (((id the InstructionsF of SCM+FSA) +* ( halt SCM+FSA, goto 2))* Macro i). 0 by A4,FUNCT_7:116 .= (((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2))* Macro i). 0 by A1,FUNCT_7:def 3 .= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2 )).i by A3,A2,FUNCT_1:13 .= (id the InstructionsF of SCM+FSA).i by A9,FUNCT_4:11 .= i; end; theorem for i being Instruction of SCM+FSA holds (Directed Macro i). 1 = goto 2 proof let i be Instruction of SCM+FSA; A1: (Macro i). 1 = halt SCM+FSA by COMPOS_1:59; 1 in { 0, 1} by TARSKI:def 2; then A2: 1 in dom Macro i by COMPOS_1:61; A3: halt SCM+FSA in dom (halt SCM+FSA .--> goto 2) by TARSKI:def 1; A4: dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA; card Macro i = 2 & rng Macro i c= the InstructionsF of SCM+FSA by COMPOS_1:56,RELAT_1:def 19; hence (Directed Macro i). 1 = (((id the InstructionsF of SCM+FSA) +* ( halt SCM+FSA,goto 2))* Macro i). 1 by FUNCT_7:116 .= (((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2))* Macro i). 1 by A4,FUNCT_7:def 3 .= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2 )). halt SCM+FSA by A2,A1,FUNCT_1:13 .= (halt SCM+FSA .--> goto 2).halt SCM+FSA by A3,FUNCT_4:13 .= goto 2 by FUNCOP_1:72; end; registration let a be Int-Location, k be Integer; cluster a := k -> initial non empty NAT-defined (the InstructionsF of SCM+FSA)-valued; coherence proof a := k = aSeq(a,k) ^ Stop SCM+FSA by SCMFSA_7:1; hence thesis; end; end; Lm1: for s being State of SCM+FSA st IC s = 0 for P being Instruction-Sequence of SCM+FSA for a being Int-Location, k being Integer st a := k c= P holds P halts_on s proof let s be State of SCM+FSA; assume A1: IC s = 0; let P be Instruction-Sequence of SCM+FSA; A2: dom P = NAT by PARTFUN1:def 2; let a be Int-Location, k be Integer; assume A3: a := k c= P; per cases; suppose A4: k > 0; then consider k1 being Nat such that A5: k1 + 1 = k and A6: a := k = <% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA by SCMFSA_7:def 1; A7: len (<% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0))) = len <% a := intloc 0 %> + len (k1 --> AddTo(a,intloc 0)) by AFINSQ_1:17 .= 1 + len (k1 --> AddTo(a,intloc 0)) by AFINSQ_1:34 .= k by A5; set f = <% a:=intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA; A8: f.0 = (<% a := intloc 0 %> ^ ((k1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA)).0 by AFINSQ_1:27 .= a := intloc 0 by AFINSQ_1:35; reconsider k as Element of NAT by A4,INT_1:3; A9: len f = len (<% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0))) + len Stop SCM+FSA by AFINSQ_1:17 .= k + 1 by A7,AFINSQ_1:34; A10: now let i be Element of NAT; assume that A11: i <= k; i < k + 1 by A11,NAT_1:13; hence i in dom f by A9,AFINSQ_1:86; end; A12: for i being Element of NAT st i <= k holds P.i = f.i by A3,A6,A10,GRFUNC_1:2; then A13: P. 0 = a := intloc 0 by A8; A14: now let n be Element of NAT; assume n = 0; hence A15: Comput(P,s,n) = s; hence CurInstr(P,Comput(P,s,n)) = a:= intloc 0 by A1,A13,A2,PARTFUN1:def 6; thus Comput(P,s,n+1) = Following(P, Comput(P,s,n)) by EXTPRO_1:3 .= Exec(a:= intloc 0,s) by A15,A1,A13,A2,PARTFUN1:def 6; end; A16: now let i be Element of NAT; assume that A17: 1 <= i and A18: i < k; reconsider i1 = i - 1 as Element of NAT by A17,INT_1:5; i - 1 < k - 1 by A18,XREAL_1:9; then A19: i1 in Segm k1 by A5,NAT_1:44; A20: len <%a:= intloc 0%> = 1 by AFINSQ_1:33; A21: len(k1-->AddTo(a,intloc 0)) = k1; i in dom (<%a:=intloc 0%>^(k1-->AddTo(a,intloc 0))) by A18,A7,AFINSQ_1:86; hence f.i=(<%a:=intloc 0%>^(k1-->AddTo(a,intloc 0))).i by AFINSQ_1:def 3 .= (k1-->AddTo(a,intloc 0)).(i - 1) by A17,A18,A20,A21,A5,AFINSQ_1:18 .= AddTo(a,intloc 0) by A19,FUNCOP_1:7; end; A22: now let i be Nat; assume that A23: 0 < i and A24: i < k; A25: 0+1 <= i by A23,NAT_1:13; A26: i in NAT by ORDINAL1:def 12; hence P. i = f.(i) by A12,A24 .=AddTo(a,intloc 0) by A16,A25,A24,A26; end; A27: for i being Element of NAT st i <= k holds IC Comput(P,s,i) = i proof defpred P[Nat] means $1 <= k implies IC Comput(P,s,$1) = $1; let i be Element of NAT; assume A28: i <= k; A29: for n being Nat st P[n] holds P[n + 1] proof let n be Nat; assume A30: P[n]; assume A31: n+1 <= k; then A32: n < k by NAT_1:13; per cases; suppose A33: n=0; hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A14 .= n+1 by A1,A33,SCMFSA_2:63; end; suppose A34: n>0; n + 0 <= n + 1 by XREAL_1:7; then A35: CurInstr(P,Comput(P,s,n)) = P. n by A30,A31,A2,PARTFUN1:def 6,XXREAL_0:2 .= AddTo(a,intloc 0) by A22,A32,A34; A36: Comput(P,s,n+1) = Following(P, Comput(P,s,n)) by EXTPRO_1:3 .= Exec(AddTo(a,intloc 0), Comput(P,s,n)) by A35; thus IC Comput(P,s,n+1) = IC Comput(P,s,n)+1 by A36,SCMFSA_2:64 .= n+1 by A30,A31,NAT_1:13; end; end; A37: P[0] by A1; for i being Nat holds P[i] from NAT_1:sch 2(A37,A29); hence thesis by A28; end; k < k + len Stop SCM+FSA by XREAL_1:29; then A38: f.(k) = (Stop SCM+FSA).(k - k) by A7,AFINSQ_1:18 .= halt SCM+FSA by AFINSQ_1:34; CurInstr(P,Comput(P,s,k)) = P.IC Comput(P,s,k) by A2,PARTFUN1:def 6 .= P. k by A27 .= halt SCM+FSA by A38,A12; hence thesis by EXTPRO_1:29; end; suppose A39: k <= 0; then reconsider mk = - k as Element of NAT by INT_1:3; consider k1 being Nat such that A40: k1 + k = 1 and A41: a:=k = (<%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA) by A39,SCMFSA_7:def 1; A42: len (<%a:=intloc 0%>^(k1-->SubFrom(a,intloc 0))) = len<%a:=intloc 0%> + len(k1-->SubFrom(a,intloc 0)) by AFINSQ_1:17 .= 1 + len(k1-->SubFrom(a,intloc 0)) by AFINSQ_1:34 .= mk+1+1 by A40; set f = <%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA; A43: f.0 = (<%a:=intloc 0%>^((k1-->SubFrom(a,intloc 0))^Stop SCM+FSA)) .0 by AFINSQ_1:27 .= a := intloc 0 by AFINSQ_1:35; A44: len f = len(<%a:=intloc 0%>^(k1-->SubFrom(a,intloc 0)))+len Stop SCM+FSA by AFINSQ_1:17 .= mk+1+1 + 1 by A42,AFINSQ_1:34; A45: now let i be Nat; assume that 0 <= i and A46: i <= mk+1+1; i < mk+1+1+1 by A46,NAT_1:13; hence i in dom f by A44,AFINSQ_1:86; end; A47: for i being Nat st 0 <= i & i <= mk+1+1 holds P.i = f.i by A3,A41,A45,GRFUNC_1:2; then A48: P.0 = a := intloc 0 by A43; A49: now let n be Element of NAT; assume n = 0; hence A50: Comput(P,s,n) = s; hence CurInstr(P,Comput(P,s,n)) = a:= intloc 0 by A1,A48,A2,PARTFUN1:def 6; thus Comput(P,s,n+1) = Following(P, Comput(P,s,n)) by EXTPRO_1:3 .= Exec(a:= intloc 0,s) by A50,A1,A48,A2,PARTFUN1:def 6; end; A51: now A52: len <%a:= intloc 0%> = 1 by AFINSQ_1:33; let i be Nat; assume that A53: 1 <= i and A54: i < mk+1+1; reconsider i1 = i - 1 as Element of NAT by A53,INT_1:5; i-1 < k1+1-1 by A54,A40,XREAL_1:9; then A55: i1 in Segm k1 by NAT_1:44; A56: len(k1-->SubFrom(a,intloc 0)) = k1; i in dom (<%a:=intloc 0%>^(k1-->SubFrom(a,intloc 0))) by A54,A42,AFINSQ_1:86; hence f.i = (<%a:=intloc 0%>^(k1-->SubFrom(a,intloc 0))).i by AFINSQ_1:def 3 .= (k1-->SubFrom(a,intloc 0)).(i - 1) by A40,A53,A54,A52,A56,AFINSQ_1:18 .= SubFrom(a,intloc 0) by A55,FUNCOP_1:7; end; A57: now let i be Nat; assume that A58: 0 < i and A59: i < mk+1+1; A60: 0+1 <= i by A58,NAT_1:13; thus P. i = f.(i) by A47,A59 .=SubFrom(a,intloc 0) by A51,A60,A59; end; A61: for i being Nat st i <= mk+1+1 holds IC Comput(P,s,i) = i proof defpred P[Nat] means $1<=mk+1+1 implies IC Comput(P,s,$1)= $1; let i be Nat; assume A62: i <= mk+1+1; A63: for n being Nat st P[n] holds P[n + 1] proof let n be Nat; assume A64: P[n]; assume A65: n+1 <= mk+1+1; then A66: n < mk+1+1 by NAT_1:13; per cases; suppose A67: n=0; hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A49 .= n+1 by A1,A67,SCMFSA_2:63; end; suppose A68: n>0; n + 0 <= n + 1 by XREAL_1:7; then A69: CurInstr(P,Comput(P,s,n)) = P. n by A64,A65,A2,PARTFUN1:def 6,XXREAL_0:2 .= SubFrom(a,intloc 0) by A57,A66,A68; A70: Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3 .= Exec(SubFrom(a,intloc 0), Comput(P,s,n)) by A69; thus IC Comput(P,s,n+1) = IC Comput(P,s,n) + 1 by A70,SCMFSA_2:65 .= n+1 by A64,A65,NAT_1:13; end; end; A71: P[0] by A1; for i being Nat holds P[i] from NAT_1:sch 2(A71,A63); hence thesis by A62; end; len (<%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0))) <= mk+1+1 & mk+1+1 < len (<%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0))) + len Stop SCM+FSA implies f.(mk+1+1)=(Stop SCM+FSA).(mk+1+1- len (<%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)))) by AFINSQ_1:18; then A72: f.(mk+1+1) = halt SCM+FSA by A42,XREAL_1:29; CurInstr(P,Comput(P,s,mk+1+1)) = P.IC Comput(P,s,mk+1+1) by A2,PARTFUN1:def 6 .= P. (mk+1+1) by A61 .= halt SCM+FSA by A72,A47; hence thesis by EXTPRO_1:29; end; end; registration let a be Int-Location, k be Integer; cluster a := k -> parahalting; correctness proof A1: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15; let s be 0-started State of SCM+FSA; A2: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29; let P be Instruction-Sequence of SCM+FSA such that A3: a := k c= P; IC s = IC Start-At(0,SCM+FSA) by A2,A1,GRFUNC_1:2 .= 0; hence P halts_on s by Lm1,A3; end; end; theorem for s being State of SCM+FSA for a being read-write Int-Location, k being Integer holds IExec(a := k,P,s).a = k & (for b being read-write Int-Location st b <> a holds IExec(a := k,P,s).b = s.b) & for f being FinSeq-Location holds IExec(a := k,P,s).f = s.f proof let s be State of SCM+FSA; let a be read-write Int-Location; let k be Integer; set s1 = s +* Initialize((intloc 0).-->1); A1: s1.intloc 0 = (Initialize((intloc 0).-->1)).intloc 0 by FUNCT_4:13,SCMFSA_M:10 .= 1 by SCMFSA_M:12; reconsider s1 as 0-started State of SCM+FSA; A2: a := k c= P+*(a:=k) by FUNCT_4:25; thus IExec(a := k,P,s).a = (Result(P+*(a:=k),s1)).a .= k by A1,A2,SCMFSA_7:6; hereby let b be read-write Int-Location; assume A3: b <> a; b <> intloc 0 & b <> IC SCM+FSA by SCMFSA_2:56; then A4: not b in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2; thus IExec(a := k,P,s).b = (Result(P+*(a:=k),s1)).b .= s1.b by A1,A2,A3,SCMFSA_7:6 .= s.b by A4,FUNCT_4:11; end; let f be FinSeq-Location; f <> intloc 0 & f <> IC SCM+FSA by SCMFSA_2:57,58; then A5: not f in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2; thus IExec(a := k,P,s).f = (Result(P+*(a:=k),s1)).f .= s1.f by A1,A2,SCMFSA_7:6 .= s.f by A5,FUNCT_4:11; end; Lm2: for p1,p2,p3,p4 being XFinSequence holds p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3 ^ p4) proof let p1,p2,p3,p4 be XFinSequence; thus p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3) ^ p4 by AFINSQ_1:27 .= p1 ^ (p2 ^ p3 ^ p4) by AFINSQ_1:27; end; Lm3: for c0 being Element of NAT for s being c0-started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for a being Int-Location, k being Integer st for c being Element of NAT st c < len aSeq(a,k) holds aSeq(a,k).c = P. (c0 + c) for i being Element of NAT st i <= len aSeq(a,k) holds IC Comput(P,s,i) = c0 + i proof let c0 be Element of NAT; let s be c0-started State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; A1: dom P = NAT by PARTFUN1:def 2; A2: IC s = c0 by MEMSTR_0:def 12; let a be Int-Location; let k be Integer; assume A3: for c being Element of NAT st c < len aSeq(a,k) holds aSeq(a,k).c = P. (c0 + c); A4: for c being Element of NAT st c in dom aSeq(a,k) holds aSeq(a,k).c = P.(c0 + c) by A3,AFINSQ_1:66; per cases; suppose A5: k > 0; then reconsider k9= k as Element of NAT by INT_1:3; consider k1 being Nat such that A6: k1 + 1 = k9 and A7: aSeq(a,k9) = <%a:=intloc 0%> ^ (k1 --> AddTo(a,intloc 0)) by A5, SCMFSA_7:def 2; defpred Q[Nat] means $1 <= k9 implies IC Comput(P,s,$1) = (c0 + $1); A8: len aSeq(a,k9) = len <%a:=intloc 0%> + len (k1-->AddTo(a,intloc 0)) by A7, AFINSQ_1:17 .= 1 + len(k1-->AddTo(a,intloc 0)) by AFINSQ_1:34 .= k9 by A6; for i being Element of NAT st i <= len aSeq(a,k9) holds IC Comput(P,s,i) = (c0 + i) proof A9: now let i be Element of NAT; assume that A10: 1 <= i and A11: i < k9; reconsider i1 = i - 1 as Element of NAT by A10,INT_1:5; i = i1 + 1; then i1 < k1 by A11,A6,XREAL_1:6; then A12: i1 in Segm k1 by NAT_1:44; A13: len (k1 --> AddTo(a,intloc 0)) = k1; len <% a:= intloc 0 %> = 1 by AFINSQ_1:33; hence aSeq(a,k9).i = (k1 --> AddTo(a,intloc 0)).(i - 1) by A10,A7,A13,A6,A11,AFINSQ_1:18 .= AddTo(a,intloc 0) by A12,FUNCOP_1:7; end; A14: for i being Element of NAT st i < k9 holds i in dom aSeq(a,k9) by A8,AFINSQ_1:86; A15: now let i be Nat; assume that A16: 0 < i and A17: i < k9; A18: 0+1 <= i by A16,NAT_1:13; A19: i in NAT by ORDINAL1:def 12; hence P. (c0 + i) = aSeq(a,k9).(i) by A4,A14,A17 .=AddTo(a,intloc 0) by A9,A18,A17,A19; end; A20: P. (c0 + 0) = aSeq(a,k9).0 by A3,A5,A8 .= a:= intloc 0 by A7,AFINSQ_1:35; A21: now let n be Element of NAT; assume n = 0; hence A22: Comput(P,s,n) = s; thus CurInstr(P,Comput(P,s,n)) = P.IC Comput(P,s,n) by A1,PARTFUN1:def 6 .= a:= intloc 0 by A20,A22,MEMSTR_0:def 12; thus Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3 .= Exec(a:= intloc 0,s) by A22,A2,A20,A1,PARTFUN1:def 6; end; A23: for n being Nat st Q[n] holds Q[n + 1] proof let n be Nat; assume A24: Q[n]; assume A25: n + 1 <= k9; per cases; suppose A26: n = 0; hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A21 .= c0 + 1 + n by A2,A26,SCMFSA_2:63 .= c0 + (n + 1); end; suppose A27: n > 0; A28: n < k9 by A25,NAT_1:13; A29: n + 0 <= n + 1 by XREAL_1:7; A30: CurInstr(P,Comput(P,s,n)) = P.(c0 + n) by A24,A25,A29,A1,PARTFUN1:def 6,XXREAL_0:2 .= AddTo(a,intloc 0) by A15,A27,A28; A31: Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3 .= Exec(AddTo(a,intloc 0), Comput(P,s,n)) by A30; thus IC Comput(P,s,n+1) = IC Comput(P,s,n) + 1 by A31,SCMFSA_2:64 .= (c0 + n + 1) by A24,A25,A29,XXREAL_0:2 .= (c0 + (n + 1)); end; end; let i be Element of NAT; assume A32: i <= len aSeq(a,k9); A33: Q[0] by A2; for i being Nat holds Q[i] from NAT_1:sch 2(A33,A23); hence thesis by A8,A32; end; hence thesis; end; suppose A34: k <= 0; then reconsider mk = - k as Element of NAT by INT_1:3; defpred Q[Nat] means $1 <= mk+1+1 implies IC Comput(P,s,$1) = (c0 + $1); consider k1 being Nat such that A35: k1 + k = 1 and A36: aSeq(a,k) = <%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) by A34, SCMFSA_7:def 2; A37: len aSeq(a,k) = len <% a:=intloc 0 %> + len (k1-->SubFrom(a,intloc 0) ) by A36,AFINSQ_1:17 .= 1 + len (k1-->SubFrom(a,intloc 0)) by AFINSQ_1:34 .= mk+1+1 by A35; for i being Element of NAT st i <= len aSeq(a,k) holds IC Comput( P,s,i) = (c0 + i) proof A38: now let i be Element of NAT; assume that A39: 1 <= i and A40: i < mk+1+1; A41: i - 1 < mk+1+1 - 1 by A40,XREAL_1:9; reconsider i1 = i - 1 as Element of NAT by A39,INT_1:5; A42: i1 in Segm k1 by A35,A41,NAT_1:44; A43: len(k1 --> SubFrom(a,intloc 0)) = k1; len <% a:= intloc 0 %> = 1 by AFINSQ_1:33; hence aSeq(a,k).i = (k1-->SubFrom(a,intloc 0)).(i - 1) by A36,A39,A43,A35,A40,AFINSQ_1:18 .= SubFrom(a,intloc 0) by A42,FUNCOP_1:7; end; A44: for i being Element of NAT st i < mk+1+1 holds i in dom aSeq(a,k) by A37,AFINSQ_1:86; A45: now let i be Nat; assume that A46: 0 < i and A47: i < mk+1+1; A48: 0+1 <= i by A46,NAT_1:13; A49: i in NAT by ORDINAL1:def 12; hence P. (c0 + i) = aSeq(a,k).(i) by A4,A44,A47 .=SubFrom(a,intloc 0) by A38,A48,A47,A49; end; A50: P. (c0 + 0) = aSeq(a,k).0 by A3,A37 .= a:= intloc 0 by A36,AFINSQ_1:35; A51: for n being Element of NAT st n = 0 holds Comput(P,s,n) = s & CurInstr(P,Comput(P,s,n)) = a:= intloc 0 & Comput(P,s,n+1) = Exec(a:= intloc 0,s) proof let n be Element of NAT; assume n = 0; hence A52: Comput(P,s,n) = s; thus CurInstr(P,Comput(P,s,n)) = P.IC Comput(P,s,n) by A1,PARTFUN1:def 6 .= a:= intloc 0 by A50,A52,MEMSTR_0:def 12; thus Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3 .= Exec(a:= intloc 0,s) by A52,A2,A50,A1,PARTFUN1:def 6; end; A53: for n being Nat st Q[n] holds Q[n + 1] proof let n be Nat; assume A54: Q[n]; assume A55: n + 1 <= mk+1+1; per cases; suppose A56: n = 0; hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A51 .= (c0 + n)+1 by A2,A56,SCMFSA_2:63 .= c0 + (n + 1); end; suppose A57: n > 0; A58: n < mk+1+1 by A55,NAT_1:13; A59: n + 0 <= n + 1 by XREAL_1:7; A60: CurInstr(P,Comput(P,s,n)) = P. (c0 + n) by A54,A55,A59,A1,PARTFUN1:def 6,XXREAL_0:2 .= SubFrom(a,intloc 0) by A45,A57,A58; A61: Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3 .= Exec(SubFrom(a,intloc 0), Comput(P,s,n)) by A60; thus IC Comput(P,s,n+1) = IC Comput(P,s,n)+1 by A61,SCMFSA_2:65 .= c0 + n + 1 by A54,A55,A59,XXREAL_0:2 .= c0 + (n + 1); end; end; let i be Element of NAT; assume A62: i <= len aSeq(a,k); A63: Q[0] by A2; for i being Nat holds Q[i] from NAT_1:sch 2(A63,A53); hence thesis by A37,A62; end; hence thesis; end; end; Lm4: for s being 0-started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for a being Int-Location, k being Integer st aSeq(a,k) c= P for i being Element of NAT st i <= len aSeq(a,k) holds IC Comput(P,s,i) = i proof let s be 0-started State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; let a be Int-Location; let k be Integer; assume A1: aSeq(a,k) c= P; A2: for c being Element of NAT st c < len aSeq(a,k) holds P.(0+c) = ( aSeq(a,k)). c by A1,AFINSQ_1:86,GRFUNC_1:2; let i be Element of NAT; assume i <= len aSeq(a,k); then IC Comput(P,s,i) = (0+i) by A2,Lm3; hence thesis; end; Lm5: for s being 0-started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for f being FinSeq-Location, p being FinSequence of INT st f := p c= P holds P halts_on s proof set a2 = intloc 2; set a1 = intloc 1; let s be 0-started State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; A1: dom P = NAT by PARTFUN1:def 2; set D = the InstructionsF of SCM+FSA; let f be FinSeq-Location; let p be FinSequence of INT; set q = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %> ^ aSeq(f,p) ^ Stop SCM+FSA; set q0 = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %>; assume A2: f := p c= P; set q = aSeq(a1,len p)^<% f:=<0,...,0>a1 %>^aSeq(f,p)^Stop SCM+FSA; A3: for i,k being Element of NAT st i < len q holds P. i = q.(i) by A2,AFINSQ_1:86,GRFUNC_1:2; consider pp being XFinSequence of D^omega such that A4: len pp = len p & for k being Nat st k < len pp ex i being Integer st i = p.(k+1) & pp.k = (aSeq(a1,k+1) ^ aSeq(a2,i) ^ <% (f,a1):= a2 %>) and A5: aSeq(f,p) = FlattenSeq pp by SCMFSA_7:def 3; len q = len (q0 ^ FlattenSeq pp) + 1 by A5,AFINSQ_1:75; then A6: len (q0 ^ FlattenSeq pp) < len q by NAT_1:13; defpred P[XFinSequence] means $1 c= pp implies ex pp0 being XFinSequence of D^omega st (pp0 = $1 & for i being Element of NAT st i <= len (q0 ^ FlattenSeq pp0) holds IC Comput(P,s,i) = i); A7: for r being XFinSequence, x being object st P[r] holds P[r ^ <% x %>] proof let r be XFinSequence; let x be object; assume A8: P[r]; set r1 = len r; len<% x %> =1 by AFINSQ_1:34; then len (r ^ <% x %>) = r1+1 by AFINSQ_1:17; then r1 < len (r ^ <% x %>) by XREAL_1:29; then A9: r1 in dom (r ^ <% x %>) by AFINSQ_1:86; assume A10: r ^ <% x %> c= pp; then A11: dom (r ^ <% x %>) c= dom pp by GRFUNC_1:2; then r1 < len pp by A9,AFINSQ_1:86; then consider pr1 being Integer such that pr1 = p.(r1+1) and A12: pp.r1 = aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %> by A4; r c= r ^ <% x %> by AFINSQ_1:74; then consider pp0 being XFinSequence of D^omega such that A13: pp0 = r and A14: for i being Element of NAT st i <= len (q0 ^ FlattenSeq pp0) holds IC Comput(P,s,i) = i by A8,A10,XBOOLE_1:1; set c2 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)); set c1 = len (q0 ^ FlattenSeq pp0); IC Comput(P,s,c1) = c1 by A14; then reconsider s1 = Comput(P,s,c1) as c1-started State of SCM+FSA by MEMSTR_0:def 12; A15: x = (r ^ <% x %>).r1 by AFINSQ_1:36 .= pp.r1 by A10,A9,GRFUNC_1:2; then x in D^omega by A9,A11,FUNCT_1:102; then reconsider pp1 = pp0 ^ <% x %> as XFinSequence of D^omega; take pp1; thus pp1 = r ^ <% x %> by A13; reconsider x as Element of D^omega by A9,A11,A15,FUNCT_1:102; A16: FlattenSeq pp1 = FlattenSeq pp0 ^ FlattenSeq <% x %> by AFINSQ_2:75 .= FlattenSeq pp0 ^ x by AFINSQ_2:73; set s2 = Comput(P,s,c2); A17: x = aSeq(a1,r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by A12,A15,AFINSQ_1:27; then A18: len q0 + len FlattenSeq pp1 = len q0 + len (FlattenSeq pp0 ^ aSeq(a1, r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1):=a2 %>)) by A16,AFINSQ_1:27 .= len (q0 ^ (FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1) :=a2 %>))) by AFINSQ_1:17 .= len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1) :=a2 %>)) by Lm2 .= c2 + len (aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by AFINSQ_1:17 .= c2 + (len aSeq(a2,pr1) + len <% (f,a1):=a2 %>) by AFINSQ_1:17 .= c2 + (len aSeq(a2,pr1) + 1) by AFINSQ_1:34 .= c2 + len aSeq(a2,pr1) + 1; then A19: len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(a2,pr1) + 1 by AFINSQ_1:17; then A20: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(a2,pr1) by NAT_1:13; A21: FlattenSeq pp1 c= FlattenSeq pp by A10,A13,AFINSQ_2:82; A22: now let p be XFinSequence; assume p c= x; then FlattenSeq pp0 ^ p c= FlattenSeq pp0 ^ x by AFINSQ_2:81; then FlattenSeq pp0 ^ p c= FlattenSeq pp by A21,A16; then q0 ^ (FlattenSeq pp0 ^ p) c= q0 ^ FlattenSeq pp by AFINSQ_2:81; then A23: q0 ^ FlattenSeq pp0 ^ p c= q0 ^ FlattenSeq pp by AFINSQ_1:27; q0 ^ FlattenSeq pp c= q by A5,AFINSQ_1:74; hence q0 ^ FlattenSeq pp0 ^ p c= q by A23; end; A24: for c being Element of NAT st c < len aSeq(a1,r1+1) holds aSeq(a1,r1+1).c = P.(c1 + c) proof let c be Element of NAT; assume c < len aSeq(a1,r1+1); then A25: c in dom aSeq(a1,r1+1) by AFINSQ_1:66; then A26: c1 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)) by AFINSQ_1:23; A27: q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) c= q by A17,A22,AFINSQ_1:74; then A28: dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)) c= dom q by GRFUNC_1:2; thus aSeq(a1,r1+1).c = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)).(c1 + c) by A25,AFINSQ_1:def 3 .= q.(c1 + c) by A27,A26,GRFUNC_1:2 .= P. (c1 + c) by A2,A28,A26,GRFUNC_1:2; end; set c3 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)); A29: c2 = c1 + len aSeq(a1,r1+1) by AFINSQ_1:17; A30: q0 ^ FlattenSeq pp1 = q0 ^ FlattenSeq pp0 ^ x by A16,AFINSQ_1:27; then len (q0 ^ FlattenSeq pp1) <= len q by A22,NAT_1:43; then A31: c2 + len aSeq(a2,pr1) < len q by A19,NAT_1:13; A32: c3 = c2 + len aSeq(a2,pr1) by AFINSQ_1:17; A33: Comput(P,s,c2) = Comput(P,s1, len aSeq(a1,r1+1)) by A29,EXTPRO_1:4; IC Comput(P,s,c2) = c2 by A29,A33,A24,Lm3; then reconsider s2 as c2-started State of SCM+FSA by MEMSTR_0:def 12; A34: for c being Element of NAT st c < len aSeq(a2,pr1) holds aSeq(a2,pr1).c = P.(c2+ c) proof let c be Element of NAT; assume c < len aSeq(a2,pr1); then A35: c in dom aSeq(a2,pr1) by AFINSQ_1:66; then A36: c2 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)) by AFINSQ_1:23; q0 ^ FlattenSeq pp0 ^ (aSeq(a1,r1+1) ^ aSeq(a2,pr1)) c= q by A12,A15,A22, AFINSQ_1:74; then A37: q0 ^FlattenSeq pp0^aSeq(a1,r1+1) ^ aSeq(a2,pr1) c= q by AFINSQ_1:27; then A38: dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)) c= dom q by GRFUNC_1:2; thus aSeq(a2,pr1).c = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)).(c2 + c) by A35,AFINSQ_1:def 3 .= q.(c2 + c) by A36,A37,GRFUNC_1:2 .= P. (c2 + c) by A2,A38,A36,GRFUNC_1:2; end; A39: now let i be Element of NAT; assume i <= len aSeq(a2,pr1); hence c2 + i = IC Comput(P,s2,i) by A34,Lm3 .= IC Comput(P,s,c2+i) by EXTPRO_1:4; end; A40: now let i be Element of NAT; assume i <= len aSeq(a1,r1+1); hence c1 + i = IC Comput(P,s1,i) by A24,Lm3 .= IC Comput(P,s,c1 + i) by EXTPRO_1:4; end; A41: for i being Element of NAT st i < len (q0 ^ FlattenSeq pp1) holds IC Comput(P,s,i) = i proof let i be Element of NAT; assume A42: i < len (q0 ^ FlattenSeq pp1); A43: now A44: i < len q0 + len FlattenSeq pp1 by A42,AFINSQ_1:17; assume A45: not i <= c1; assume not (c1 + 1 <= i & i <= c2); hence c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1) by A18,A45,A44,NAT_1:13; end; per cases by A43; suppose i <= len (q0 ^ FlattenSeq pp0); hence thesis by A14; end; suppose A46: c1 + 1 <= i & i <= c2; then c1 + 1 - c1 <= i - c1 by XREAL_1:9; then reconsider ii = i - c1 as Element of NAT by INT_1:3; i - c1 <= c2 - c1 by A46,XREAL_1:9; hence i = IC Comput(P,s,c1+ii) by A29,A40 .= IC Comput(P,s,i); thus thesis; end; suppose A47: c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1); then c2 + 1 - c2 <= i - c2 by XREAL_1:9; then reconsider ii = i - c2 as Element of NAT by INT_1:3; i - c2 <= c2 + len aSeq(a2,pr1) - c2 by A47,XREAL_1:9; hence i = IC Comput(P,s,c2+ii)by A39 .= IC Comput(P,s,i); end; end; q0 ^ FlattenSeq pp0 ^ x c= q by A22; then consider rq being XFinSequence of D such that A48: (q0 ^ FlattenSeq pp0 ^ x)^rq = q by AFINSQ_2:80; len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(a2,pr1) + 1 by A18,AFINSQ_1:17; then A49: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(a2,pr1) by NAT_1:13; then A50: c3 in dom(q0 ^ FlattenSeq pp0 ^ x) by A30,A32,AFINSQ_1:66; dom<% (f,a1):=a2 %> = 1 by AFINSQ_1:33; then A51: 0 in dom<% (f,a1):=a2 %> by CARD_1:49,TARSKI:def 1; len<% (f,a1):=a2 %> = 1 by AFINSQ_1:34; then len(aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) = len (aSeq(a1,r1+1) ^ aSeq(a2,pr1)) + 1 by AFINSQ_1:17; then len (aSeq(a1,r1+1) ^ aSeq(a2,pr1)) < len(aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by XREAL_1:29; then A52: len (aSeq(a1,r1+1) ^ aSeq(a2,pr1)) in dom(aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by AFINSQ_1:66; A53: c3 = c1 + len aSeq(a1,r1+1) + len aSeq(a2,pr1) by A29,AFINSQ_1:17; A54: (P)/.IC Comput(P,s,c3) = P.IC Comput(P,s,c3) by A1,PARTFUN1:def 6; CurInstr(P,Comput(P,s,c3)) = P. c3 by A32,A41,A54,A49 .= q.(c3 ) by A3,A32,A31 .= (q0 ^ FlattenSeq pp0 ^ x). (c1 + (len aSeq(a1,r1+1) + (len aSeq(a2,pr1)))) by A53,A50,A48,AFINSQ_1:def 3 .= (q0 ^ FlattenSeq pp0 ^ x). (c1 + len(aSeq(a1,r1+1) ^ aSeq(a2,pr1))) by AFINSQ_1:17; then A55: CurInstr(P,Comput(P,s,c3)) = (aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>). (len (aSeq(a1,r1+1) ^ aSeq(a2,pr1))+0) by A52,A12,A15,AFINSQ_1:def 3 .= <% (f,a1):=a2 %>.0 by A51,AFINSQ_1:def 3 .= (f,a1):=a2; Comput(P,s,c3+1) = Following(P,Comput(P,s, c3)) by EXTPRO_1:3 .= Exec((f,a1):=a2, Comput(P,s,c3)) by A55; then A56: IC Comput(P,s,len (q0 ^ FlattenSeq pp1)) = Exec((f,a1):=a2, Comput(P,s,c3)).IC SCM+FSA by A19,AFINSQ_1:17 .= IC Comput(P,s,c3)+1 by SCMFSA_2:73 .= c3+1 by A32,A41,A20; thus for i being Element of NAT st i <= len (q0 ^ FlattenSeq pp1) holds IC Comput(P,s,i) = i proof let i be Element of NAT; assume A57: i <= len (q0 ^ FlattenSeq pp1); per cases by A57,XXREAL_0:1; suppose i < len (q0 ^ FlattenSeq pp1); hence thesis by A41; end; suppose i = len (q0 ^ FlattenSeq pp1); hence thesis by A32,A19,A56; end; end; end; set k = len aSeq(a1,len p); A58: len q0 = k + 1 by AFINSQ_1:75; q = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %> ^ (aSeq(f,p) ^ Stop SCM+FSA) by AFINSQ_1:27 .= aSeq(a1,len p) ^ (<% f :=<0,...,0> a1 %> ^ (aSeq(f,p) ^ Stop SCM+FSA)) by AFINSQ_1:27; then A59: aSeq(a1,len p) c= f:=p by AFINSQ_1:74; A60: P[{}] proof assume {} c= pp; take <%>(D^omega); thus <%>(D^omega) = {}; A61: q = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %> ^ (aSeq(f,p) ^ Stop SCM+FSA ) by AFINSQ_1:27; then len q = len q0 + len ((aSeq(f,p) ^ Stop SCM+FSA)) by AFINSQ_1:17; then len q0 <= len q by NAT_1:11; then A62: k < len q by A58,NAT_1:13; A63: now let i be Element of NAT; assume i < len q0; then i <= len aSeq(a1,len p) by A58,NAT_1:13; hence IC Comput(P,s,i) = i by A2,A59,Lm4,XBOOLE_1:1; end; A64: k < len q0 by A58,NAT_1:13; then A65: k in dom q0 by AFINSQ_1:66; A66: IC Comput(P,s,k) = k by A63,A64; then A67: CurInstr(P,Comput(P,s,k)) = P. k by A1,PARTFUN1:def 6 .= q.k by A3,A62 .= q0.k by A61,A65,AFINSQ_1:def 3 .= f:=<0,...,0>a1 by AFINSQ_1:36; A68: Comput(P,s,len q0) = Following(P,Comput(P,s,k)) by A58,EXTPRO_1:3 .= Exec(f:=<0,...,0>a1, Comput(P,s,k)) by A67; A69: IC Comput(P,s,len q0) = IC Comput(P,s,k)+1 by A68,SCMFSA_2:75 .= len q0 by A58,A66; A70: now let i be Element of NAT; assume i <= len q0; then i < len q0 or i = len q0 by XXREAL_0:1; hence IC Comput(P,s,i) = i by A63,A69; end; q0 ^ FlattenSeq <%>(D^omega) = q0 ^ <%>D by AFINSQ_2:74 .= q0 ^ {} .= q0; hence thesis by A70; end; for r being XFinSequence holds P[r] from AFINSQ_1:sch 3(A60,A7); then ex pp0 being XFinSequence of D^omega st pp0 = pp & for i being Element of NAT st i <= len (q0 ^ FlattenSeq pp0) holds IC Comput(P,s,i) = i; then IC Comput(P,s,len (q0 ^ FlattenSeq pp)) = len (q0 ^ FlattenSeq pp); then CurInstr(P, Comput(P,s,len (q0 ^ FlattenSeq pp))) = P. len (q0 ^ FlattenSeq pp) by A1,PARTFUN1:def 6 .= q.len (q0 ^ FlattenSeq pp) by A3,A6 .= halt SCM+FSA by A5,AFINSQ_1:36; hence thesis by EXTPRO_1:29; end; registration let f be FinSeq-Location, p be FinSequence of INT; cluster f := p -> initial non empty NAT-defined (the InstructionsF of SCM+FSA)-valued; coherence; end; registration let f be FinSeq-Location, p be FinSequence of INT; cluster f := p -> parahalting; correctness by Lm5; end; theorem for s being State of SCM+FSA, f being FinSeq-Location, p being FinSequence of INT holds IExec(f := p,P,s).f = p & (for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds IExec(f := p,P,s).a = s.a) & for g being FinSeq-Location st g <> f holds IExec(f := p,P,s).g = s.g proof let s be State of SCM+FSA; let f be FinSeq-Location; let p be FinSequence of INT; A1: (s+*Initialize((intloc 0).-->1)).intloc 0 = (Initialize((intloc 0).-->1)).intloc 0 by FUNCT_4:13,SCMFSA_M:10 .= 1 by SCMFSA_M:12; reconsider s1 = s+*Initialize((intloc 0).-->1) as 0-started State of SCM+FSA; A2: (f := p) c= P+*(f:=p) by FUNCT_4:25; thus IExec(f := p,P,s).f = (Result(P+*(f := p),s1)).f .= p by A1,A2,SCMFSA_7:7; hereby let a be read-write Int-Location; a <> intloc 0 & a <> IC SCM+FSA by SCMFSA_2:56; then A3: not a in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2; assume A4: a <> intloc 1 & a <> intloc 2; thus IExec(f := p,P,s).a = (Result(P+*(f:=p),s+* Initialize((intloc 0).-->1))).a .= s1.a by A1,A2,A4,SCMFSA_7:7 .= s.a by A3,FUNCT_4:11; end; let g be FinSeq-Location; assume A5: g <> f; g <> intloc 0 & g <> IC SCM+FSA by SCMFSA_2:57,58; then A6: not g in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2; thus IExec(f := p,P,s).g = (Result(P+*(f:=p),s+*Initialize((intloc 0).-->1))).g .= s1.g by A1,A2,A5,SCMFSA_7:7 .= s.g by A6,FUNCT_4:11; end; definition let i be Instruction of SCM+FSA; let a be Int-Location; pred i refers a means not for b being Int-Location, l being Nat for f being FinSeq-Location holds b := a <> i & AddTo(b,a) <> i & SubFrom(b,a) <> i & MultBy(b,a) <> i & Divide(b,a) <> i & Divide(a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b :=(f,a) <> i & (f,b) := a <> i & (f,a):= b <> i & f :=<0,...,0> a <> i; end; definition let I be preProgram of SCM+FSA; let a be Int-Location; pred I refers a means ex i being Instruction of SCM+FSA st i in rng I & i refers a; end; definition let i be Instruction of SCM+FSA; let a be Int-Location; pred i destroys a means not for b being Int-Location for f being FinSeq-Location holds a := b <> i & AddTo(a,b) <> i & SubFrom(a,b) <> i & MultBy(a,b) <> i & Divide(a,b) <> i & Divide(b,a) <> i & a :=(f,b) <> i & a :=len f <> i; end; definition let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function; let a be Int-Location; pred I destroys a means ex i being Instruction of SCM+FSA st i in rng I & i destroys a; end; definition let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function; attr I is good means I does not destroy intloc 0; end; theorem for a being Int-Location holds halt SCM+FSA does not destroy a; theorem Th6: for a,b,c being Int-Location holds a <> b implies b := c does not destroy a proof let a,b,c be Int-Location; assume A1: a <> b; now let e be Int-Location; let l be Element of NAT; let f be FinSeq-Location; thus a := e <> b := c by A1,SF_MASTR:1; A2: InsCode (b := c) = 1 by SCMFSA_2:18; hence AddTo(a,e) <> b := c by SCMFSA_2:19; thus SubFrom(a,e) <> b := c by A2,SCMFSA_2:20; thus MultBy(a,e) <> b := c by A2,SCMFSA_2:21; thus Divide(a,e) <> b := c & Divide(e,a) <> b := c by A2,SCMFSA_2:22; thus a :=(f,e) <> b := c by A2,SCMFSA_2:26; thus a :=len f <> b := c by A2,SCMFSA_2:28; end; hence thesis; end; theorem Th7: for a,b,c being Int-Location holds a <> b implies AddTo(b,c) does not destroy a proof let a,b,c be Int-Location; assume A1: a <> b; now let e be Int-Location; let l be Element of NAT; let f be FinSeq-Location; A2: InsCode AddTo(b,c) = 2 by SCMFSA_2:19; hence a := e <> AddTo(b,c) by SCMFSA_2:18; thus AddTo(a,e) <> AddTo(b,c) by A1,SF_MASTR:2; thus SubFrom(a,e) <> AddTo(b,c) by A2,SCMFSA_2:20; thus MultBy(a,e) <> AddTo(b,c) by A2,SCMFSA_2:21; thus Divide(a,e) <> AddTo(b,c) & Divide(e,a) <> AddTo(b,c) by A2, SCMFSA_2:22; thus a :=(f,e) <> AddTo(b,c) by A2,SCMFSA_2:26; thus a :=len f <> AddTo(b,c) by A2,SCMFSA_2:28; end; hence thesis; end; theorem Th8: for a,b,c being Int-Location holds a <> b implies SubFrom(b,c) does not destroy a proof let a,b,c be Int-Location; assume A1: a <> b; now let e be Int-Location; let l be Element of NAT; let f be FinSeq-Location; A2: InsCode SubFrom(b,c) = 3 by SCMFSA_2:20; hence a := e <> SubFrom(b,c) by SCMFSA_2:18; thus AddTo(a,e) <> SubFrom(b,c) by A2,SCMFSA_2:19; thus SubFrom(a,e) <> SubFrom(b,c) by A1,SF_MASTR:3; thus MultBy(a,e) <> SubFrom(b,c) by A2,SCMFSA_2:21; thus Divide(a,e) <> SubFrom(b,c) & Divide(e,a) <> SubFrom(b,c) by A2, SCMFSA_2:22; thus a :=(f,e) <> SubFrom(b,c) by A2,SCMFSA_2:26; thus a :=len f <> SubFrom(b,c) by A2,SCMFSA_2:28; end; hence thesis; end; theorem for a,b,c being Int-Location holds a <> b implies MultBy(b,c) does not destroy a proof let a,b,c be Int-Location; assume A1: a <> b; now let e be Int-Location; let l be Element of NAT; let f be FinSeq-Location; A2: InsCode MultBy(b,c) = 4 by SCMFSA_2:21; hence a := e <> MultBy(b,c) by SCMFSA_2:18; thus AddTo(a,e) <> MultBy(b,c) by A2,SCMFSA_2:19; thus SubFrom(a,e) <> MultBy(b,c) by A2,SCMFSA_2:20; thus MultBy(a,e) <> MultBy(b,c) by A1,SF_MASTR:4; thus Divide(a,e) <> MultBy(b,c) & Divide(e,a) <> MultBy(b,c) by A2, SCMFSA_2:22; thus a :=(f,e) <> MultBy(b,c) by A2,SCMFSA_2:26; thus a :=len f <> MultBy(b,c) by A2,SCMFSA_2:28; end; hence thesis; end; theorem for a,b,c being Int-Location holds a <> b & a <> c implies Divide(b,c) does not destroy a proof let a,b,c be Int-Location; assume A1: a <> b & a <> c; now let e be Int-Location; let l be Element of NAT; let h be FinSeq-Location; A2: InsCode Divide(b,c) = 5 by SCMFSA_2:22; hence a := e <> Divide(b,c) by SCMFSA_2:18; thus AddTo(a,e) <> Divide(b,c) by A2,SCMFSA_2:19; thus SubFrom(a,e) <> Divide(b,c) by A2,SCMFSA_2:20; thus MultBy(a,e) <> Divide(b,c) by A2,SCMFSA_2:21; thus Divide(e,a) <> Divide(b,c) & Divide(a,e) <> Divide(b,c) by A1, SF_MASTR:5; thus a := (h,e) <> Divide(b,c) by A2,SCMFSA_2:26; thus a :=len h <> Divide(b,c) by A2,SCMFSA_2:28; end; hence thesis; end; theorem for a being Int-Location, l being Nat holds goto l does not destroy a; theorem for a,b being Int-Location, l being Nat holds b =0_goto l does not destroy a; theorem for a,b being Int-Location, l being Nat holds b >0_goto l does not destroy a; theorem for a,b,c being Int-Location, f being FinSeq-Location holds a <> b implies b := (f,c) does not destroy a proof let a,b,c be Int-Location; let f be FinSeq-Location; assume A1: a <> b; now let e be Int-Location; let l be Element of NAT; let h be FinSeq-Location; A2: InsCode (b := (f,c)) = 9 by SCMFSA_2:26; hence a := e <> b := (f,c) by SCMFSA_2:18; thus AddTo(a,e) <> b := (f,c) by A2,SCMFSA_2:19; thus SubFrom(a,e) <> b := (f,c) by A2,SCMFSA_2:20; thus MultBy(a,e) <> b := (f,c) by A2,SCMFSA_2:21; thus Divide(a,e) <> b := (f,c) & Divide(e,a) <> b := (f,c) by A2, SCMFSA_2:22; thus a := (h,e) <> b := (f,c) by A1,SF_MASTR:9; thus a :=len h <> b := (f,c) by A2,SCMFSA_2:28; end; hence thesis; end; theorem for a,b,c being Int-Location, f being FinSeq-Location holds (f,c):= b does not destroy a proof let a,b,c be Int-Location; let f be FinSeq-Location; now let e be Int-Location; let h be FinSeq-Location; A1: InsCode ((f,c) := b) = 10 by SCMFSA_2:27; hence a := e <> (f,c) := b by SCMFSA_2:18; thus AddTo(a,e) <> (f,c) := b by A1,SCMFSA_2:19; thus SubFrom(a,e) <> (f,c) := b by A1,SCMFSA_2:20; thus MultBy(a,e) <> (f,c) := b by A1,SCMFSA_2:21; thus Divide(e,a) <> (f,c) := b & Divide(a,e) <> (f,c) := b by A1, SCMFSA_2:22; thus a := (h,e) <> (f,c) := b by A1,SCMFSA_2:26; thus a :=len h <> (f,c) := b by A1,SCMFSA_2:28; end; hence thesis; end; theorem for a,b being Int-Location, f being FinSeq-Location holds a <> b implies b :=len f does not destroy a proof let a,b be Int-Location; let f be FinSeq-Location; assume A1: a <> b; now let c be Int-Location; let g be FinSeq-Location; A2: InsCode (b :=len f) = 11 by SCMFSA_2:28; hence a := c <> b :=len f by SCMFSA_2:18; thus AddTo(a,c) <> b :=len f by A2,SCMFSA_2:19; thus SubFrom(a,c) <> b :=len f by A2,SCMFSA_2:20; thus MultBy(a,c) <> b :=len f by A2,SCMFSA_2:21; thus Divide(a,c) <> b :=len f & Divide(c,a) <> b :=len f by A2,SCMFSA_2:22; thus a :=(g,c) <> b :=len f by A2,SCMFSA_2:26; thus a :=len g <> b :=len f by A1,SF_MASTR:11; end; hence thesis; end; theorem for a,b being Int-Location, f being FinSeq-Location holds f:=<0,...,0> b does not destroy a proof let a,b be Int-Location; let f be FinSeq-Location; now let e be Int-Location; let h be FinSeq-Location; A1: InsCode (f :=<0,...,0> b) = 12 by SCMFSA_2:29; hence a := e <> f :=<0,...,0> b by SCMFSA_2:18; thus AddTo(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:19; thus SubFrom(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:20; thus MultBy(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:21; thus Divide(a,e) <> f :=<0,...,0> b & Divide(e,a) <> f :=<0,...,0> b by A1, SCMFSA_2:22; thus a :=(h,e) <> f :=<0,...,0> b by A1,SCMFSA_2:26; thus a :=len h <> f :=<0,...,0> b by A1,SCMFSA_2:28; end; hence thesis; end; ::$CD definition let I be Program of SCM+FSA; let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; pred I is_halting_on s,P means P +* I halts_on Initialize s; end; ::$CT theorem for I being Program of SCM+FSA holds I is parahalting iff for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P proof set SAt = Start-At(0,SCM+FSA); let I be Program of SCM+FSA; thus I is parahalting implies for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P by FUNCT_4:25; assume A1: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P; let s be 0-started State of SCM+FSA; A2: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29; let P be Instruction-Sequence of SCM+FSA such that A3: I c= P; A4: P = P+*I by A3,FUNCT_4:98; A5: Initialize s = s by A2,FUNCT_4:98; I is_halting_on s,P by A1; hence P halts_on s by A4,A5; end; theorem Th19: for i being Instruction of SCM+FSA, a being Int-Location, s being State of SCM+FSA st i does not destroy a holds Exec(i,s).a = s.a proof let i be Instruction of SCM+FSA; let a be Int-Location; let s be State of SCM+FSA; assume A1: i does not destroy a; InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16; then per cases; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:95; hence thesis by EXTPRO_1:def 3; end; suppose InsCode i = 1; then consider da,db being Int-Location such that A2: i = da := db by SCMFSA_2:30; da <> a by A1,A2; hence thesis by A2,SCMFSA_2:63; end; suppose InsCode i = 2; then consider da, db being Int-Location such that A3: i = AddTo(da,db) by SCMFSA_2:31; da <> a by A1,A3; hence thesis by A3,SCMFSA_2:64; end; suppose InsCode i = 3; then consider da, db being Int-Location such that A4: i = SubFrom(da, db) by SCMFSA_2:32; da <> a by A1,A4; hence thesis by A4,SCMFSA_2:65; end; suppose InsCode i = 4; then consider da, db being Int-Location such that A5: i = MultBy(da,db) by SCMFSA_2:33; da <> a by A1,A5; hence thesis by A5,SCMFSA_2:66; end; suppose InsCode i = 5; then consider da, db being Int-Location such that A6: i = Divide(da, db) by SCMFSA_2:34; da <> a & db <> a by A1,A6; hence thesis by A6,SCMFSA_2:67; end; suppose InsCode i = 6; then ex loc being Nat st i = goto loc by SCMFSA_2:35; hence thesis by SCMFSA_2:69; end; suppose InsCode i = 7; then ex loc being Nat, da being Int-Location st i = da=0_goto loc by SCMFSA_2:36; hence thesis by SCMFSA_2:70; end; suppose InsCode i = 8; then ex loc being Nat, da being Int-Location st i = da>0_goto loc by SCMFSA_2:37; hence thesis by SCMFSA_2:71; end; suppose InsCode i = 9; then consider db, da being Int-Location, g being FinSeq-Location such that A7: i = da := (g,db) by SCMFSA_2:38; da <> a by A1,A7; hence thesis by A7,SCMFSA_2:72; end; suppose InsCode i = 10; then ex db, da being Int-Location, g being FinSeq-Location st i = (g,db):= da by SCMFSA_2:39; hence thesis by SCMFSA_2:73; end; suppose InsCode i = 11; then consider da being Int-Location, g being FinSeq-Location such that A8: i = da :=len g by SCMFSA_2:40; da <> a by A1,A8; hence thesis by A8,SCMFSA_2:74; end; suppose InsCode i = 12; then ex da being Int-Location, g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:41; hence thesis by SCMFSA_2:75; end; end; theorem Th20: for s being State of SCM+FSA, P being Instruction-Sequence of SCM+FSA, I being really-closed Program of SCM+FSA, a being Int-Location st I does not destroy a :::& I is_closed_on s,P for k being Nat holds Comput(P +* I,Initialize s,k).a = s.a proof let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; let I be really-closed Program of SCM+FSA; let a be Int-Location; assume A1: I does not destroy a; defpred P[Nat] means Comput(P+*I,Initialize s,$1).a = s.a; A2: I c= P+*I by FUNCT_4:25; ::: assume :::A3: I is_closed_on s,P; A3: now let k be Nat; assume A4: P[k]; set l = IC Comput(P+*I,Initialize s,k); IC Initialize s = 0 by MEMSTR_0:47; then IC Initialize s in dom I by AFINSQ_1:65; then A5: l in dom I by A2,AMISTD_1:21; then (P+*I).l = I.l by A2,GRFUNC_1:2; then (P+*I).l in rng I by A5,FUNCT_1:def 3; then A6: (P+*I).l does not destroy a by A1; A7: dom(P+*I) = NAT by PARTFUN1:def 2; Comput(P+*I,(Initialize s),k + 1).a = (Following(P+*I,Comput(P+*I,(Initialize s),k))).a by EXTPRO_1:3 .=(Exec((P+*I). IC Comput(P+*I,Initialize s,k), Comput(P+*I,Initialize s,k))).a by A7,PARTFUN1:def 6 .= Comput(P+*I,s+* Start-At(0,SCM+FSA),k).a by A6,Th19 .= s.a by A4; hence P[k+1]; end; A8: not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102; Comput(P+*I,Initialize s,0).a = (Initialize s).a .= s.a by A8,FUNCT_4:11; then A9: P[0]; thus for k being Nat holds P[k] from NAT_1:sch 2(A9, A3); end; registration cluster Stop SCM+FSA -> parahalting good; coherence proof thus Stop SCM+FSA is parahalting proof A1: 0 in dom Stop SCM+FSA by AFINSQ_1:65; A2: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15; let s be 0-started State of SCM+FSA; A3: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29; let P be Instruction-Sequence of SCM+FSA such that A4: Stop SCM+FSA c= P; A5: dom P = NAT by PARTFUN1:def 2; CurInstr(P,Comput(P,s,0)) = CurInstr(P,s) .= P.IC s by A5,PARTFUN1:def 6 .= P.(IC Start-At(0,SCM+FSA)) by A3,A2,GRFUNC_1:2 .= P. 0 .= (Stop SCM+FSA). 0 by A1,A4,GRFUNC_1:2 .= halt SCM+FSA; hence thesis by EXTPRO_1:29; end; thus Stop SCM+FSA does not destroy intloc 0 proof now let i be Instruction of SCM+FSA; A6: rng Stop SCM+FSA = {halt SCM+FSA} by AFINSQ_1:33; assume i in rng Stop SCM+FSA; then i = halt SCM+FSA by A6,TARSKI:def 1; hence i does not destroy intloc 0; end; hence thesis; end; end; end; registration cluster parahalting good halt-ending unique-halt for Program of SCM+FSA; existence proof take Stop SCM+FSA; thus thesis; end; end; registration cluster really-closed good -> keeping_0 for Program of SCM+FSA; correctness proof let I be Program of SCM+FSA; assume A1: I is really-closed good; let s be 0-started State of SCM+FSA; A2: Initialize s = s by MEMSTR_0:44; let P such that A3: I c= P; let k be Nat; :::A5: I is_closed_on s,P by A1,Th18; P +* I = P by A3,FUNCT_4:98; hence Comput(P,s,k).intloc 0 = s.intloc 0 by A1,A2,Th20; end; end; theorem Th21: for a being Int-Location, k being Integer holds rng aSeq(a,k) c= {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} proof let a be Int-Location; let k be Integer; let x be object; assume A1: x in rng aSeq(a,k); per cases; suppose A2: k > 0 & k = 0 + 1; then ex k1 being Nat st k1 + 1 = k & aSeq(a,k) = <% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) by SCMFSA_7:def 2; then aSeq(a,k) = <% a := intloc 0 %> ^ {} by A2 .= <% a := intloc 0 %>; then rng aSeq(a,k) = {a := intloc 0} by AFINSQ_1:33; then x = a := intloc 0 by A1,TARSKI:def 1; hence x in {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by ENUMSET1:def 1; end; suppose A3: k > 0 & k <> 1; then consider k1 being Nat such that A4: k1 + 1 = k and A5: aSeq(a,k) = <% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) by SCMFSA_7:def 2; A6: k1 <> 0 by A3,A4; rng aSeq(a,k) = rng <% a := intloc 0 %> \/ rng (k1 --> AddTo(a, intloc 0)) by A5,AFINSQ_1:26 .= {a := intloc 0} \/ rng ( k1 --> AddTo(a,intloc 0)) by AFINSQ_1:33 .= {a := intloc 0} \/ {AddTo(a,intloc 0)} by A6,FUNCOP_1:8; then x in {a := intloc 0} or x in {AddTo(a,intloc 0)} by A1, XBOOLE_0:def 3; then x = a := intloc 0 or x = AddTo(a,intloc 0) by TARSKI:def 1; hence x in {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by ENUMSET1:def 1; end; suppose A7: not k > 0; then consider k1 being Nat such that A8: k1 + k = 1 and A9: aSeq(a,k) = <% a := intloc 0 %> ^ (k1 --> SubFrom(a,intloc 0)) by SCMFSA_7:def 2; A10: k1 <> 0 by A7,A8; rng aSeq(a,k) = rng <% a := intloc 0 %> \/ rng (k1 --> SubFrom(a, intloc 0)) by A9,AFINSQ_1:26 .= {a := intloc 0} \/ rng ( k1 --> SubFrom(a,intloc 0)) by AFINSQ_1:33 .= {a := intloc 0} \/ {SubFrom(a,intloc 0)} by A10,FUNCOP_1:8; then x in {a := intloc 0} or x in {SubFrom(a,intloc 0)} by A1, XBOOLE_0:def 3; then x = a := intloc 0 or x = SubFrom(a,intloc 0) by TARSKI:def 1; hence x in {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by ENUMSET1:def 1; end; end; theorem Th22: for a being Int-Location, k being Integer holds rng (a := k) c= {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} proof let a be Int-Location; let k be Integer; let x be object; A1: rng aSeq(a,k) c= {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0 ) } by Th21; A2: rng (a := k) = rng (aSeq(a,k) ^ Stop SCM+FSA) by SCMFSA_7:1 .= rng aSeq(a,k) \/ rng Stop SCM+FSA by AFINSQ_1:26 .= rng aSeq(a,k) \/ {halt SCM+FSA} by AFINSQ_1:33; assume x in rng (a := k); then x in rng aSeq(a,k) or x in {halt SCM+FSA} by A2,XBOOLE_0:def 3; then x = a := intloc 0 or x = AddTo(a,intloc 0) or x = SubFrom(a,intloc 0) or x = halt SCM+FSA by A1,ENUMSET1:def 1,TARSKI:def 1; hence x in {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0 )} by ENUMSET1:def 2; end; registration let a be read-write Int-Location, k be Integer; cluster a := k -> good; correctness proof now let i be Instruction of SCM+FSA; A1: rng (a := k) c= {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0), SubFrom(a,intloc 0)} by Th22; assume A2: i in rng (a := k); per cases by A2,A1,ENUMSET1:def 2; suppose i = halt SCM+FSA; hence i does not destroy intloc 0; end; suppose i = a := intloc 0; hence i does not destroy intloc 0 by Th6; end; suppose i = AddTo(a,intloc 0); hence i does not destroy intloc 0 by Th7; end; suppose i = SubFrom(a,intloc 0); hence i does not destroy intloc 0 by Th8; end; end; then a := k does not destroy intloc 0; hence thesis; end; end; reserve n for Nat; registration let a be read-write Int-Location, k be Integer; cluster a := k -> really-closed; correctness proof per cases; suppose k > 0; then consider k1 being Nat such that k1 + 1 = k and A1: a := k = <% a:= intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA by SCMFSA_7:def 1; defpred P[Nat] means <% a:= intloc 0 %> ^ ($1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA is really-closed; <% a:= intloc 0 %> ^ (0 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA = <% a:= intloc 0 %> ^ {} ^ Stop SCM+FSA .= <% a:= intloc 0 %> ^ Stop SCM+FSA .= Macro(a:= intloc 0); then <% a:= intloc 0 %> ^ (0 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA is really-closed; then A2: P[0]; A3: for n st P[n] holds P[n+1] proof let n; assume A4: P[n]; set p1 = n --> AddTo(a,intloc 0); now per cases; suppose n is empty; then p1 is empty; then <% a:= intloc 0 %> ^ p1 = <% a:= intloc 0 %>; hence <% a:= intloc 0 %> ^ p1 is halt-free; end; suppose A5: n is non empty; then p1 is non empty; then reconsider pp=p1 as Program of SCM+FSA; A6: rng pp = {AddTo(a,intloc 0)} by A5,FUNCOP_1:8; now assume halt SCM+FSA in rng pp; then halt SCM+FSA = AddTo(a,intloc 0) by A6,TARSKI:def 1; hence contradiction; end; then pp is halt-free by COMPOS_1:def 11; hence <% a:= intloc 0 %> ^ p1 is halt-free; end; end; then reconsider p = <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) as halt-free Program of SCM+FSA; set m = <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^ Stop SCM+FSA; m = stop p; then reconsider m as really-closed MacroInstruction of SCM+FSA by A4; A7: CutLastLoc m = <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) by AFINSQ_2:83; A8: card CutLastLoc m = card m -' 1 by VALUED_1:65; <% a:= intloc 0 %> ^ (Segm(n+1) --> AddTo(a,intloc 0)) ^ Stop SCM+FSA = <% a:= intloc 0 %> ^ ((Segm n --> AddTo(a,intloc 0)) ^ <%AddTo(a,intloc 0)%>) ^ Stop SCM+FSA by AFINSQ_1:87 .= <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^ <%AddTo(a,intloc 0)%> ^ Stop SCM+FSA by AFINSQ_1:27 .= <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^ (<%AddTo(a,intloc 0)%> ^ Stop SCM+FSA) by AFINSQ_1:27 .= <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^ Macro AddTo(a,intloc 0) .= CutLastLoc m +* Shift(Macro AddTo(a,intloc 0),card m -' 1) by A7,A8,AFINSQ_1:77 .= CutLastLoc m +* Shift(Macro IncAddr(AddTo(a,intloc 0),card m -' 1),card m -' 1) by COMPOS_0:4 .= CutLastLoc m +* Shift(IncAddr(Macro AddTo(a,intloc 0),card m -' 1),card m -' 1) by COMPOS_1:74 .= CutLastLoc m +* Reloc(Macro AddTo(a,intloc 0),card m -' 1) .= m ';' Macro AddTo(a,intloc 0) .= m ';' AddTo(a,intloc 0); then <% a:= intloc 0 %> ^ ((n+1) --> AddTo(a,intloc 0)) ^ Stop SCM+FSA is really-closed; hence P[n+1]; end; for n holds P[n] from NAT_1:sch 2(A2,A3); hence thesis by A1; end; suppose k <= 0; then consider k1 being Nat such that k1 + k = 1 and A9: a := k = <% a:= intloc 0 %> ^ ( k1 --> SubFrom(a,intloc 0) ) ^ Stop SCM+FSA by SCMFSA_7:def 1; defpred P[Nat] means <% a:= intloc 0 %> ^ ($1 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA is really-closed; <% a:= intloc 0 %> ^ (0 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA = <% a:= intloc 0 %> ^ {} ^ Stop SCM+FSA .= <% a:= intloc 0 %> ^ Stop SCM+FSA .= Macro(a:= intloc 0); then <% a:= intloc 0 %> ^ (0 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA is really-closed; then A10: P[0]; A11: for n st P[n] holds P[n+1] proof let n; assume A12: P[n]; set p1 = n --> SubFrom(a,intloc 0); now per cases; suppose n is empty; then p1 is empty; then <% a:= intloc 0 %> ^ p1 = <% a:= intloc 0 %>; hence <% a:= intloc 0 %> ^ p1 is halt-free; end; suppose A13: n is non empty; then p1 is non empty; then reconsider pp=p1 as Program of SCM+FSA; A14: rng pp = {SubFrom(a,intloc 0)} by A13,FUNCOP_1:8; now assume halt SCM+FSA in rng pp; then halt SCM+FSA = SubFrom(a,intloc 0) by A14,TARSKI:def 1; hence contradiction; end; then pp is halt-free by COMPOS_1:def 11; hence <% a:= intloc 0 %> ^ p1 is halt-free; end; end; then reconsider p = <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) as halt-free Program of SCM+FSA; set m = <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA; m = stop p; then reconsider m as really-closed MacroInstruction of SCM+FSA by A12; A15: CutLastLoc m = <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) by AFINSQ_2:83; A16: card CutLastLoc m = card m -' 1 by VALUED_1:65; <% a:= intloc 0 %> ^ (Segm(n+1) --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA = <% a:= intloc 0 %> ^ ((Segm n --> SubFrom(a,intloc 0)) ^ <%SubFrom(a,intloc 0)%>) ^ Stop SCM+FSA by AFINSQ_1:87 .= <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^ <%SubFrom(a,intloc 0)%> ^ Stop SCM+FSA by AFINSQ_1:27 .= <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^ (<%SubFrom(a,intloc 0)%> ^ Stop SCM+FSA) by AFINSQ_1:27 .= <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^ Macro SubFrom(a,intloc 0) .= CutLastLoc m +* Shift(Macro SubFrom(a,intloc 0),card m -' 1) by A15,A16,AFINSQ_1:77 .= CutLastLoc m +* Shift(Macro IncAddr(SubFrom(a,intloc 0),card m -' 1),card m -' 1) by COMPOS_0:4 .= CutLastLoc m +* Shift(IncAddr(Macro SubFrom(a,intloc 0),card m -' 1),card m -' 1) by COMPOS_1:74 .= CutLastLoc m +* Reloc(Macro SubFrom(a,intloc 0),card m -' 1) .= m ';' Macro SubFrom(a,intloc 0) .= m ';' SubFrom(a,intloc 0); then <% a:= intloc 0 %> ^ ((n+1) --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA is really-closed; hence P[n+1]; end; for n holds P[n] from NAT_1:sch 2(A10,A11); hence thesis by A9; end; end; end; registration let a be read-write Int-Location, k be Integer; cluster a := k -> keeping_0; correctness; end;