Copyright (c) 1996 Association of Mizar Users
environ vocabulary AMI_3, AMI_1, SCMFSA_2, FINSEQ_1, RELAT_1, SCMFSA_7, ARYTM_1, FUNCT_1, CAT_1, SCMFSA6A, CARD_1, FUNCT_4, INT_1, FINSEQ_2, AMI_2, SCMFSA6B, SF_MASTR, BOOLE, DTCONSTR, ABSVALUE, AMI_5, UNIALG_2, SCMFSA_4, FUNCOP_1, SCMFSA7B, FINSEQ_4; notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, INT_1, RELAT_1, FUNCT_1, FUNCT_4, FUNCT_7, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINARITH, FINSOP_1, FUNCOP_1, DTCONSTR, CARD_1, CQC_LANG, AMI_1, AMI_3, AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B, GROUP_1; constructors REAL_1, FINSOP_1, ENUMSET1, BINARITH, AMI_5, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B, FINSEQ_4, MEMBERED; clusters RELSET_1, FINSEQ_1, INT_1, FUNCT_1, AMI_1, SCMFSA_2, SCMFSA_4, SCMFSA_7, SF_MASTR, SCMFSA6B, FUNCOP_1, CQC_LANG, NAT_1, FRAENKEL, XREAL_0, MEMBERED; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; theorems AXIOMS, SCMFSA_7, BINARITH, REAL_1, FINSEQ_1, FINSEQ_2, NAT_1, GRFUNC_1, FUNCT_1, FUNCT_4, FUNCT_7, FINSEQ_3, FINSEQ_4, AMI_1, ENUMSET1, SCMFSA_2, CQC_THE1, CQC_LANG, AMI_5, FUNCOP_1, INT_1, DTCONSTR, FINSEQ_6, RELAT_1, SCMFSA_4, TARSKI, AMI_3, SCMFSA6A, SF_MASTR, SCMFSA6B, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes NAT_1, FINSEQ_1; begin reserve m for Nat; set A = the Instruction-Locations of SCM+FSA; theorem Th1: ::TG4 for p being FinSequence of the Instructions of SCM+FSA holds dom Load p = {insloc m: m < len p} proof let p be FinSequence of the Instructions of SCM+FSA; A1: dom Load p = {insloc (m -' 1): m in dom p} by SCMFSA_7:def 1; now let x be set; assume A2: x in dom Load p; then consider k being Nat such that A3: x = insloc (k -' 1) and k in dom p by A1; k -' 1 < len p by A2,A3,SCMFSA_7:29; hence x in {insloc m: m < len p} by A3; end; then A4: dom Load p c= {insloc m: m < len p} by TARSKI:def 3; now let x be set; assume x in {insloc m: m < len p}; then ex k being Nat st x = insloc k & k < len p; hence x in dom Load p by SCMFSA_7:29; end; then {insloc m: m < len p} c= dom Load p by TARSKI:def 3; hence thesis by A4,XBOOLE_0:def 10; end; theorem Th2: ::T83(@AAAA) for p being FinSequence of the Instructions of SCM+FSA holds rng Load p = rng p proof let p be FinSequence of the Instructions of SCM+FSA; A1: dom Load p = {insloc (m -' 1): m in dom p} by SCMFSA_7:def 1; now let y be set; assume y in rng Load p; then consider x being set such that A2: x in dom Load p & y = (Load p).x by FUNCT_1:def 5; consider m being Nat such that A3: x = insloc (m -' 1) & m in dom p by A1,A2; A4: m -' 1 + 1 in dom p by A2,A3,SCMFSA_7:26; then p.(m -' 1 + 1) = p/.(m -' 1 + 1) by FINSEQ_4:def 4 .= y by A2,A3,SCMFSA_7:def 1; hence ex x being set st x in dom p & y = p.x by A4; end; then A5: rng Load p c= rng p by FUNCT_1:19; now let y be set; assume y in rng p; then consider x being set such that A6: x in dom p & y = p.x by FUNCT_1: def 5 ; A7: dom p = Seg len p by FINSEQ_1:def 3; reconsider x as Nat by A6,FINSEQ_3:25; A8: insloc (x -' 1) in dom Load p by A1,A6; dom p = {m : 1 <= m & m <= len p} by A7,FINSEQ_1:def 1; then consider m being Nat such that A9: x = m & 1 <= m & m <= len p by A6; A10: x -' 1 + 1 = x - 1 + 1 by A9,SCMFSA_7:3 .= x by XCMPLX_1:27; (Load p).insloc (x -' 1) = p/.(x -' 1 + 1) by A8,SCMFSA_7:def 1 .= y by A6,A10,FINSEQ_4:def 4; hence ex x being set st x in dom Load p & y = (Load p).x by A8; end; then rng p c= rng Load p by FUNCT_1:19; hence rng Load p = rng p by A5,XBOOLE_0:def 10; end; definition let p be FinSequence of the Instructions of SCM+FSA; cluster Load p -> initial programmed; coherence proof A1: dom Load p = {insloc m: m < len p} by Th1; A2: now let k,n be Nat; assume that A3: insloc n in dom Load p and A4: k < n; n < len p by A3,SCMFSA_7:29; then k < len p by A4,AXIOMS:22; hence insloc k in dom Load p by A1; end; now let x be set; assume x in dom Load p; then consider m such that A5: insloc m = x & m < len p by A1; thus x in the Instruction-Locations of SCM+FSA by A5; end; then dom Load p c= the Instruction-Locations of SCM+FSA by TARSKI:def 3; hence thesis by A2,AMI_3:def 13,SCMFSA_4:def 4; end; end; theorem ::TQ50 for i being Instruction of SCM+FSA holds Load <* i *> = insloc 0 .--> i proof let i be Instruction of SCM+FSA; A1: dom Load <* i *> = {insloc m: m < len <* i *>} by Th1; A2: len <* i *> = 1 by FINSEQ_1:56; A3: dom (insloc 0 .--> i) = {insloc 0} by CQC_LANG:5; now let x be set; assume x in dom Load <* i *>; then consider m being Nat such that A4: x = insloc m and A5: m < 0 + len <* i *> by A1; m <= 0 by A2,A5,NAT_1:38; then x = insloc 0 by A4,NAT_1:19; hence x in {insloc 0} by TARSKI:def 1; end; then A6: dom Load <* i *> c= {insloc 0} by TARSKI:def 3; now let x be set; assume x in {insloc 0}; then x = insloc 0 by TARSKI:def 1; hence x in dom Load <* i *> by A1,A2; end; then A7: {insloc 0} c= dom Load <* i *> by TARSKI:def 3; then A8: dom Load <* i *> = {insloc 0} by A6,XBOOLE_0:def 10; now let x be set; assume A9: x in {insloc 0}; then A10: x = insloc 0 by TARSKI:def 1; hence (Load <* i *>).x = <* i *>/.(0 + 1) by A7,A9,SCMFSA_7:def 1 .= <* i *>.1 by A2,FINSEQ_4:24 .= i by FINSEQ_1:57 .= (insloc 0 .--> i).x by A10,CQC_LANG:6; end; hence thesis by A3,A8,FUNCT_1:9; end; theorem Th4: for i being Instruction of SCM+FSA holds dom Macro i = { insloc 0, insloc 1 } proof let i be Instruction of SCM+FSA; for x be set holds x in dom Macro i iff x = insloc 0 or x = insloc 1 by SCMFSA6B:32; hence thesis by TARSKI:def 2; end; theorem Th5: ::TQ56 for i being Instruction of SCM+FSA holds Macro i = Load <* i,halt SCM+FSA *> proof let i be Instruction of SCM+FSA; A1: dom Load <* i,halt SCM+FSA *> = {insloc (m -' 1): m in dom <* i,halt SCM+FSA *>} by SCMFSA_7:def 1; A2: dom <* i,halt SCM+FSA *> = Seg len <* i,halt SCM+FSA *> by FINSEQ_1:def 3 .= {1,2} by FINSEQ_1:4,61; then A3: 1 in dom <* i,halt SCM+FSA *> & 2 in dom <* i,halt SCM+FSA *> by TARSKI:def 2 ; A4: dom Macro i = {insloc 0,insloc 1} by Th4; now let x be set; assume x in dom Load <* i,halt SCM+FSA *>; then consider m being Nat such that A5: x = insloc (m -' 1) and A6: m in dom <* i,halt SCM+FSA *> by A1; x = insloc (0 + 1 -' 1) or x = insloc (1 + 1 -' 1) by A2,A5,A6,TARSKI: def 2; then x = insloc 0 or x = insloc 1 by BINARITH:39; hence x in {insloc 0,insloc 1} by TARSKI:def 2; end; then A7: dom Load <* i,halt SCM+FSA *> c= {insloc 0,insloc 1} by TARSKI:def 3; now let x be set; assume x in {insloc 0,insloc 1}; then x = insloc 0 or x = insloc 1 by TARSKI:def 2; then x = insloc (0 + 1 -' 1) or x = insloc (1 + 1 -' 1) by BINARITH:39; hence x in dom Load <* i,halt SCM+FSA *> by A1,A3; end; then A8: {insloc 0,insloc 1} c= dom Load <* i,halt SCM+FSA *> by TARSKI:def 3; then A9: dom Load <* i,halt SCM+FSA *> = {insloc 0,insloc 1} by A7,XBOOLE_0:def 10; now let x be set; assume A10: x in {insloc 0,insloc 1}; per cases by A10,TARSKI:def 2; suppose A11: x = insloc 0; hence (Load <* i,halt SCM+FSA *>).x = <* i,halt SCM+FSA *>/.(0 + 1) by A8,A10,SCMFSA_7:def 1 .= <* i,halt SCM+FSA *>.1 by A3,FINSEQ_4:def 4 .= (<* i *> ^ <* halt SCM+FSA *>).1 by FINSEQ_1:def 9 .= i by FINSEQ_1:58 .= (Macro i).x by A11,SCMFSA6B:33; suppose A12: x = insloc 1; hence (Load <* i,halt SCM+FSA *>).x = <* i,halt SCM+FSA *>/.(1 + 1) by A8,A10,SCMFSA_7:def 1 .= <* i,halt SCM+FSA *>.2 by A3,FINSEQ_4:def 4 .= (<* i *> ^ <* halt SCM+FSA *>).2 by FINSEQ_1:def 9 .= (<* i *> ^ <* halt SCM+FSA *>).(len <* i *> + 1) by FINSEQ_1:57 .= halt SCM+FSA by FINSEQ_1:59 .= (Macro i).x by A12,SCMFSA6B:33; end; hence thesis by A4,A9,FUNCT_1:9; end; theorem Th6: ::T54(@BBB8) for i being Instruction of SCM+FSA holds card Macro i = 2 proof let i be Instruction of SCM+FSA; thus card Macro i = card Load <* i,halt SCM+FSA *> by Th5 .= len <* i,halt SCM+FSA *> by SCMFSA_7:25 .= 2 by FINSEQ_1:61; end; theorem ::T25(@BBB8) for i being Instruction of SCM+FSA holds (i = halt SCM+FSA implies (Directed Macro i).insloc 0 = goto insloc 2) & (i <> halt SCM+FSA implies (Directed Macro i).insloc 0 = i) proof let i be Instruction of SCM+FSA; insloc 0 in {insloc 0,insloc 1} by TARSKI:def 2; then A1: insloc 0 in dom Macro i by Th4; A2: card Macro i = 2 by Th6; A3: (Macro i).insloc 0 = i by SCMFSA6B:33; hereby assume A4: i = halt SCM+FSA; dom (halt SCM+FSA .--> goto insloc 2) = {halt SCM+FSA} by CQC_LANG:5; then A5: i in dom (halt SCM+FSA .--> goto insloc 2) by A4,TARSKI:def 1; thus (Directed Macro i).insloc 0 = (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 2))*Macro i).insloc 0 by A2,SCMFSA6A:def 1 .= ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 2)).i by A1,A3,FUNCT_1:23 .= (halt SCM+FSA .--> goto insloc 2).i by A5,FUNCT_4:14 .= goto insloc 2 by A4,CQC_LANG:6; end; assume A6: i <> halt SCM+FSA; dom (halt SCM+FSA .--> goto insloc 2) = {halt SCM+FSA} by CQC_LANG:5; then A7: not i in dom (halt SCM+FSA .--> goto insloc 2) by A6,TARSKI:def 1; thus (Directed Macro i).insloc 0 = (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 2))* Macro i).insloc 0 by A2,SCMFSA6A:def 1 .= ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 2)).i by A1,A3,FUNCT_1:23 .= (id the Instructions of SCM+FSA).i by A7,FUNCT_4:12 .= i by FUNCT_1:35; end; theorem ::T26(@BBB8) for i being Instruction of SCM+FSA holds (Directed Macro i).insloc 1 = goto insloc 2 proof let i be Instruction of SCM+FSA; A1: dom (halt SCM+FSA .--> goto insloc 2 ) = {halt SCM+FSA} by CQC_LANG:5; A2: card Macro i = 2 by Th6; insloc 1 in {insloc 0,insloc 1} by TARSKI:def 2; then A3: insloc 1 in dom Macro i by Th4; A4: halt SCM+FSA in dom (halt SCM+FSA .--> goto insloc 2) by A1,TARSKI:def 1; A5: (Macro i).insloc 1 = halt SCM+FSA by SCMFSA6B:33; thus (Directed Macro i).insloc 1 = (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 2))* Macro i).insloc 1 by A2,SCMFSA6A:def 1 .= ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 2)). halt SCM+FSA by A3,A5,FUNCT_1:23 .= (halt SCM+FSA .--> goto insloc 2).halt SCM+FSA by A4,FUNCT_4:14 .= goto insloc 2 by CQC_LANG:6; end; definition let a be Int-Location, k be Integer; cluster a := k -> initial programmed; coherence proof a := k = Load (aSeq(a,k) ^ <* halt SCM+FSA *>) by SCMFSA_7:33; hence a := k is initial programmed; end; end; Lm1: ::SCMFSA_7'38 for s being State of SCM+FSA st IC s = insloc 0 for a being Int-Location, k being Integer st a := k c= s holds s is halting proof let s be State of SCM+FSA; assume A1: IC s = insloc 0; let a be Int-Location, k be Integer; assume A2: a := k c= s; per cases; suppose A3: k > 0; then consider k1 being Nat such that A4: k1 + 1 = k & a := k = Load (<* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0)) ^ <* halt SCM+FSA *>) by SCMFSA_7:def 2; set f = <* a:=intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0)) ^ <* halt SCM+FSA *>; A5: len (<* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0))) = len <* a := intloc 0 *> + len (k1 |-> AddTo(a,intloc 0)) by FINSEQ_1:35 .= 1 + len (k1 |-> AddTo(a,intloc 0)) by FINSEQ_1:56 .= k by A4,FINSEQ_2:69; reconsider k as Nat by A3,INT_1:16; A6: len f = len (<* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0))) + len <* halt SCM+FSA *> by FINSEQ_1:35 .= k + 1 by A5,FINSEQ_1:56; then A7: dom f = Seg (k + 1) by FINSEQ_1:def 3; A8: now let i be Nat; assume A9: 0 <= i & i <= k; then 0 + 1 <= i + 1 & i + 1 <= k + 1 by AXIOMS:24; hence i + 1 in dom f by A7,FINSEQ_1:3; i < k + 1 & dom Load f = {insloc m: m < len f} by A9,Th1,NAT_1:38; hence insloc i in dom Load f by A6; end; A10: now let i be Nat; assume 0 <= i & i <= k; then A11: i + 1 in dom f & insloc i in dom Load f by A8; hence s.insloc i = (Load f).insloc i by A2,A4,GRFUNC_1:8 .= f/.(i+1) by A11,SCMFSA_7:def 1 .= f.(i+1) by A11,FINSEQ_4:def 4; end; A12: f.1 = (<* a := intloc 0 *> ^ ((k1 |-> AddTo(a,intloc 0)) ^ <*halt SCM+FSA*>)).1 by FINSEQ_1:45 .= a := intloc 0 by FINSEQ_1:58; A13: s.insloc 0 = f.(0 + 1) by A3,A10 .= a := intloc 0 by A12; A14: now let i be Nat; assume A15: 1 < i & i <= k; then A16: 1 <= i - 1 by SCMFSA_7:4; then 0 <= i - 1 by AXIOMS:22; then reconsider i1 = i - 1 as Nat by INT_1:16; i - 1 <= k - 1 by A15,REAL_1:49; then i - 1 <= k1 by A4,XCMPLX_1:26; then A17: i1 in Seg k1 by A16,FINSEQ_1:3; A18: len <* a := intloc 0 *> = 1 by FINSEQ_1:56; dom (<* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0))) = Seg k by A5,FINSEQ_1:def 3; then i in dom (<* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0))) by A15,FINSEQ_1:3; hence f.i = (<* a:= intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0))).i by FINSEQ_1:def 7 .= (k1 |-> AddTo(a,intloc 0)).(i - 1) by A5,A15,A18,FINSEQ_1:37 .= AddTo(a,intloc 0) by A17,FINSEQ_2:70; end; A19: now let i be Nat; assume A20: 0 < i & i < k; then A21: 0 + 1 < i + 1 by REAL_1:53; A22: i + 1 <= k by A20,NAT_1:38; thus s.insloc i = f.(i+1) by A10,A20 .= AddTo(a,intloc 0) by A14,A21,A22; end; k < k + 1 by REAL_1:69; then f.(k + 1) = <* halt SCM+FSA *>.(k + 1 - k) by A5,A6,FINSEQ_1:37 .= <* halt SCM+FSA *>.1 by XCMPLX_1:26 .= halt SCM+FSA by FINSEQ_1:def 8; then A23: s.insloc k = halt SCM+FSA by A3,A10; A24: now let n be Nat; assume n = 0; hence A25: (Computation s).n = s by AMI_1:def 19; hence A26: CurInstr (Computation s).n = a:= intloc 0 by A1,A13,AMI_1:def 17; thus (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(a:= intloc 0,s) by A25,A26,AMI_1:def 18; end; A27: for i being Nat st i <= k holds IC (Computation s).i = insloc i proof let i be Nat; assume A28: i <= k; defpred P[Nat] means $1 <= k implies IC (Computation s).$1 = insloc $1; A29: P[0] by A1,AMI_1:def 19; A30: for n being Nat st P[n] holds P[n + 1] proof let n be Nat; assume A31: P[n]; assume A32: n+1 <= k; then A33: n < k by NAT_1:38; per cases by NAT_1:19; suppose A34: n=0; hence IC (Computation s).(n+1) = IC Exec(a:= intloc 0,s) by A24 .= Exec(a:= intloc 0,s).IC SCM+FSA by AMI_1:def 15 .= Next insloc n by A1,A34,SCMFSA_2:89 .= insloc (n+1) by SCMFSA_2:32; suppose A35: n>0; n + 0 <= n + 1 by REAL_1:55; then A36: CurInstr (Computation s).n = ((Computation s).n).insloc n by A31,A32,AMI_1:def 17,AXIOMS:22 .= s.insloc n by AMI_1:54 .= AddTo(a,intloc 0) by A19,A33,A35; A37: (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(AddTo(a,intloc 0),(Computation s).n) by A36,AMI_1:def 18; thus IC (Computation s).(n+1) = (Computation s).(n+1).IC SCM+FSA by AMI_1:def 15 .= Next IC (Computation s).n by A37,SCMFSA_2:90 .= insloc (n+1) by A31,A32,NAT_1:38,SCMFSA_2:32; end; for i being Nat holds P[i] from Ind(A29,A30); hence IC (Computation s).i = insloc i by A28; end; CurInstr (Computation s).k = ((Computation s).k).IC (Computation s).k by AMI_1:def 17 .= ((Computation s).k).insloc k by A27 .= halt SCM+FSA by A23,AMI_1:54; hence s is halting by AMI_1:def 20; suppose A38: k <= 0; then A39: 0 <= - k by REAL_1:26,50; then reconsider mk = - k as Nat by INT_1:16; 0 + 0 <= mk + (1+1) by A39,REAL_1:55; then A40: 0 <= mk+1+1 by XCMPLX_1:1; consider k1 being Nat such that A41: k1 + k = 1 & a:=k = Load (<*a:=intloc 0*> ^ (k1 |-> SubFrom(a,intloc 0)) ^ <*halt SCM+FSA*>) by A38,SCMFSA_7:def 2; A42: k1 = 1 - k by A41,XCMPLX_1:26 .= 1 + mk by XCMPLX_0:def 8; set f = <*a:=intloc 0*> ^ (k1 |-> SubFrom(a,intloc 0)) ^ <*halt SCM+FSA*>; A43: len (<*a:=intloc 0*>^(k1|->SubFrom(a,intloc 0))) = len<*a:=intloc 0*> + len(k1|->SubFrom(a,intloc 0)) by FINSEQ_1:35 .= 1 + len(k1|->SubFrom(a,intloc 0)) by FINSEQ_1:56 .= mk+1+1 by A42,FINSEQ_2:69; A44: len f = len(<*a:=intloc 0*>^(k1|->SubFrom(a,intloc 0)))+len<*halt SCM+FSA *> by FINSEQ_1:35 .= mk+1+1 + 1 by A43,FINSEQ_1:56; then A45: dom f = Seg (mk+1+1 + 1) by FINSEQ_1:def 3; A46: now let i be Nat; assume A47: 0 <= i & i <= mk+1+1; then 0 + 1 <= i + 1 & i + 1 <= mk+1+1 + 1 by AXIOMS:24; hence i + 1 in dom f by A45,FINSEQ_1:3; i < mk+1+1 + 1 & dom Load f = {insloc m: m < len f} by A47,Th1,NAT_1: 38 ; hence insloc i in dom Load f by A44; end; A48: now let i be Nat; assume 0 <= i & i <= mk+1+1; then A49: i + 1 in dom f & insloc i in dom Load f by A46; hence s.insloc i = (Load f).insloc i by A2,A41,GRFUNC_1:8 .= f/.(i+1) by A49,SCMFSA_7:def 1 .= f.(i+1) by A49,FINSEQ_4:def 4; end; A50: f.1 = (<*a:=intloc 0*>^((k1|->SubFrom(a,intloc 0))^<*halt SCM+FSA*>)).1 by FINSEQ_1:45 .= a := intloc 0 by FINSEQ_1:58; A51: s.insloc 0 = f.(0 + 1) by A40,A48 .= a := intloc 0 by A50; A52: now let i be Nat; assume A53: 1 < i & i <= mk+1+1; then A54: 1 - 1 < i - 1 by REAL_1:54; then A55: 1 - 1 + 1 <= i - 1 by INT_1:20; reconsider i1 = i - 1 as Nat by A54,INT_1:16; i - 1 <= mk+1+1 - 1 by A53,REAL_1:49; then i - 1 <= k1 by A42,XCMPLX_1:26; then A56: i1 in Seg k1 by A55,FINSEQ_1:3; A57: len <*a:= intloc 0*> = 1 by FINSEQ_1:56; dom (<*a:=intloc 0*>^(k1|->SubFrom(a,intloc 0))) = Seg (mk+1+1) by A43,FINSEQ_1:def 3; then i in dom (<*a:=intloc 0*>^(k1|->SubFrom(a,intloc 0))) by A53, FINSEQ_1:3; hence f.i = (<*a:=intloc 0*>^(k1|->SubFrom(a,intloc 0))).i by FINSEQ_1:def 7 .= (k1|->SubFrom(a,intloc 0)).(i - 1) by A43,A53,A57,FINSEQ_1:37 .= SubFrom(a,intloc 0) by A56,FINSEQ_2:70; end; A58: now let i be Nat; assume A59: 0 < i & i < mk+1+1; then A60: 0 + 1 < i + 1 by REAL_1:53; A61: i + 1 <= mk+1+1 by A59,NAT_1:38; thus s.insloc i = f.(i+1) by A48,A59 .=SubFrom(a,intloc 0) by A52,A60,A61; end; mk+1+1 < mk+1+1 + 1 by REAL_1:69; then A62: f.(mk+1+1+1) = <*halt SCM+FSA*>.(mk+1+1+1-(mk+1+1)) by A43,A44, FINSEQ_1:37 .= <*halt SCM+FSA*>.1 by XCMPLX_1:26 .= halt SCM+FSA by FINSEQ_1:def 8; 0 <= mk+1+1 by NAT_1:18; then A63: s.insloc (mk+1+1) = halt SCM+FSA by A48,A62; A64: now let n be Nat; assume n = 0; hence A65: (Computation s).n = s by AMI_1:def 19; hence A66: CurInstr (Computation s).n = a:= intloc 0 by A1,A51,AMI_1:def 17; thus (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(a:= intloc 0,s) by A65,A66,AMI_1:def 18; end; A67: for i being Nat st i <= mk+1+1 holds IC (Computation s).i = insloc i proof let i be Nat; assume A68: i <= mk+1+1; defpred P[Nat] means $1<=mk+1+1 implies IC (Computation s).$1=insloc $1; A69: P[0] by A1,AMI_1:def 19; A70: for n being Nat st P[n] holds P[n + 1] proof let n be Nat; assume A71: P[n]; assume A72: n+1 <= mk+1+1; then A73: n < mk+1+1 by NAT_1:38; per cases by NAT_1:19; suppose A74: n=0; hence IC (Computation s).(n+1) = IC Exec(a:= intloc 0,s) by A64 .= Exec(a:= intloc 0,s).IC SCM+FSA by AMI_1:def 15 .= Next insloc n by A1,A74,SCMFSA_2:89 .= insloc (n+1) by SCMFSA_2:32; suppose A75: n>0; n + 0 <= n + 1 by REAL_1:55; then A76: CurInstr (Computation s).n = ((Computation s).n).insloc n by A71,A72,AMI_1:def 17,AXIOMS:22 .= s.insloc n by AMI_1:54 .= SubFrom(a,intloc 0) by A58,A73,A75; A77: (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(SubFrom(a,intloc 0),(Computation s).n) by A76,AMI_1:def 18; thus IC (Computation s).(n+1) = (Computation s).(n+1).IC SCM+FSA by AMI_1:def 15 .= Next IC (Computation s).n by A77,SCMFSA_2:91 .= insloc (n+1) by A71,A72,NAT_1:38,SCMFSA_2:32; end; for i being Nat holds P[i] from Ind(A69,A70); hence IC (Computation s).i = insloc i by A68; end; CurInstr (Computation s).(mk+1+1) = ((Computation s).(mk+1+1)).IC (Computation s).(mk+1+1) by AMI_1:def 17 .= ((Computation s).(mk+1+1)).insloc (mk+1+1) by A67 .= halt SCM+FSA by A63,AMI_1:54; hence s is halting by AMI_1:def 20; end; definition let a be Int-Location, k be Integer; cluster a := k -> parahalting; correctness proof now let s be State of SCM+FSA; assume A1: a := k +* Start-At insloc 0 c= s; A2: IC SCM+FSA in dom (a := k +* Start-At insloc 0) by SF_MASTR:65; A3: IC s = s.IC SCM+FSA by AMI_1:def 15 .= (a := k +* Start-At insloc 0).IC SCM+FSA by A1,A2,GRFUNC_1:8 .= insloc 0 by SF_MASTR:66; a := k c= s by A1,SCMFSA6B:5; hence s is halting by A3,Lm1; end; then a := k +* Start-At insloc 0 is halting by AMI_1:def 26; hence a := k is parahalting by SCMFSA6B:def 3; end; end; theorem ::* for s being State of SCM+FSA for a being read-write Int-Location, k being Integer holds IExec(a := k,s).a = k & (for b being read-write Int-Location st b <> a holds IExec(a := k,s).b = s.b) & (for f being FinSeq-Location holds IExec(a := k,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 +* Initialized (a := k); IC SCM+FSA in dom Initialized (a := k) by SCMFSA6A:24; then s1.IC SCM+FSA = (Initialized (a := k)).IC SCM+FSA by FUNCT_4:14 .= insloc 0 by SCMFSA6A:46; then A1: IC s1 = insloc 0 by AMI_1:def 15; intloc 0 in dom Initialized (a := k) by SCMFSA6A:45; then A2: s1.intloc 0 = (Initialized (a := k)).intloc 0 by FUNCT_4:14 .= 1 by SCMFSA6A:46; A3: Initialized (a := k) c= s1 by FUNCT_4:26; a := k c= Initialized (a := k) by SCMFSA6A:26; then A4: a := k c= s1 by A3,XBOOLE_1:1; A5: IExec(a := k,s) = Result s1 +* s | A by SCMFSA6B:def 1; not a in A by SCMFSA_2:84; then not a in dom s /\ A by XBOOLE_0:def 3; then not a in dom (s | A) by RELAT_1:90; hence IExec(a := k,s).a = (Result s1).a by A5,FUNCT_4:12 .= k by A1,A2,A4,SCMFSA_7:38; hereby let b be read-write Int-Location; assume A6: b <> a; A7: not b in dom Initialized (a := k) by SCMFSA6A:48; not b in A by SCMFSA_2:84; then not b in dom s /\ A by XBOOLE_0:def 3; then not b in dom (s | A) by RELAT_1:90; hence IExec(a := k,s).b = (Result s1).b by A5,FUNCT_4:12 .= s1.b by A1,A2,A4,A6,SCMFSA_7:38 .= s.b by A7,FUNCT_4:12; end; let f be FinSeq-Location; A8: not f in dom Initialized (a := k) by SCMFSA6A:49; not f in A by SCMFSA_2:85; then not f in dom s /\ A by XBOOLE_0:def 3; then not f in dom (s | A) by RELAT_1:90; hence IExec(a := k,s).f = (Result s1).f by A5,FUNCT_4:12 .= s1.f by A1,A2,A4,SCMFSA_7:38 .= s.f by A8,FUNCT_4:12; end; Lm2: for a,b,c,d being Real holds a + b + c + d = a + b + (c + d) & a + b + c + d = a + (b + c + d) & a + b + c + d = a + (b + (c + d)) & a + b + c + d = a + (b + c) + d proof let a,b,c,d be Real; thus a + b + c + d = a + b + (c + d) by XCMPLX_1:1; thus a + b + c + d = a + (b + c) + d by XCMPLX_1:1 .= a + (b + c + d) by XCMPLX_1:1; hence a + b + c + d = a + (b + (c + d)) by XCMPLX_1:1; thus a + b + c + d = a + (b + c) + d by XCMPLX_1:1; end; Lm3: for p1,p2,p3,p4 being FinSequence holds p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3 ^ p4) proof let p1,p2,p3,p4 be FinSequence; thus p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3) ^ p4 by FINSEQ_1:45 .= p1 ^ (p2 ^ p3 ^ p4) by FINSEQ_1:45; end; Lm4: for p1,p2,p3 being FinSequence holds len p1 + len p2 + len p3 = len (p1 ^ p2 ^ p3) & len p1 + len p2 + len p3 = len (p1 ^ (p2 ^ p3)) & len p1 + (len p2 + len p3) = len (p1 ^ (p2 ^ p3)) & len p1 + (len p2 + len p3) = len (p1 ^ p2 ^ p3) proof let p1,p2,p3 be FinSequence; thus len p1 + len p2 + len p3 = len (p1 ^ p2) + len p3 by FINSEQ_1:35 .= len (p1 ^ p2 ^ p3) by FINSEQ_1:35; hence len p1 + len p2 + len p3 = len (p1 ^ (p2 ^ p3)) by FINSEQ_1:45; hence len p1 + (len p2 + len p3) = len (p1 ^ (p2 ^ p3)) by XCMPLX_1:1; hence thesis by FINSEQ_1:45; end; Lm5: ::TG3 for s being State of SCM+FSA st IC s = insloc 0 & s.intloc 0 = 1 for f being FinSeq-Location, p being FinSequence of INT st (f := p) c= s holds s is halting & (Result s).f = p & (for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result s).b = s.b) & (for g being FinSeq-Location st g <> f holds (Result s).g = s.g) proof set O = intloc 0; set D = the Instructions of SCM+FSA; let s be State of SCM+FSA such that A1: IC s = insloc 0 and A2: s.O = 1; let f be FinSeq-Location; let p be FinSequence of INT; intloc 0 <> intloc 1 & intloc 0 <> intloc 2 by SCMFSA_2:16; then reconsider a1 = intloc 1,a2 = intloc 2 as read-write Int-Location by SF_MASTR:def 5; A3: a1 <> a2 by SCMFSA_2:16; assume A4: (f := p) c= s; set q = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *> ^ aSeq(f,p) ^ <* halt SCM+FSA *>; set q0 = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *>; A5: (f := p) = Load q by SCMFSA_7:def 5; A6: dom Load q = {insloc (m -' 1): m in dom q} by SCMFSA_7:def 1; A7: now let k be Nat; assume A8: insloc k in dom Load q; then A9: k + 1 in dom q by SCMFSA_7:26; thus (Load q).insloc k = q/.(k+1) by A8,SCMFSA_7:def 1 .= q.(k+1) by A9,FINSEQ_4:def 4; end; consider pp being FinSequence of D* such that A10: len pp = len p and A11: for k being Nat st 1 <= k & k <= len p holds ex i being Integer st i = p.k & pp.k = (aSeq(a1,k) ^ aSeq(a2,i) ^ <* (f,a1):= a2 *>) and A12: aSeq(f,p) = FlattenSeq pp by SCMFSA_7:def 4; set k = len aSeq(a1,len p); A13: len q0 = k + 1 by FINSEQ_2:19; A14: q = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *> ^ (aSeq(f,p) ^ <* halt SCM+FSA *>) by FINSEQ_1:45; A15: now q = aSeq(a1,len p) ^ (<* f :=<0,...,0> a1 *> ^ (aSeq(f,p) ^ <* halt SCM+FSA *>)) by A14,FINSEQ_1:45; then Load aSeq(a1,len p) c= (f := p) by A5,SCMFSA_7:31; hence Load aSeq(a1,len p) c= s by A4,XBOOLE_1:1; end; A16: now let i be Nat; assume A17: insloc i in dom Load q; then A18: i + 1 in dom q by SCMFSA_7:26; s.insloc i = (Load q).insloc i by A4,A5,A17,GRFUNC_1:8; then s.insloc i = q/.(i + 1) by A17,SCMFSA_7:def 1; hence s.insloc i = q.(i + 1) by A18,FINSEQ_4:def 4; end; A19: now let i,k be Nat; assume i < len q; then A20: insloc i in dom Load q by SCMFSA_7:29; thus ((Computation s).k).insloc i = s.insloc i by AMI_1:54 .= q.(i + 1) by A16,A20; end; defpred P[FinSequence] means $1 c= pp implies (ex pp0 being FinSequence of D* st (pp0 = $1 & (for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds IC (Computation s).i = insloc i) & (((Computation s).(len (q0 ^ FlattenSeq pp0)).f) | Seg len pp0 = p | Seg len pp0) & len ((Computation s).(len (q0 ^ FlattenSeq pp0)).f) = len p & (for b being Int-Location st b <> a1 & b <> a2 holds (Computation s).(len (q0 ^ FlattenSeq pp0)).b = s.b) & (for g being FinSeq-Location st g <> f holds (Computation s).(len (q0 ^ FlattenSeq pp0)).g = s.g))); A21: P[{}] proof A22: q0 ^ FlattenSeq <*>(D*) = q0 ^ <*>D by SCMFSA_7:13 .= q0 by FINSEQ_1:47; assume {} c= pp; take <*>(D*); thus <*>(D*) = {}; A23: now let i be Nat such that A24: i < len q0; i < len q0 implies i <= len aSeq(a1,len p) by A13,NAT_1:38; hence IC (Computation s).i = insloc i by A1,A2,A15,A24,SCMFSA_7:37; end; k < len q0 by A13,NAT_1:38; then A25: IC (Computation s).k = insloc k by A23; len q = len q0 + len (aSeq(f,p) ^ <* halt SCM+FSA *>) by A14,FINSEQ_1:35; then len q0 <= len q by NAT_1:29; then A26: k < len q by A13,NAT_1:38; A27: 1 <= len q0 by A13,NAT_1:29; A28: CurInstr (Computation s).k = ((Computation s).k).insloc k by A25,AMI_1:def 17 .= q.len q0 by A13,A19,A26 .= q0.len q0 by A14,A27,SCMFSA_7:9 .= f:=<0,...,0>a1 by A13,FINSEQ_1:59; A29: (Computation s).len q0 = Following (Computation s).k by A13,AMI_1:def 19 .= Exec(f:=<0,...,0>a1,(Computation s).k) by A28,AMI_1:def 18; A30: IC (Computation s).len q0 = (Computation s).len q0.IC SCM+FSA by AMI_1:def 15 .= Next IC (Computation s).k by A29,SCMFSA_2:101 .= insloc len q0 by A13,A25,SCMFSA_2:32; now let i be Nat; assume i <= len q0; then i < len q0 or i = len q0 by REAL_1:def 5; hence IC (Computation s).i = insloc i by A23,A30; end; hence for i being Nat st i <= len (q0 ^ FlattenSeq <*>(D*)) holds IC (Computation s).i = insloc i by A22; len <*>(D*) = 0 by FINSEQ_1:32; hence ((Computation s).(len (q0 ^ FlattenSeq <*>(D*))).f)|Seg len <*>(D *) = p | Seg len <*>(D*) by SCMFSA_7:21; consider ki being Nat such that A31: ki = abs((Computation s).k.a1) & Exec(f:=<0,...,0>a1, (Computation s).k).f = ki |-> 0 by SCMFSA_2:101; ki = abs( len p ) by A1,A2,A15,A31,SCMFSA_7:37 .= len p by SCMFSA_7:1; hence len ((Computation s).(len (q0 ^ FlattenSeq <*>(D*))).f) = len p by A22,A29,A31,FINSEQ_2:69; now let b be Int-Location such that A32: b <> a1 & b <> a2; thus (Computation s).(len q0).b = (Computation s).k.b by A29,SCMFSA_2:101 .= s.b by A1,A2,A15,A32,SCMFSA_7:37; end; hence for b being Int-Location st b <> a1 & b <> a2 holds (Computation s).(len (q0 ^ FlattenSeq <*>(D* ))).b = s.b by A22; now let g be FinSeq-Location such that A33: g <> f; thus (Computation s).(len q0).g = (Computation s).k.g by A29,A33,SCMFSA_2:101 .= s.g by A1,A2,A15,SCMFSA_7:37; end; hence thesis by A22; end; A34: for r being FinSequence, x being set st P[r] holds P[r ^ <* x *>] proof let r be FinSequence, x be set; assume A35: P[r]; assume A36: r ^ <* x *> c= pp; now r c= r ^ <* x *> by FINSEQ_6:12; hence r c= pp by A36,XBOOLE_1:1; end; then consider pp0 being FinSequence of D* such that A37: pp0 = r and A38: for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds IC (Computation s).i = insloc i and A39: ((Computation s).(len (q0 ^ FlattenSeq pp0)).f) | Seg len pp0 = p | Seg len pp0 and A40: len ((Computation s).(len (q0 ^ FlattenSeq pp0)).f) = len p and A41: for b being Int-Location st b <> a1 & b <> a2 holds (Computation s).(len (q0 ^ FlattenSeq pp0)).b = s.b and A42: for h being FinSeq-Location st h <> f holds (Computation s).(len (q0 ^ FlattenSeq pp0)).h = s.h by A35; set r1 = len r + 1; A43: now len (r ^ <* x *>) = r1 by FINSEQ_2:19; then r1 in Seg len (r ^ <* x *>) by FINSEQ_1:6; hence r1 in dom (r ^ <* x *>) by FINSEQ_1:def 3; end; A44: now dom (r ^ <* x *>) c= dom pp by A36,GRFUNC_1:8; hence r1 in dom pp by A43; end; then A45: r1 in Seg len pp by FINSEQ_1:def 3; then 1 <= r1 & r1 <= len p by A10,FINSEQ_1:3; then consider pr1 being Integer such that A46: pr1 = p.r1 and A47: pp.r1 = aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *> by A11; A48: now thus x = (r ^ <* x *>).r1 by FINSEQ_1:59 .= pp.r1 by A36,A43,GRFUNC_1:8; end; then x in D* & x is Element of D* by A44,FINSEQ_2:13; then <* x *> is FinSequence of D* by SCMFSA_7:22; then reconsider pp1 = pp0 ^ <* x *> as FinSequence of D* by SCMFSA_7:23; take pp1; thus pp1 = r ^ <* x *> by A37; reconsider x as Element of D* by A44,A48,FINSEQ_2:13; A49: x = aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>) by A47,A48,FINSEQ_1: 45; A50: FlattenSeq pp1 c= FlattenSeq pp by A36,A37,SCMFSA_7:19; A51: now thus FlattenSeq pp1 = FlattenSeq pp0 ^ FlattenSeq <* x *> by SCMFSA_7:14 .= FlattenSeq pp0 ^ x by DTCONSTR:13; end; then A52: q0 ^ FlattenSeq pp1 = q0 ^ FlattenSeq pp0 ^ x by FINSEQ_1:45; set c1 = len (q0 ^ FlattenSeq pp0); set s1 = (Computation s).c1; set c2 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)); set s2 = (Computation s).c2; set c3 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)); A53: c2 = c1 + len aSeq(a1,r1) by FINSEQ_1:35; then A54: s2 = (Computation (Computation s).c1).len aSeq(a1,r1) by AMI_1:51; A55: c3 = c1 + len aSeq(a1,r1) + len aSeq(a2,pr1) by A53,FINSEQ_1:35; A56: c3 = c2 + len aSeq(a2,pr1) by FINSEQ_1:35; A57: now let p be FinSequence; assume p c= x; then FlattenSeq pp0 ^ p c= FlattenSeq pp0 ^ x by FINSEQ_6:15; then FlattenSeq pp0 ^ p c= FlattenSeq pp by A50,A51,XBOOLE_1:1; then q0 ^ (FlattenSeq pp0 ^ p) c= q0 ^ FlattenSeq pp by FINSEQ_6:15; then A58: q0 ^ FlattenSeq pp0 ^ p c= q0 ^ FlattenSeq pp by FINSEQ_1:45; q0 ^ FlattenSeq pp c= q by A12,FINSEQ_6:12; hence q0 ^ FlattenSeq pp0 ^ p c= q by A58,XBOOLE_1:1; end; A59: for c being Nat st c in dom aSeq(a1,r1) holds aSeq(a1,r1).c = s1.insloc (c1 + c -' 1) proof let c be Nat; assume A60: c in dom aSeq(a1,r1); A61: now aSeq(a1,r1) c= x by A49,FINSEQ_6:12; hence q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) c= q by A57; end; then A62: dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)) c= dom q by GRFUNC_1:8; A63: c1 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)) by A60,FINSEQ_1:41; then A64:insloc (c1 + c -' 1) in dom Load q by A6,A62; A65: now c1 + c >= 1 by A63,FINSEQ_3:27; then c1 + c -' 1 = c1 + c - 1 by SCMFSA_7:3; hence c1 + c -' 1 + 1 = c1 + c by XCMPLX_1:27; end; thus aSeq(a1,r1).c = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)).(c1 + c) by A60,FINSEQ_1:def 7 .= q.(c1 + c -' 1 + 1) by A61,A63,A65,GRFUNC_1:8 .= (Load q).insloc (c1 + c -' 1) by A7,A64 .= s.insloc (c1 + c -' 1) by A4,A5,A64,GRFUNC_1:8 .= s1.insloc (c1 + c -' 1) by AMI_1:54; end; A66: s1.O = 1 & IC s1 = insloc c1 by A2,A38,A41; A67: now let i be Nat; assume i <= len aSeq(a1,r1); hence insloc (c1 + i) = IC (Computation s1).i by A59,A66,SCMFSA_7:36 .= IC (Computation s).(c1 + i) by AMI_1:51; end; A68: now let c be Nat; assume A69: c in dom aSeq(a2,pr1); then A70: c2 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)) by FINSEQ_1:41; A71: now aSeq(a1,r1) ^ aSeq(a2,pr1) c= x by A47,A48,FINSEQ_6:12; then q0 ^ FlattenSeq pp0 ^ (aSeq(a1,r1) ^ aSeq(a2,pr1)) c= q by A57; hence q0 ^FlattenSeq pp0^aSeq(a1,r1) ^ aSeq(a2,pr1) c= q by FINSEQ_1:45; end; A72: now dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)) c= dom q by A71,GRFUNC_1:8; hence insloc (c2 + c -' 1) in dom Load q by A6,A70; end; A73: now c2 + c >= 1 by A70,FINSEQ_3:27; hence c2 + c -' 1 + 1 = c2 + c - 1 + 1 by SCMFSA_7:3 .= c2 + c by XCMPLX_1:27; end; thus aSeq(a2,pr1).c = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)).(c2 + c) by A69,FINSEQ_1:def 7 .= q.(c2 + c) by A70,A71,GRFUNC_1:8 .= (Load q).insloc (c2 + c -' 1) by A7,A72,A73 .= s.insloc (c2 + c -' 1) by A4,A5,A72,GRFUNC_1:8 .= s2.insloc (c2 + c -' 1) by AMI_1:54; end; A74: s2.O = 1 & IC s2 = insloc c2 by A53,A54,A59,A66,SCMFSA_7:36; A75: now let i be Nat; assume i <= len aSeq(a2,pr1); hence insloc (c2 + i) = IC (Computation s2).i by A68,A74,SCMFSA_7:36 .= IC (Computation s).(c2 + i) by AMI_1:51; end; A76: now thus len q0 + len FlattenSeq pp1 = len q0 + len (FlattenSeq pp0 ^ aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>)) by A49,A51,FINSEQ_1:45 .= len (q0 ^ (FlattenSeq pp0 ^ aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>))) by FINSEQ_1:35 .= len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>)) by Lm3 .= c2 + len (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>) by FINSEQ_1:35 .= c2 + (len aSeq(a2,pr1) + len <* (f,a1):=a2 *>) by FINSEQ_1:35; end; A77: now thus len q0 + len FlattenSeq pp1 = c2 + (len aSeq(a2,pr1) + 1) by A76,FINSEQ_1:56 .= c2 + len aSeq(a2,pr1) + 1 by XCMPLX_1:1; end; A78: for i being Nat st i < len (q0 ^ FlattenSeq pp1) holds IC (Computation s).i = insloc i proof let i be Nat; assume A79: i < len (q0 ^ FlattenSeq pp1); A80: now assume A81: not i <= c1; assume A82: not (c1 + 1 <= i & i <= c2); i < len q0 + len FlattenSeq pp1 by A79,FINSEQ_1:35; hence c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1) by A77,A81,A82,NAT_1 :38; end; per cases by A80; suppose i <= len (q0 ^ FlattenSeq pp0); hence thesis by A38; suppose A83: c1 + 1 <= i & i <= c2; then c1 + 1 - c1 <= i - c1 by REAL_1:49; then 1 <= i - c1 by XCMPLX_1:26; then A84: 0 <= i - c1 by AXIOMS:22; i - c1 <= c2 - c1 by A83,REAL_1:49; then A85: i - c1 <= len aSeq(a1,r1) by A53,XCMPLX_1:26; reconsider ii = i - c1 as Nat by A84,INT_1:16; thus insloc i = insloc (c1 + ii) by XCMPLX_1:27 .= IC (Computation s).(c1 + ii) by A67,A85 .= IC (Computation s).i by XCMPLX_1:27; suppose A86: c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1); then c2 + 1 - c2 <= i - c2 by REAL_1:49; then 1 <= i - c2 by XCMPLX_1:26; then A87: 0 <= i - c2 by AXIOMS:22; i - c2 <= c2 + len aSeq(a2,pr1) - c2 by A86,REAL_1:49; then A88: i - c2 <= len aSeq(a2,pr1) by XCMPLX_1:26; reconsider ii = i - c2 as Nat by A87,INT_1:16; thus insloc i = insloc (c2 + ii) by XCMPLX_1:27 .= IC (Computation s).(c2 + ii) by A75,A88 .= IC (Computation s).i by XCMPLX_1:27; end; A89: len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(a2,pr1) + 1 & 1 <= c2 + len aSeq(a2,pr1) + 1 by A77,FINSEQ_1:35,NAT_1:29; then A90: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(a2,pr1) by NAT_1:38; A91: q0 ^ FlattenSeq pp1 c= q by A52,A57; A92: now len (q0 ^ FlattenSeq pp1) <= len q by A91,SCMFSA_7:8; hence c2 + len aSeq(a2,pr1) < len q by A89,NAT_1:38; end; A93: 1 <= len <* (f,a1):=a2 *> by FINSEQ_1:57; A94: now len <* (f,a1):=a2 *> <= len (aSeq(a1,r1) ^ aSeq(a2,pr1)) + len <* (f,a1):=a2 *> by NAT_1:37; then len <* (f,a1):=a2 *> <= len (aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *>) by FINSEQ_1:35; hence 1 <= len x by A47,A48,FINSEQ_1:57; end; A95: now thus CurInstr (Computation s).c3 = (Computation s).c3.IC (Computation s).c3 by AMI_1:def 17 .= (Computation s).c3.insloc c3 by A56,A78,A90 .= q.(c3 + 1) by A19,A56,A92 .= (q0 ^ FlattenSeq pp1).(c3 + 1) by A56,A89,A91,SCMFSA_7:18; end; A96: now thus CurInstr (Computation s).c3 = (q0 ^ FlattenSeq pp0 ^ x).(c3 + len <* (f,a1):=a2 *>) by A52,A95,FINSEQ_1:57 .= (q0 ^ FlattenSeq pp0 ^ x).(c1 + (len aSeq(a1,r1) + (len aSeq(a2,pr1) + len <* (f,a1):=a2 *>))) by A55,Lm2; end; A97: now thus CurInstr (Computation s).c3 = (q0 ^ FlattenSeq pp0 ^ x).(c1 + len x) by A47,A48,A96,Lm4 .= (aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *>). len (aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *>) by A47,A48,A94, SCMFSA_7:10 .= (aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *>). (len (aSeq(a1,r1) ^ aSeq(a2,pr1)) + len <* (f,a1):=a2 *>) by FINSEQ_1:35 .= <* (f,a1):=a2 *>.len <* (f,a1):=a2 *> by A93,SCMFSA_7:10 .= <* (f,a1):=a2 *>.1 by FINSEQ_1:57 .= (f,a1):=a2 by FINSEQ_1:57; end; A98: now thus (Computation s).(c3 + 1) = Following (Computation s).c3 by AMI_1:def 19 .= Exec((f,a1):=a2,(Computation s).c3) by A97,AMI_1:def 18; end; then A99: (Computation s).(len (q0 ^ FlattenSeq pp1)) = Exec((f,a1):=a2,(Computation s).c3) by A89,FINSEQ_1:35; A100: now thus IC (Computation s).len (q0 ^ FlattenSeq pp1) = Exec((f,a1):=a2,(Computation s).c3).IC SCM+FSA by A56,A89,A98,AMI_1: def 15 .= Next IC (Computation s).c3 by SCMFSA_2:99 .= Next insloc c3 by A56,A78,A90 .= insloc len (q0 ^ FlattenSeq pp1) by A56,A89,SCMFSA_2:32; end; thus for i being Nat st i <= len (q0 ^ FlattenSeq pp1) holds IC (Computation s).i = insloc i proof let i be Nat; assume A101: i <= len (q0 ^ FlattenSeq pp1); per cases by A101,REAL_1:def 5; suppose i < len (q0 ^ FlattenSeq pp1); hence IC (Computation s).i = insloc i by A78; suppose i = len (q0 ^ FlattenSeq pp1); hence IC (Computation s).i = insloc i by A100; end; consider ki being Nat such that A102: ki = abs((Computation s).c3.a1) & Exec((f,a1):=a2, (Computation s).c3).f = (Computation s).c3.f +*(ki,(Computation s).c3.a2) by SCMFSA_2:99; A103:now thus ki = abs( (Computation s).(c2 + len aSeq(a2,pr1)).a1 ) by A102, FINSEQ_1:35 .= abs( (Computation s2).(len aSeq(a2,pr1)).a1 ) by AMI_1:51 .= abs( s2.a1 ) by A3,A68,A74,SCMFSA_7:36 .= abs( r1 ) by A54,A59,A66,SCMFSA_7:36 .= r1 by SCMFSA_7:1; end; A104: now thus (Computation s).c3.a2 = (Computation s).(c2 + len aSeq(a2,pr1)).a2 by FINSEQ_1:35 .= (Computation s2).(len aSeq(a2,pr1)).a2 by AMI_1:51 .= p.r1 by A46,A68,A74,SCMFSA_7:36; end; A105: now thus (Computation s).c3.f = (Computation s).(c2 + len aSeq(a2,pr1)).f by FINSEQ_1:35 .= (Computation s2).(len aSeq(a2,pr1)).f by AMI_1:51 .= s2.f by A68,A74,SCMFSA_7:36 .= s1.f by A54,A59,A66,SCMFSA_7:36; end; A106: dom (s1.f +*(r1,p.r1)) = dom (s1.f) by FUNCT_7:32; then A107: len (s1.f +*(r1,p.r1)) = len (s1.f) by FINSEQ_3:31; len pp1 <= len pp by A36,A37,SCMFSA_7:8; then A108: Seg len pp1 c= Seg len p by A10,FINSEQ_1:7; A109: now dom ((Computation s).(len (q0 ^ FlattenSeq pp1)).f) = Seg len p by A40,A56,A89,A98,A102,A103,A104,A105,A106,FINSEQ_1:def 3; hence dom (((Computation s).(len (q0 ^ FlattenSeq pp1)).f) | Seg len pp1 ) = Seg len pp1 by A108,RELAT_1:91; end; A110: now Seg len pp1 c= dom p by A108,FINSEQ_1:def 3; hence dom (p | Seg len pp1) = Seg len pp1 by RELAT_1:91; end; for i being Nat st i in Seg len pp1 holds (((Computation s).(len (q0 ^ FlattenSeq pp1)).f) | Seg len pp1).i = (p | Seg len pp1).i proof let i be Nat; assume A111: i in Seg len pp1; then A112: 1 <= i & i <= len pp1 by FINSEQ_1:3; A113: r1 in dom (s1.f) by A10,A40,A45,FINSEQ_1:def 3; per cases; suppose A114: i = len pp1; then A115: i = len pp0 + 1 by FINSEQ_2:19; then A116: i in Seg len pp1 by A114,FINSEQ_1:6; hence (((Computation s).len (q0 ^ FlattenSeq pp1)).f | Seg len pp1). i = (s1.f +*(r1,p.r1)).i by A99,A102,A103,A104,A105,FUNCT_1:72 .= p.r1 by A37,A113,A115,FUNCT_7:33 .= (p | Seg len pp1).i by A37,A115,A116,FUNCT_1:72; suppose A117: i <> len pp1; then A118: i <> r1 by A37,FINSEQ_2:19; 1 <= i & i < len pp1 by A112,A117,REAL_1:def 5; then 1 <= i & i < len pp0 + 1 by FINSEQ_2:19; then 1 <= i & i <= len pp0 by NAT_1:38; then A119: i in Seg len pp0 by FINSEQ_1:3; now thus (((Computation s).(len (q0 ^ FlattenSeq pp1))).f | Seg len pp1).i = (s1.f +*(r1,p.r1)).i by A99,A102,A103,A104,A105,A111,FUNCT_1:72 .= s1.f.i by A118,FUNCT_7:34; end; hence (((Computation s).(len (q0 ^ FlattenSeq pp1))).f | Seg len pp1). i = (p | Seg len pp0).i by A39,A119,FUNCT_1:72 .= p.i by A119,FUNCT_1:72 .= (p | Seg len pp1).i by A111,FUNCT_1:72; end; then for i being set st i in Seg len pp1 holds (((Computation s).(len (q0 ^ FlattenSeq pp1)).f) | Seg len pp1).i = (p | Seg len pp1).i; hence ((Computation s).(len (q0 ^ FlattenSeq pp1)).f) | Seg len pp1 = p | Seg len pp1 by A109,A110,FUNCT_1:9; thus len ((Computation s).(len (q0^FlattenSeq pp1)).f) = len p by A40,A89 ,A98,A102,A103,A104,A105,A107,FINSEQ_1:35; hereby let b be Int-Location; assume A120: b <> a1 & b <> a2; thus (Computation s).(len (q0 ^ FlattenSeq pp1)).b = (Computation s).(c2 + len aSeq(a2,pr1)).b by A56,A89,A98,SCMFSA_2: 99 .= (Computation s2).(len aSeq(a2,pr1)).b by AMI_1:51 .= s2.b by A68,A74,A120,SCMFSA_7:36 .= s1.b by A54,A59,A66,A120,SCMFSA_7:36 .= s.b by A41,A120; end; hereby let h be FinSeq-Location; assume A121: h <> f; hence (Computation s).(len (q0 ^ FlattenSeq pp1)).h = (Computation s).(c2 + len aSeq(a2,pr1)).h by A56,A89,A98,SCMFSA_2: 99 .= (Computation s2).(len aSeq(a2,pr1)).h by AMI_1:51 .= s2.h by A68,A74,SCMFSA_7:36 .= s1.h by A54,A59,A66,SCMFSA_7:36 .= s.h by A42,A121; end; end; for r being FinSequence holds P[r] from IndSeq(A21,A34); then consider pp0 being FinSequence of D* such that A122: pp0 = pp and A123: for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds IC (Computation s).i = insloc i and A124: ((Computation s).(len (q0 ^ FlattenSeq pp0)).f) | Seg len pp0 = p | Seg len pp0 and A125: len ((Computation s).(len (q0 ^ FlattenSeq pp0)).f) = len p and A126: for b being Int-Location st b <> a1 & b <> a2 holds (Computation s).(len (q0 ^ FlattenSeq pp0)).b = s.b and A127: for g being FinSeq-Location st g <> f holds (Computation s).(len (q0 ^ FlattenSeq pp0)).g = s.g; A128: IC (Computation s).len (q0 ^ FlattenSeq pp) = insloc len (q0 ^ FlattenSeq pp) by A122,A123; len q = len (q0 ^ FlattenSeq pp) + 1 by A12,FINSEQ_2:19; then A129: len (q0 ^ FlattenSeq pp) < len q by NAT_1:38; A130: CurInstr (Computation s).len (q0 ^ FlattenSeq pp) = ((Computation s).len (q0 ^ FlattenSeq pp)). insloc len (q0 ^ FlattenSeq pp) by A128,AMI_1:def 17 .= q.(len (q0 ^ FlattenSeq pp) + 1) by A19,A129 .= halt SCM+FSA by A12,FINSEQ_1:59; hence s is halting by AMI_1:def 20; then A131: (Computation s).len (q0^FlattenSeq pp) = Result s by A130,AMI_1: def 22; dom ((Computation s).(len (q0 ^ FlattenSeq pp0)).f) = Seg len pp0 by A10,A122,A125,FINSEQ_1:def 3; then A132: (Result s).f = p | Seg len pp0 by A122,A124,A131,RELAT_1:97; dom p = Seg len pp0 by A10,A122,FINSEQ_1:def 3; hence (Result s).f = p by A132,RELAT_1:97; thus thesis by A122,A126,A127,A131; end; Lm6: ::SCMFSA_7'36 for s being State of SCM+FSA, c0 being Nat st IC s = insloc c0 for a being Int-Location, k being Integer st (for c being Nat st c < len aSeq(a,k) holds aSeq(a,k).(c + 1) = s.insloc (c0 + c)) holds for i being Nat st i <= len aSeq(a,k) holds IC (Computation s).i = insloc (c0 + i) proof let s be State of SCM+FSA; let c0 be Nat; assume A1: IC s = insloc c0; let a be Int-Location; let k be Integer; assume A2: for c being Nat st c < len aSeq(a,k) holds aSeq(a,k).(c + 1) = s.insloc (c0 + c); per cases; suppose A3: k > 0; then reconsider k'= k as Nat by INT_1:16; consider k1 being Nat such that A4: k1 + 1 = k' and A5: aSeq(a,k') = <*a:=intloc 0*> ^ (k1 |-> AddTo(a,intloc 0)) by A3,SCMFSA_7:def 3; A6: len aSeq(a,k') = len <*a:=intloc 0*> + len (k1|->AddTo(a,intloc 0)) by A5, FINSEQ_1:35 .= 1 + len(k1|->AddTo(a,intloc 0)) by FINSEQ_1:56 .= k' by A4,FINSEQ_2:69; defpred Q[Nat] means $1 <= k' implies IC (Computation s).$1 = insloc (c0 + $1); for i being Nat st i <= len aSeq(a,k') holds IC (Computation s).i = insloc (c0 + i) proof let i be Nat; assume A7: i <= len aSeq(a,k'); A8: s.insloc (c0 + 0) = aSeq(a,k').(0 + 1) by A2,A3,A6 .= a:= intloc 0 by A5,FINSEQ_1:58; A9: now let i be Nat; assume A10: 1 < i & i <= k'; then A11: 1 <= i - 1 by SCMFSA_7:4; then 0 <= i - 1 by AXIOMS:22; then reconsider i1 = i - 1 as Nat by INT_1:16; i - 1 <= k' - 1 by A10,REAL_1:49; then i - 1 <= k1 by A4,XCMPLX_1:26; then A12: i1 in Seg k1 by A11,FINSEQ_1:3; len <* a:= intloc 0 *> = 1 by FINSEQ_1:56; hence aSeq(a,k').i = (k1 |-> AddTo(a,intloc 0)).(i - 1) by A5,A6,A10,FINSEQ_1:37 .= AddTo(a,intloc 0) by A12,FINSEQ_2:70; end; A13: now let i be Nat; assume A14: 0 < i & i < k'; then A15: 0 + 1 < i + 1 by REAL_1:53; A16: i + 1 <= k' by A14,NAT_1:38; thus s.insloc (c0 + i) = aSeq(a,k').(i+1) by A2,A6,A14 .=AddTo(a,intloc 0) by A9,A15,A16; end; A17: now let n be Nat; assume n = 0; hence A18: (Computation s).n = s by AMI_1:def 19; hence A19: CurInstr (Computation s).n = a:= intloc 0 by A1,A8,AMI_1:def 17; thus (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(a:= intloc 0,s) by A18,A19,AMI_1:def 18; end; A20: Q[0] by A1,AMI_1:def 19; A21: for n being Nat st Q[n] holds Q[n + 1] proof let n be Nat; assume A22: Q[n]; assume A23: n + 1 <= k'; per cases by NAT_1:19; suppose A24: n = 0; hence IC (Computation s).(n+1) = IC Exec(a:= intloc 0,s) by A17 .= Exec(a:= intloc 0,s).IC SCM+FSA by AMI_1:def 15 .= Next insloc (c0 + n) by A1,A24,SCMFSA_2:89 .= insloc (c0 + n + 1) by SCMFSA_2:32 .= insloc (c0 + (n + 1)) by XCMPLX_1:1; suppose A25: n > 0; A26: n + 0 <= n + 1 by REAL_1:55; A27: 0 < n & n < k' by A23,A25,NAT_1:38; A28: CurInstr (Computation s).n = ((Computation s).n).insloc (c0 + n) by A22,A23,A26,AMI_1:def 17, AXIOMS:22 .= s.insloc (c0 + n) by AMI_1:54 .= AddTo(a,intloc 0) by A13,A27; A29: (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(AddTo(a,intloc 0),(Computation s).n) by A28,AMI_1:def 18; thus IC (Computation s).(n+1) = (Computation s).(n+1).IC SCM+FSA by AMI_1:def 15 .= Next IC (Computation s).n by A29,SCMFSA_2:90 .= insloc (c0 + n + 1) by A22,A23,A26,AXIOMS:22,SCMFSA_2:32 .= insloc (c0 + (n + 1)) by XCMPLX_1:1; end; for i being Nat holds Q[i] from Ind(A20,A21); hence thesis by A6,A7; end; hence for i being Nat st i <= len aSeq(a,k) holds IC (Computation s).i = insloc (c0 + i); suppose A30: k <= 0; then A31: 0 <= - k by REAL_1:26,50; then reconsider mk = - k as Nat by INT_1:16; 0 + 0 <= mk + (1+1) by A31,REAL_1:55; then A32: 0 <= mk+1+1 by XCMPLX_1:1; consider k1 being Nat such that A33: k1 + k = 1 and A34: aSeq(a,k) = <*a:=intloc 0*> ^ (k1 |-> SubFrom(a,intloc 0)) by A30,SCMFSA_7:def 3; A35: k1 = 1 - k by A33,XCMPLX_1:26 .= 1 + mk by XCMPLX_0:def 8; A36: len aSeq(a,k) = len <* a:=intloc 0 *> + len (k1|->SubFrom(a,intloc 0)) by A34,FINSEQ_1: 35 .= 1 + len (k1|->SubFrom(a,intloc 0)) by FINSEQ_1:56 .= mk+1+1 by A35,FINSEQ_2:69; defpred Q[Nat] means $1 <= mk+1+1 implies IC (Computation s).$1 = insloc (c0 + $1); for i being Nat st i <= len aSeq(a,k) holds IC (Computation s).i = insloc (c0 + i) proof let i be Nat; assume A37: i <= len aSeq(a,k); A38: s.insloc (c0 + 0) = aSeq(a,k).(0+1) by A2,A32,A36 .= a:= intloc 0 by A34,FINSEQ_1:58; A39: now let i be Nat; assume A40: 1 < i & i <= mk+1+1; then A41: 1 - 1 < i - 1 by REAL_1:54; then A42: 1 - 1 + 1 <= i - 1 by INT_1:20; reconsider i1 = i - 1 as Nat by A41,INT_1:16; i - 1 <= mk+1+1 - 1 by A40,REAL_1:49; then i - 1 <= k1 by A35,XCMPLX_1:26; then A43: i1 in Seg k1 by A42,FINSEQ_1:3; len <* a:= intloc 0 *> = 1 by FINSEQ_1:56; hence aSeq(a,k).i = (k1|->SubFrom(a,intloc 0)).(i - 1) by A34,A36,A40,FINSEQ_1:37 .= SubFrom(a,intloc 0) by A43,FINSEQ_2:70; end; A44: now let i be Nat; assume A45: 0 < i & i < mk+1+1; then A46: 0 + 1 < i + 1 by REAL_1:53; A47: i + 1 <= mk+1+1 by A45,NAT_1:38; thus s.insloc (c0 + i) = aSeq(a,k).(i+1) by A2,A36,A45 .=SubFrom(a,intloc 0) by A39,A46,A47; end; A48: for n being Nat st n = 0 holds ((Computation s).n = s & CurInstr (Computation s).n = a:= intloc 0 & (Computation s).(n+1) = Exec(a:= intloc 0,s)) proof let n be Nat; assume n = 0; hence A49: (Computation s).n = s by AMI_1:def 19; hence A50: CurInstr (Computation s).n = a:= intloc 0 by A1,A38,AMI_1:def 17; thus (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(a:= intloc 0,s) by A49,A50,AMI_1:def 18; end; A51: Q[0] by A1,AMI_1:def 19; A52: for n being Nat st Q[n] holds Q[n + 1] proof let n be Nat; assume A53: Q[n]; assume A54: n + 1 <= mk+1+1; per cases by NAT_1:19; suppose A55: n = 0; hence IC (Computation s).(n+1) = IC Exec(a:= intloc 0,s) by A48 .= Exec(a:= intloc 0,s).IC SCM+FSA by AMI_1:def 15 .= Next insloc (c0 + n) by A1,A55,SCMFSA_2:89 .= insloc (c0 + n + 1) by SCMFSA_2:32 .= insloc (c0 + (n + 1)) by XCMPLX_1:1; suppose A56: n > 0; A57: n + 0 <= n + 1 by REAL_1:55; A58: 0 < n & n < mk+1+1 by A54,A56,NAT_1:38; A59: CurInstr (Computation s).n = ((Computation s).n).insloc (c0 + n) by A53,A54,A57,AMI_1:def 17, AXIOMS:22 .= s.insloc (c0 + n) by AMI_1:54 .= SubFrom(a,intloc 0) by A44,A58; A60: (Computation s).(n+1) = Following (Computation s).n by AMI_1:def 19 .= Exec(SubFrom(a,intloc 0),(Computation s).n) by A59,AMI_1:def 18; thus IC (Computation s).(n+1) = (Computation s).(n+1).IC SCM+FSA by AMI_1:def 15 .= Next IC (Computation s).n by A60,SCMFSA_2:91 .= insloc (c0 + n + 1) by A53,A54,A57,AXIOMS:22,SCMFSA_2:32 .= insloc (c0 + (n + 1)) by XCMPLX_1:1; end; for i being Nat holds Q[i] from Ind(A51,A52); hence thesis by A36,A37; end; hence for i being Nat st i <= len aSeq(a,k) holds IC (Computation s).i = insloc (c0 + i); end; Lm7: ::SCMFSA_7'37 for s being State of SCM+FSA st IC s = insloc 0 for a being Int-Location, k being Integer st Load aSeq(a,k) c= s holds for i being Nat st i <= len aSeq(a,k) holds IC (Computation s).i = insloc i proof let s be State of SCM+FSA; assume A1: IC s = insloc 0; let a be Int-Location; let k be Integer; assume A2: Load aSeq(a,k) c= s; let i be Nat; assume A3: i <= len aSeq(a,k); now let c be Nat; assume c < len aSeq(a,k); then A4: insloc c in dom Load aSeq(a,k) by SCMFSA_7:29; then A5: c + 1 in dom aSeq(a,k) by SCMFSA_7:26; s.insloc c = (Load aSeq(a,k)).insloc c by A2,A4,GRFUNC_1:8 .= (aSeq(a,k))/.(c + 1) by A4,SCMFSA_7:def 1; hence s.insloc (0 + c) = aSeq(a,k).(c + 1) by A5,FINSEQ_4:def 4; end; then IC (Computation s).i = insloc (0 + i) by A1,A3,Lm6; hence IC (Computation s).i = insloc i; end; Lm8: ::SCMFSA_7'39 for s being State of SCM+FSA st IC s = insloc 0 for f being FinSeq-Location, p being FinSequence of INT st (f := p) c= s holds s is halting proof set D = the Instructions of SCM+FSA; let s be State of SCM+FSA; assume A1: IC s = insloc 0; let f be FinSeq-Location; let p be FinSequence of INT; set a1 = intloc 1; set a2 = intloc 2; assume A2: (f := p) c= s; set q = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *> ^ aSeq(f,p) ^ <* halt SCM+FSA *>; set q0 = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *>; A3: (f := p) = Load q by SCMFSA_7:def 5; A4: now let k be Nat; assume A5: insloc k in dom Load q; then A6: k + 1 in dom q by SCMFSA_7:26; thus (Load q).insloc k = q/.(k + 1) by A5,SCMFSA_7:def 1 .= q.(k + 1) by A6,FINSEQ_4:def 4; end; consider pp being FinSequence of D* such that A7: len pp = len p and A8: for k being Nat st 1 <= k & k <= len p holds ex i being Integer st i = p.k & pp.k = (aSeq(a1,k) ^ aSeq(a2,i) ^ <* (f,a1):= a2 *>) and A9: aSeq(f,p) = FlattenSeq pp by SCMFSA_7:def 4; set k = len aSeq(a1,len p); A10: len q0 = k + 1 by FINSEQ_2:19; q = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *> ^ (aSeq(f,p) ^ <* halt SCM+FSA *>) by FINSEQ_1:45 .= aSeq(a1,len p) ^ (<* f :=<0,...,0> a1 *> ^ (aSeq(f,p) ^ <* halt SCM+FSA *>)) by FINSEQ_1:45; then Load aSeq(a1,len p) c= (f := p) by A3,SCMFSA_7:31; then A11: Load aSeq(a1,len p) c= s by A2,XBOOLE_1:1; A12: now let i be Nat; assume A13: insloc i in dom Load q; then A14: i + 1 in dom q by SCMFSA_7:26; s.insloc i = (Load q).insloc i by A2,A3,A13,GRFUNC_1:8; then s.insloc i = q/.(i + 1) by A13,SCMFSA_7:def 1; hence s.insloc i = q.(i + 1) by A14,FINSEQ_4:def 4; end; A15: now let i,k be Nat; assume i < len q; then A16: insloc i in dom Load q by SCMFSA_7:29; thus ((Computation s).k).insloc i = s.insloc i by AMI_1:54 .= q.(i + 1) by A12,A16; end; defpred P[FinSequence] means $1 c= pp implies ex pp0 being FinSequence of D* st (pp0 = $1 & for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds IC (Computation s).i = insloc i); A17: P[{}] proof A18: q0 ^ FlattenSeq <*>(D*) = q0 ^ <*>D by SCMFSA_7:13 .= q0 by FINSEQ_1:47; assume {} c= pp; A19: now let i be Nat such that A20: i < len q0; i < len q0 implies i <= len aSeq(a1,len p) by A10,NAT_1:38; hence IC (Computation s).i = insloc i by A1,A11,A20,Lm7; end; k < len q0 by A10,NAT_1:38; then A21: IC (Computation s).k = insloc k by A19; A22: q = aSeq(a1,len p) ^ <* f :=<0,...,0> a1 *> ^ (aSeq(f,p) ^ <* halt SCM+FSA *>) by FINSEQ_1:45; then len q = len q0 + len ((aSeq(f,p) ^ <* halt SCM+FSA *>)) by FINSEQ_1:35; then len q0 <= len q by NAT_1:29; then A23: k < len q by A10,NAT_1:38; A24: 1 <= len q0 by A10,NAT_1:29; A25: CurInstr (Computation s).k = ((Computation s).k).insloc k by A21,AMI_1:def 17 .= q.len q0 by A10,A15,A23 .= q0.len q0 by A22,A24,SCMFSA_7:9 .= f:=<0,...,0>a1 by A10,FINSEQ_1:59; A26: (Computation s).len q0 = Following (Computation s).k by A10,AMI_1:def 19 .= Exec(f:=<0,...,0>a1,(Computation s).k) by A25,AMI_1:def 18; A27: IC (Computation s).len q0 = (Computation s).len q0.IC SCM+FSA by AMI_1:def 15 .= Next IC (Computation s).k by A26,SCMFSA_2:101 .= insloc len q0 by A10,A21,SCMFSA_2:32; take <*>(D*); thus <*>(D*) = {}; now let i be Nat; assume i <= len q0; then i < len q0 or i = len q0 by REAL_1:def 5; hence IC (Computation s).i = insloc i by A19,A27; end; hence for i being Nat st i <= len (q0 ^ FlattenSeq <*>(D*)) holds IC (Computation s).i = insloc i by A18; end; A28: for r being FinSequence, x being set st P[r] holds P[r ^ <* x *>] proof let r be FinSequence; let x be set; assume A29: P[r]; assume A30: r ^ <* x *> c= pp; r c= r ^ <* x *> by FINSEQ_6:12; then consider pp0 being FinSequence of D* such that A31: pp0 = r and A32: for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds IC (Computation s).i = insloc i by A29,A30,XBOOLE_1:1; set r1 = len r + 1; len (r ^ <* x *>) = r1 by FINSEQ_2:19; then r1 in Seg len (r ^ <* x *>) by FINSEQ_1:6; then A33: r1 in dom (r ^ <* x *>) by FINSEQ_1:def 3; A34: dom (r ^ <* x *>) c= dom pp by A30,GRFUNC_1:8; then r1 in dom pp by A33; then r1 in Seg len pp by FINSEQ_1:def 3; then 1 <= r1 & r1 <= len pp by FINSEQ_1:3; then consider pr1 being Integer such that pr1 = p.r1 and A35: pp.r1 = aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *> by A7,A8; A36: now thus x = (r ^ <* x *>).r1 by FINSEQ_1:59 .= pp.r1 by A30,A33,GRFUNC_1:8; end; then x in D* by A33,A34,FINSEQ_2:13; then <* x *> is FinSequence of D* by SCMFSA_7:22; then reconsider pp1 = pp0 ^ <* x *> as FinSequence of D* by SCMFSA_7:23; take pp1; thus pp1 = r ^ <* x *> by A31; reconsider x as Element of D* by A33,A34,A36,FINSEQ_2:13; A37: x = aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>) by A35,A36,FINSEQ_1: 45; A38: FlattenSeq pp1 c= FlattenSeq pp by A30,A31,SCMFSA_7:19; A39: FlattenSeq pp1 = FlattenSeq pp0 ^ FlattenSeq <* x *> by SCMFSA_7:14 .= FlattenSeq pp0 ^ x by DTCONSTR:13; then A40: q0 ^ FlattenSeq pp1 = q0 ^ FlattenSeq pp0 ^ x by FINSEQ_1:45; set c1 = len (q0 ^ FlattenSeq pp0); set s1 = (Computation s).c1; set c2 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)); set s2 = (Computation s).c2; set c3 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)); A41: c2 = c1 + len aSeq(a1,r1) by FINSEQ_1:35; then A42: s2 = (Computation (Computation s).c1).len aSeq(a1,r1) by AMI_1:51; A43: c3 = c1 + len aSeq(a1,r1) + len aSeq(a2,pr1) by A41,FINSEQ_1:35; A44: c3 = c2 + len aSeq(a2,pr1) by FINSEQ_1:35; A45: now let p be FinSequence; assume p c= x; then FlattenSeq pp0 ^ p c= FlattenSeq pp0 ^ x by FINSEQ_6:15; then FlattenSeq pp0 ^ p c= FlattenSeq pp by A38,A39,XBOOLE_1:1; then q0 ^ (FlattenSeq pp0 ^ p) c= q0 ^ FlattenSeq pp by FINSEQ_6:15; then A46: q0 ^ FlattenSeq pp0 ^ p c= q0 ^ FlattenSeq pp by FINSEQ_1:45; q0 ^ FlattenSeq pp c= q by A9,FINSEQ_6:12; hence q0 ^ FlattenSeq pp0 ^ p c= q by A46,XBOOLE_1:1; end; A47: IC s1 = insloc c1 & for c being Nat st c < len aSeq(a1,r1) holds aSeq(a1,r1).(c + 1) = s1.insloc (c1 + c) proof thus IC s1 = insloc c1 by A32; let c be Nat; assume A48: c < len aSeq(a1,r1); aSeq(a1,r1) c= x by A37,FINSEQ_6:12; then A49: q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) c= q by A45; then A50: dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)) c= dom q by GRFUNC_1:8; 1 <= c + 1 & c + 1 <= len aSeq(a1,r1) by A48,SCMFSA_7:28; then A51: c + 1 in dom aSeq(a1,r1) by FINSEQ_3:27; then A52: c1 + (c + 1) in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)) by FINSEQ_1:41; then c1 + (c + 1) in dom q by A50; then c1 + c + 1 in dom q by XCMPLX_1:1; then A53: insloc (c1 + c) in dom Load q by SCMFSA_7:26; thus aSeq(a1,r1).(c + 1) = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1)).(c1 + (c + 1)) by A51,FINSEQ_1:def 7 .= q.(c1 + (c + 1)) by A49,A52,GRFUNC_1:8 .= q.(c1 + c + 1) by XCMPLX_1:1 .= (Load q).insloc (c1 + c) by A4,A53 .= s.insloc (c1 + c) by A2,A3,A53,GRFUNC_1:8 .= s1.insloc (c1 + c) by AMI_1:54; end; A54: now let i be Nat; assume i <= len aSeq(a1,r1); hence insloc (c1 + i) = IC (Computation s1).i by A47,Lm6 .= IC (Computation s).(c1 + i) by AMI_1:51; end; A55: IC s2 = insloc c2 & (for c being Nat st c < len aSeq(a2,pr1) holds aSeq(a2,pr1).(c + 1) = s2.insloc (c2 + c)) proof thus IC s2 = insloc c2 by A41,A42,A47,Lm6; let c be Nat; assume c < len aSeq(a2,pr1); then 1 <= c + 1 & c + 1 <= len aSeq(a2,pr1) by SCMFSA_7:28; then A56: c + 1 in dom aSeq(a2,pr1) by FINSEQ_3:27; then A57: c2 + (c + 1) in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)) by FINSEQ_1:41; aSeq(a1,r1) ^ aSeq(a2,pr1) c= x by A35,A36,FINSEQ_6:12; then q0 ^ FlattenSeq pp0 ^ (aSeq(a1,r1) ^ aSeq(a2,pr1)) c= q by A45; then A58: q0 ^FlattenSeq pp0^aSeq(a1,r1) ^ aSeq(a2,pr1) c= q by FINSEQ_1:45; then dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)) c= dom q by GRFUNC_1:8; then c2 + (c + 1) in dom q by A57; then c2 + c + 1 in dom q by XCMPLX_1:1; then A59: insloc (c2 + c) in dom Load q by SCMFSA_7:26; thus aSeq(a2,pr1).(c + 1) = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ aSeq(a2,pr1)).(c2 + (c + 1)) by A56,FINSEQ_1:def 7 .= q.(c2 + (c + 1)) by A57,A58,GRFUNC_1:8 .= q.(c2 + c + 1) by XCMPLX_1:1 .= (Load q).insloc (c2 + c) by A4,A59 .= s.insloc (c2 + c) by A2,A3,A59,GRFUNC_1:8 .= s2.insloc (c2 + c) by AMI_1:54; end; A60: now let i be Nat; assume i <= len aSeq(a2,pr1); hence insloc (c2 + i) = IC (Computation s2).i by A55,Lm6 .= IC (Computation s).(c2 + i) by AMI_1:51; end; A61: now thus len q0 + len FlattenSeq pp1 = len q0 + len (FlattenSeq pp0 ^ aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>)) by A37,A39,FINSEQ_1:45 .= len (q0 ^ (FlattenSeq pp0 ^ aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>))) by FINSEQ_1:35 .= len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1) ^ (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>)) by Lm3 .= c2 + len (aSeq(a2,pr1) ^ <* (f,a1):=a2 *>) by FINSEQ_1:35 .= c2 + (len aSeq(a2,pr1) + len <* (f,a1):=a2 *>) by FINSEQ_1:35 .= c2 + (len aSeq(a2,pr1) + 1) by FINSEQ_1:56 .= c2 + len aSeq(a2,pr1) + 1 by XCMPLX_1:1; end; A62: for i being Nat st i < len (q0 ^ FlattenSeq pp1) holds IC (Computation s).i = insloc i proof let i be Nat; assume A63: i < len (q0 ^ FlattenSeq pp1); A64: now assume A65: not i <= c1; assume A66: not (c1 + 1 <= i & i <= c2); i < len q0 + len FlattenSeq pp1 by A63,FINSEQ_1:35; hence c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1) by A61,A65,A66,NAT_1 :38; end; per cases by A64; suppose i <= len (q0 ^ FlattenSeq pp0); hence thesis by A32; suppose A67: c1 + 1 <= i & i <= c2; then c1 + 1 - c1 <= i - c1 by REAL_1:49; then 1 <= i - c1 by XCMPLX_1:26; then A68: 0 <= i - c1 by AXIOMS:22; i - c1 <= c2 - c1 by A67,REAL_1:49; then A69: i - c1 <= len aSeq(a1,r1) by A41,XCMPLX_1:26; reconsider ii = i - c1 as Nat by A68,INT_1:16; insloc i = insloc (c1 + ii) by XCMPLX_1:27; then insloc i = IC (Computation s).(c1 + ii) by A54,A69; hence insloc i = IC (Computation s).i by XCMPLX_1:27; suppose A70: c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1); then c2 + 1 - c2 <= i - c2 by REAL_1:49; then 1 <= i - c2 by XCMPLX_1:26; then A71: 0 <= i - c2 by AXIOMS:22; i - c2 <= c2 + len aSeq(a2,pr1) - c2 by A70,REAL_1:49; then A72: i - c2 <= len aSeq(a2,pr1) by XCMPLX_1:26; reconsider ii = i - c2 as Nat by A71,INT_1:16; thus insloc i = insloc (c2 + ii) by XCMPLX_1:27 .= IC (Computation s).(c2 + ii) by A60,A72 .= IC (Computation s).i by XCMPLX_1:27; end; A73: len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(a2,pr1) + 1 & 1 <= c2 + len aSeq(a2,pr1) + 1 by A61,FINSEQ_1:35,NAT_1:29; then A74: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(a2,pr1) by NAT_1:38; A75: q0 ^ FlattenSeq pp1 c= q by A40,A45; A76: now len (q0 ^ FlattenSeq pp1) <= len q by A75,SCMFSA_7:8; hence c2 + len aSeq(a2,pr1) < len q by A73,NAT_1:38; end; A77: 1 <= len <* (f,a1):=a2 *> by FINSEQ_1:57; A78: now len <* (f,a1):= a2 *> <= len (aSeq(a1,r1) ^ aSeq(a2,pr1)) + len <* (f,a1):= a2 *> by NAT_1:37; then len <* (f,a1):= a2 *> <= len (aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):= a2 *>) by FINSEQ_1:35; hence 1 <= len x by A35,A36,FINSEQ_1:57; end; A79: now thus CurInstr (Computation s).c3 = (Computation s).c3.IC (Computation s).c3 by AMI_1:def 17 .= (Computation s).c3.insloc c3 by A44,A62,A74 .= q.(c3 + 1) by A15,A44,A76 .= (q0 ^ FlattenSeq pp0 ^ x).(c3 + 1) by A40,A44,A73,A75,SCMFSA_7:18 .= (q0 ^ FlattenSeq pp0 ^ x).(c1 + len aSeq(a1,r1) + len aSeq(a2,pr1) + len <* (f,a1):=a2 *>) by A43,FINSEQ_1:57 .= (q0 ^ FlattenSeq pp0 ^ x).(c1 + (len aSeq(a1,r1) + (len aSeq(a2,pr1) + len <* (f,a1):=a2 *>))) by Lm2 .= (q0 ^ FlattenSeq pp0 ^ x).(c1 + len x) by A35,A36,Lm4 .= x.len x by A78,SCMFSA_7:10; end; A80: now thus CurInstr (Computation s).c3 = (aSeq(a1,r1) ^ aSeq(a2,pr1) ^ <* (f,a1):=a2 *>). (len (aSeq(a1,r1) ^ aSeq(a2,pr1)) + len <* (f,a1):= a2 *>) by A35,A36,A79,FINSEQ_1:35 .= <* (f,a1):=a2 *>.len <* (f,a1):=a2 *> by A77,SCMFSA_7:10 .= <* (f,a1):=a2 *>.1 by FINSEQ_1:57 .= (f,a1):=a2 by FINSEQ_1:57; end; A81: now thus (Computation s).(c3 + 1) = Following (Computation s).c3 by AMI_1:def 19 .= Exec((f,a1):=a2,(Computation s).c3) by A80,AMI_1:def 18; end; A82: now thus IC (Computation s).len (q0 ^ FlattenSeq pp1) = Exec((f,a1):=a2,(Computation s).c3).IC SCM+FSA by A44,A73,A81,AMI_1: def 15 .= Next IC (Computation s).c3 by SCMFSA_2:99 .= Next insloc c3 by A44,A62,A74; end; thus for i being Nat st i <= len (q0 ^ FlattenSeq pp1) holds IC (Computation s).i = insloc i proof let i be Nat; assume A83: i <= len (q0 ^ FlattenSeq pp1); per cases by A83,REAL_1:def 5; suppose i < len (q0 ^ FlattenSeq pp1); hence IC (Computation s).i = insloc i by A62; suppose i = len (q0 ^ FlattenSeq pp1); hence IC (Computation s).i = insloc i by A44,A73,A82,SCMFSA_2:32; end; end; for r being FinSequence holds P[r] from IndSeq(A17,A28); then consider pp0 being FinSequence of D* such that A84: pp0 = pp and A85: for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds IC (Computation s).i = insloc i; A86: IC (Computation s).len (q0 ^ FlattenSeq pp) = insloc len (q0 ^ FlattenSeq pp) by A84,A85; len q = len (q0 ^ FlattenSeq pp) + 1 by A9,FINSEQ_2:19; then A87: len (q0 ^ FlattenSeq pp) < len q by NAT_1:38; CurInstr (Computation s).len (q0 ^ FlattenSeq pp) = ((Computation s).len (q0 ^ FlattenSeq pp)). insloc len (q0 ^ FlattenSeq pp) by A86,AMI_1:def 17 .= q.(len (q0 ^ FlattenSeq pp) + 1) by A15,A87 .= halt SCM+FSA by A9,FINSEQ_1:59; hence s is halting by AMI_1:def 20; end; definition let f be FinSeq-Location, p be FinSequence of INT; cluster f := p -> initial programmed; coherence proof f := p = Load (aSeq(intloc 1,len p) ^ <* f :=<0,...,0> intloc 1 *> ^ aSeq(f,p) ^ <* halt SCM+FSA *> ) by SCMFSA_7:def 5; hence f := p is initial programmed; end; end; definition let f be FinSeq-Location, p be FinSequence of INT; cluster f := p -> parahalting; correctness proof now let s be State of SCM+FSA; assume A1: (f := p) +* Start-At insloc 0 c= s; A2: IC SCM+FSA in dom ((f := p) +* Start-At insloc 0) by SF_MASTR:65; A3: IC s = s.IC SCM+FSA by AMI_1:def 15 .= ((f := p) +* Start-At insloc 0).IC SCM+FSA by A1,A2,GRFUNC_1:8 .= insloc 0 by SF_MASTR:66; (f := p) c= s by A1,SCMFSA6B:5; hence s is halting by A3,Lm8; end; then (f := p) +* Start-At insloc 0 is halting by AMI_1:def 26; hence (f := p) is parahalting by SCMFSA6B:def 3; end; end; theorem ::*TG1 for s being State of SCM+FSA, f being FinSeq-Location, p being FinSequence of INT holds IExec(f := p,s).f = p & (for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds IExec(f := p,s).a = s.a) & for g being FinSeq-Location st g <> f holds IExec(f := p,s).g = s.g proof let s be State of SCM+FSA; let f be FinSeq-Location; let p be FinSequence of INT; set s1 = s +* Initialized (f := p); IC SCM+FSA in dom Initialized (f := p) by SCMFSA6A:24; then s1.IC SCM+FSA = (Initialized (f := p)).IC SCM+FSA by FUNCT_4:14 .= insloc 0 by SCMFSA6A:46; then A1: IC s1 = insloc 0 by AMI_1:def 15; intloc 0 in dom Initialized (f := p) by SCMFSA6A:45; then A2: s1.intloc 0 = (Initialized (f := p)).intloc 0 by FUNCT_4:14 .= 1 by SCMFSA6A:46; A3: Initialized (f := p) c= s1 by FUNCT_4:26; (f := p) c= Initialized (f := p) by SCMFSA6A:26; then A4: (f := p) c= s1 by A3,XBOOLE_1:1; A5: IExec((f := p),s) = Result s1 +* s | A by SCMFSA6B:def 1; not f in A by SCMFSA_2:85; then not f in dom s /\ A by XBOOLE_0:def 3; then not f in dom (s | A) by RELAT_1:90; hence IExec((f := p),s).f = (Result s1).f by A5,FUNCT_4:12 .= p by A1,A2,A4,Lm5; hereby let a be read-write Int-Location; assume A6: a <> intloc 1 & a <> intloc 2; A7: not a in dom Initialized (f := p) by SCMFSA6A:48; not a in A by SCMFSA_2:84; then not a in dom s /\ A by XBOOLE_0:def 3; then not a in dom (s | A) by RELAT_1:90; hence IExec((f := p),s).a = (Result s1).a by A5,FUNCT_4:12 .= s1.a by A1,A2,A4,A6,Lm5 .= s.a by A7,FUNCT_4:12; end; let g be FinSeq-Location; assume A8: g <> f; A9: not g in dom Initialized (f := p) by SCMFSA6A:49; not g in A by SCMFSA_2:85; then not g in dom s /\ A by XBOOLE_0:def 3; then not g in dom (s | A) by RELAT_1:90; hence IExec((f := p),s).g = (Result s1).g by A5,FUNCT_4:12 .= s1.g by A1,A2,A4,A8,Lm5 .= s.g by A9,FUNCT_4:12; end; definition let i be Instruction of SCM+FSA; let a be Int-Location; pred i does_not_refer a means ::D20' for b being Int-Location for l being Instruction-Location of SCM+FSA 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 programmed FinPartState of SCM+FSA; let a be Int-Location; pred I does_not_refer a means ::D20 for i being Instruction of SCM+FSA st i in rng I holds i does_not_refer a; end; definition let i be Instruction of SCM+FSA; let a be Int-Location; pred i does_not_destroy a means :Def3: ::D19' 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 FinPartState of SCM+FSA; let a be Int-Location; pred I does_not_destroy a means :Def4: ::D19 for i being Instruction of SCM+FSA st i in rng I holds i does_not_destroy a; end; definition let I be FinPartState of SCM+FSA; attr I is good means :Def5: ::Dg I does_not_destroy intloc 0; end; definition let I be FinPartState of SCM+FSA; attr I is halt-free means :Def6: ::D8 not halt SCM+FSA in rng I; end; definition cluster halt-free good Macro-Instruction; existence proof set I = Load (<*>(the Instructions of SCM+FSA)); A1: card I = len <*>(the Instructions of SCM+FSA) by SCMFSA_7:25 .= 0 by FINSEQ_1:25; now assume halt SCM+FSA in rng I; then consider x being set such that A2: x in dom I and I.x = halt SCM+FSA by FUNCT_1:def 5; dom I c= A by AMI_3:def 13; then consider k being Nat such that A3: x = insloc k by A2,SCMFSA_2:21; k < 0 by A1,A2,A3,SCMFSA6A:15; hence contradiction by NAT_1:18; end; then A4: I is halt-free by Def6; now let i be Instruction of SCM+FSA; assume i in rng I & not i does_not_destroy intloc 0; then consider x being set such that A5: x in dom I and I.x = i by FUNCT_1:def 5; dom I c= A by AMI_3:def 13; then consider k being Nat such that A6: x = insloc k by A5,SCMFSA_2:21; k < 0 by A1,A5,A6,SCMFSA6A:15; hence contradiction by NAT_1:18; end; then I does_not_destroy intloc 0 by Def4; then I is good by Def5; hence thesis by A4; end; end; theorem Th11: ::R0'' for a being Int-Location holds halt SCM+FSA does_not_destroy a proof let a be Int-Location; now let b be Int-Location; let l be Instruction-Location of SCM+FSA; let f be FinSeq-Location; thus a := b <> halt SCM+FSA by SCMFSA_2:42,124; thus AddTo(a,b) <> halt SCM+FSA by SCMFSA_2:43,124; thus SubFrom(a,b) <> halt SCM+FSA by SCMFSA_2:44,124; thus MultBy(a,b) <> halt SCM+FSA by SCMFSA_2:45,124; thus Divide(a,b) <> halt SCM+FSA & Divide(b,a) <> halt SCM+FSA by SCMFSA_2:46,124; thus a :=(f,b) <> halt SCM+FSA by SCMFSA_2:50,124; thus a :=len f <> halt SCM+FSA by SCMFSA_2:52,124; end; hence halt SCM+FSA does_not_destroy a by Def3; end; theorem Th12: ::R1'' 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 Instruction-Location of SCM+FSA; let f be FinSeq-Location; thus a := e <> b := c by A1,SF_MASTR:5; A2: 1 <> 2 & 1 <> 3 & 1 <> 4 & 1 <> 5 & 1 <> 9 & 1 <> 11 & InsCode (b := c) = 1 by SCMFSA_2:42; hence AddTo(a,e) <> b := c by SCMFSA_2:43; thus SubFrom(a,e) <> b := c by A2,SCMFSA_2:44; thus MultBy(a,e) <> b := c by A2,SCMFSA_2:45; thus Divide(a,e) <> b := c & Divide(e,a) <> b := c by A2,SCMFSA_2:46; thus a :=(f,e) <> b := c by A2,SCMFSA_2:50; thus a :=len f <> b := c by A2,SCMFSA_2:52; end; hence b := c does_not_destroy a by Def3; end; theorem Th13: ::R2'' 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 Instruction-Location of SCM+FSA; let f be FinSeq-Location; A2: 2 <> 1 & 2 <> 3 & 2 <> 4 & 2 <> 5 & 2 <> 9 & 2 <> 11 & InsCode AddTo(b,c) = 2 by SCMFSA_2:43; hence a := e <> AddTo(b,c) by SCMFSA_2:42; thus AddTo(a,e) <> AddTo(b,c) by A1,SF_MASTR:6; thus SubFrom(a,e) <> AddTo(b,c) by A2,SCMFSA_2:44; thus MultBy(a,e) <> AddTo(b,c) by A2,SCMFSA_2:45; thus Divide(a,e) <> AddTo(b,c) & Divide(e,a) <> AddTo(b,c) by A2,SCMFSA_2:46; thus a :=(f,e) <> AddTo(b,c) by A2,SCMFSA_2:50; thus a :=len f <> AddTo(b,c) by A2,SCMFSA_2:52; end; hence AddTo(b,c) does_not_destroy a by Def3; end; theorem Th14: ::R3'' 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 Instruction-Location of SCM+FSA; let f be FinSeq-Location; A2: 3 <> 1 & 3 <> 2 & 3 <> 4 & 3 <> 5 & 3 <> 9 & 3 <> 11 & InsCode SubFrom(b,c) = 3 by SCMFSA_2:44; hence a := e <> SubFrom(b,c) by SCMFSA_2:42; thus AddTo(a,e) <> SubFrom(b,c) by A2,SCMFSA_2:43; thus SubFrom(a,e) <> SubFrom(b,c) by A1,SF_MASTR:7; thus MultBy(a,e) <> SubFrom(b,c) by A2,SCMFSA_2:45; thus Divide(a,e) <> SubFrom(b,c) & Divide(e,a) <> SubFrom(b,c) by A2,SCMFSA_2:46; thus a :=(f,e) <> SubFrom(b,c) by A2,SCMFSA_2:50; thus a :=len f <> SubFrom(b,c) by A2,SCMFSA_2:52; end; hence SubFrom(b,c) does_not_destroy a by Def3; end; theorem ::R4'' 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 Instruction-Location of SCM+FSA; let f be FinSeq-Location; A2: 4 <> 1 & 4 <> 2 & 4 <> 3 & 4 <> 5 & 4 <> 9 & 4 <> 11 & InsCode MultBy(b,c) = 4 by SCMFSA_2:45; hence a := e <> MultBy(b,c) by SCMFSA_2:42; thus AddTo(a,e) <> MultBy(b,c) by A2,SCMFSA_2:43; thus SubFrom(a,e) <> MultBy(b,c) by A2,SCMFSA_2:44; thus MultBy(a,e) <> MultBy(b,c) by A1,SF_MASTR:8; thus Divide(a,e) <> MultBy(b,c) & Divide(e,a) <> MultBy(b,c) by A2,SCMFSA_2:46; thus a :=(f,e) <> MultBy(b,c) by A2,SCMFSA_2:50; thus a :=len f <> MultBy(b,c) by A2,SCMFSA_2:52; end; hence MultBy(b,c) does_not_destroy a by Def3; end; theorem ::R5'' 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 Instruction-Location of SCM+FSA; let h be FinSeq-Location; A2: 5 <> 1 & 5 <> 2 & 5 <> 3 & 5 <> 4 & 5 <> 9 & 5 <> 11 & InsCode Divide(b,c) = 5 by SCMFSA_2:46; hence a := e <> Divide(b,c) by SCMFSA_2:42; thus AddTo(a,e) <> Divide(b,c) by A2,SCMFSA_2:43; thus SubFrom(a,e) <> Divide(b,c) by A2,SCMFSA_2:44; thus MultBy(a,e) <> Divide(b,c) by A2,SCMFSA_2:45; thus Divide(e,a) <> Divide(b,c) & Divide(a,e) <> Divide(b,c) by A1,SF_MASTR:9; thus a := (h,e) <> Divide(b,c) by A2,SCMFSA_2:50; thus a :=len h <> Divide(b,c) by A2,SCMFSA_2:52; end; hence Divide(b,c) does_not_destroy a by Def3; end; theorem ::R6'' for a being Int-Location, l being Instruction-Location of SCM+FSA holds goto l does_not_destroy a proof let a be Int-Location; let l be Instruction-Location of SCM+FSA; now let b be Int-Location; let r be Instruction-Location of SCM+FSA; let f be FinSeq-Location; A1: 6 <> 1 & 6 <> 2 & 6 <> 3 & 6 <> 4 & 6 <> 5 & 6 <> 9 & 6 <> 11 & InsCode goto l = 6 by SCMFSA_2:47; hence a := b <> goto l by SCMFSA_2:42; thus AddTo(a,b) <> goto l by A1,SCMFSA_2:43; thus SubFrom(a,b) <> goto l by A1,SCMFSA_2:44; thus MultBy(a,b) <> goto l by A1,SCMFSA_2:45; thus Divide(a,b) <> goto l & Divide(b,a) <> goto l by A1,SCMFSA_2:46; thus a :=(f,b) <> goto l by A1,SCMFSA_2:50; thus a :=len f <> goto l by A1,SCMFSA_2:52; end; hence goto l does_not_destroy a by Def3; end; theorem ::R7'' for a,b being Int-Location, l being Instruction-Location of SCM+FSA holds b =0_goto l does_not_destroy a proof let a,b be Int-Location; let l be Instruction-Location of SCM+FSA; now let e be Int-Location; let f be FinSeq-Location; A1: 7 <> 1 & 7 <> 2 & 7 <> 3 & 7 <> 4 & 7 <> 5 & 7 <> 9 & 7 <> 11 & InsCode (b =0_goto l) = 7 by SCMFSA_2:48; hence a := e <> b =0_goto l by SCMFSA_2:42; thus AddTo(a,e) <> b =0_goto l by A1,SCMFSA_2:43; thus SubFrom(a,e) <> b =0_goto l by A1,SCMFSA_2:44; thus MultBy(a,e) <> b =0_goto l by A1,SCMFSA_2:45; thus Divide(a,e) <> b =0_goto l & Divide(e,a) <> b =0_goto l by A1,SCMFSA_2:46; thus a :=(f,e) <> b =0_goto l by A1,SCMFSA_2:50; thus a :=len f <> b =0_goto l by A1,SCMFSA_2:52; end; hence b =0_goto l does_not_destroy a by Def3; end; theorem ::R8'' for a,b being Int-Location, l being Instruction-Location of SCM+FSA holds b >0_goto l does_not_destroy a proof let a,b be Int-Location; let l be Instruction-Location of SCM+FSA; now let e be Int-Location; let f be FinSeq-Location; A1: 8 <> 1 & 8 <> 2 & 8 <> 3 & 8 <> 4 & 8 <> 5 & 8 <> 9 & 8 <> 11 & InsCode (b >0_goto l) = 8 by SCMFSA_2:49; hence a := e <> b >0_goto l by SCMFSA_2:42; thus AddTo(a,e) <> b >0_goto l by A1,SCMFSA_2:43; thus SubFrom(a,e) <> b >0_goto l by A1,SCMFSA_2:44; thus MultBy(a,e) <> b >0_goto l by A1,SCMFSA_2:45; thus Divide(a,e) <> b >0_goto l & Divide(e,a) <> b >0_goto l by A1,SCMFSA_2:46; thus a :=(f,e) <> b >0_goto l by A1,SCMFSA_2:50; thus a :=len f <> b >0_goto l by A1,SCMFSA_2:52; end; hence b >0_goto l does_not_destroy a by Def3; end; theorem ::R9'' 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 Instruction-Location of SCM+FSA; let h be FinSeq-Location; A2: 9 <> 1 & 9 <> 2 & 9 <> 3 & 9 <> 4 & 9 <> 5 & 9 <> 11 & InsCode (b := (f,c)) = 9 by SCMFSA_2:50; hence a := e <> b := (f,c) by SCMFSA_2:42; thus AddTo(a,e) <> b := (f,c) by A2,SCMFSA_2:43; thus SubFrom(a,e) <> b := (f,c) by A2,SCMFSA_2:44; thus MultBy(a,e) <> b := (f,c) by A2,SCMFSA_2:45; thus Divide(a,e) <> b := (f,c) & Divide(e,a) <> b := (f,c) by A2,SCMFSA_2:46; thus a := (h,e) <> b := (f,c) by A1,SF_MASTR:13; thus a :=len h <> b := (f,c) by A2,SCMFSA_2:52; end; hence b :=(f,c) does_not_destroy a by Def3; end; theorem ::R10'' 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: 10 <> 1 & 10 <> 2 & 10 <> 3 & 10 <> 4 & 10 <> 5 & 10 <> 9 & 10 <> 11 & InsCode ((f,c) := b) = 10 by SCMFSA_2:51; hence a := e <> (f,c) := b by SCMFSA_2:42; thus AddTo(a,e) <> (f,c) := b by A1,SCMFSA_2:43; thus SubFrom(a,e) <> (f,c) := b by A1,SCMFSA_2:44; thus MultBy(a,e) <> (f,c) := b by A1,SCMFSA_2:45; thus Divide(e,a) <> (f,c) := b & Divide(a,e) <> (f,c) := b by A1,SCMFSA_2:46; thus a := (h,e) <> (f,c) := b by A1,SCMFSA_2:50; thus a :=len h <> (f,c) := b by A1,SCMFSA_2:52; end; hence (f,c):= b does_not_destroy a by Def3; end; theorem ::R11'' 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: 11 <> 1 & 11 <> 2 & 11 <> 3 & 11 <> 4 & 11 <> 5 & 11 <> 9 & InsCode (b :=len f) = 11 by SCMFSA_2:52; hence a := c <> b :=len f by SCMFSA_2:42; thus AddTo(a,c) <> b :=len f by A2,SCMFSA_2:43; thus SubFrom(a,c) <> b :=len f by A2,SCMFSA_2:44; thus MultBy(a,c) <> b :=len f by A2,SCMFSA_2:45; thus Divide(a,c) <> b :=len f & Divide(c,a) <> b :=len f by A2,SCMFSA_2:46; thus a :=(g,c) <> b :=len f by A2,SCMFSA_2:50; thus a :=len g <> b :=len f by A1,SF_MASTR:15; end; hence b :=len f does_not_destroy a by Def3; end; theorem ::R12'' 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: 12 <> 1 & 12 <> 2 & 12 <> 3 & 12 <> 4 & 12 <> 5 & 12 <> 9 & 12 <> 11 & InsCode (f :=<0,...,0> b) = 12 by SCMFSA_2:53; hence a := e <> f :=<0,...,0> b by SCMFSA_2:42; thus AddTo(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:43; thus SubFrom(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:44; thus MultBy(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:45; thus Divide(a,e) <> f :=<0,...,0> b & Divide(e,a) <> f :=<0,...,0> b by A1,SCMFSA_2:46; thus a :=(h,e) <> f :=<0,...,0> b by A1,SCMFSA_2:50; thus a :=len h <> f :=<0,...,0> b by A1,SCMFSA_2:52; end; hence f :=<0,...,0> b does_not_destroy a by Def3; end; definition let I be FinPartState of SCM+FSA; let s be State of SCM+FSA; pred I is_closed_on s means :Def7: ::D18 for k being Nat holds IC (Computation (s +* (I +* Start-At insloc 0))).k in dom I; pred I is_halting_on s means :Def8: ::D18' s +* (I +* Start-At insloc 0) is halting; end; theorem Th24: ::TQ6 for I being Macro-Instruction holds I is paraclosed iff for s being State of SCM+FSA holds I is_closed_on s proof let I be Macro-Instruction; hereby assume A1: I is paraclosed; let s be State of SCM+FSA; I +* Start-At insloc 0 c= s +* (I +* Start-At insloc 0) by FUNCT_4:26; then for k being Nat holds IC (Computation (s +* (I +* Start-At insloc 0))).k in dom I by A1,SCMFSA6B:def 2; hence I is_closed_on s by Def7; end; assume A2: for s being State of SCM+FSA holds I is_closed_on s; now let s be State of SCM+FSA; let k be Nat; assume I +* Start-At insloc 0 c= s; then I is_closed_on s & s = s +* (I +* Start-At insloc 0) by A2,AMI_5:10 ; hence IC (Computation s).k in dom I by Def7; end; hence I is paraclosed by SCMFSA6B:def 2; end; theorem ::*TQ6' for I being Macro-Instruction holds I is parahalting iff for s being State of SCM+FSA holds I is_halting_on s proof let I be Macro-Instruction; hereby assume A1: I is parahalting; let s be State of SCM+FSA; A2: I +* Start-At insloc 0 c= s +* (I +* Start-At insloc 0) by FUNCT_4:26; I +* Start-At insloc 0 is halting by A1,SCMFSA6B:def 3; then s +* (I +* Start-At insloc 0) is halting by A2,AMI_1:def 26; hence I is_halting_on s by Def8; end; assume A3: for s being State of SCM+FSA holds I is_halting_on s; now let s be State of SCM+FSA; assume I +* Start-At insloc 0 c= s; then I is_halting_on s & s = s +* (I +* Start-At insloc 0) by A3,AMI_5:10 ; hence s is halting by Def8; end; then I +* Start-At insloc 0 is halting by AMI_1:def 26; hence I is parahalting by SCMFSA6B:def 3; end; theorem Th26: ::TA10 for i being Instruction of SCM+FSA, a being Int-Location, s being State of SCM+FSA holds i does_not_destroy a implies 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; A2: InsCode i <= 11+1 by SCMFSA_2:35; A3: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26; A4: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26; A5: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26; per cases by A2,A3,A4,A5,CQC_THE1:9,NAT_1:26; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:122; hence Exec(i,s).a = s.a by AMI_1:def 8; suppose InsCode i = 1; then consider da,db being Int-Location such that A6: i = da := db by SCMFSA_2:54; da <> a by A1,A6,Def3; hence Exec(i,s).a = s.a by A6,SCMFSA_2:89; suppose InsCode i = 2; then consider da, db being Int-Location such that A7: i = AddTo(da,db) by SCMFSA_2:55; da <> a by A1,A7,Def3; hence Exec(i,s).a = s.a by A7,SCMFSA_2:90; suppose InsCode i = 3; then consider da, db being Int-Location such that A8: i = SubFrom(da, db) by SCMFSA_2:56; da <> a by A1,A8,Def3; hence Exec(i,s).a = s.a by A8,SCMFSA_2:91; suppose InsCode i = 4; then consider da, db being Int-Location such that A9: i = MultBy(da,db) by SCMFSA_2:57; da <> a by A1,A9,Def3; hence Exec(i,s).a = s.a by A9,SCMFSA_2:92; suppose InsCode i = 5; then consider da, db being Int-Location such that A10: i = Divide(da, db) by SCMFSA_2:58; da <> a & db <> a by A1,A10,Def3; hence Exec(i,s).a = s.a by A10,SCMFSA_2:93; suppose InsCode i = 6; then consider loc being Instruction-Location of SCM+FSA such that A11: i = goto loc by SCMFSA_2:59; thus Exec(i,s).a = s.a by A11,SCMFSA_2:95; suppose InsCode i = 7; then consider loc being Instruction-Location of SCM+FSA, da being Int-Location such that A12: i = da=0_goto loc by SCMFSA_2:60; thus Exec(i,s).a = s.a by A12,SCMFSA_2:96; suppose InsCode i = 8; then consider loc being Instruction-Location of SCM+FSA, da being Int-Location such that A13: i = da>0_goto loc by SCMFSA_2:61; thus Exec(i,s).a = s.a by A13,SCMFSA_2:97; suppose InsCode i = 9; then consider db, da being Int-Location, g being FinSeq-Location such that A14: i = da := (g,db) by SCMFSA_2:62; da <> a by A1,A14,Def3; hence Exec(i,s).a = s.a by A14,SCMFSA_2:98; suppose InsCode i = 10; then consider db, da being Int-Location, g being FinSeq-Location such that A15: i = (g,db):=da by SCMFSA_2:63; thus Exec(i,s).a = s.a by A15,SCMFSA_2:99; suppose InsCode i = 11; then consider da being Int-Location, g being FinSeq-Location such that A16: i = da :=len g by SCMFSA_2:64; da <> a by A1,A16,Def3; hence Exec(i,s).a = s.a by A16,SCMFSA_2:100; suppose InsCode i = 12; then consider da being Int-Location, g being FinSeq-Location such that A17: i = g :=<0,...,0> da by SCMFSA_2:65; thus Exec(i,s).a = s.a by A17,SCMFSA_2:101; end; theorem Th27: ::TQ9'' for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location st I does_not_destroy a & I is_closed_on s holds for k being Nat holds (Computation (s +* (I +* Start-At insloc 0))).k.a = s.a proof let s be State of SCM+FSA; let I be Macro-Instruction; let a be Int-Location; assume A1: I does_not_destroy a; assume A2: I is_closed_on s; set s1 = s +* (I +* Start-At insloc 0); A3: I +* Start-At insloc 0 c= s1 by FUNCT_4:26; dom I misses dom Start-At insloc 0 by SF_MASTR:64; then I c= I +* Start-At insloc 0 by FUNCT_4:33; then A4: I c= s1 by A3,XBOOLE_1:1; A5: a in dom s & not a in dom (I +* Start-At insloc 0) by SCMFSA6B:12,SCMFSA_2:66; defpred P[Nat] means (Computation s1).$1.a = s.a; A6: P[0] proof thus (Computation s1).0.a = s1.a by AMI_1:def 19 .= s.a by A5,FUNCT_4:12; end; A7: now let k be Nat; assume A8: P[k]; set l = IC (Computation s1).k; A9: l in dom I by A2,Def7; then s1.l = I.l by A4,GRFUNC_1:8; then s1.l in rng I by A9,FUNCT_1:def 5; then A10: s1.l does_not_destroy a by A1,Def4; thus P[k+1] proof thus (Computation s1).(k + 1).a = (Following (Computation s1).k).a by AMI_1:def 19 .= Exec(CurInstr (Computation s1).k,(Computation s1).k).a by AMI_1:def 18 .= Exec((Computation s1).k.l,(Computation s1).k).a by AMI_1:def 17 .= Exec(s1.l,(Computation s1).k).a by AMI_1:54 .= s.a by A8,A10,Th26; end; end; thus for k being Nat holds P[k] from Ind(A6,A7); end; theorem Th28: ::TQ7 SCM+FSA-Stop does_not_destroy intloc 0 proof now let i be Instruction of SCM+FSA; assume A1: i in rng SCM+FSA-Stop; rng SCM+FSA-Stop = {halt SCM+FSA} by CQC_LANG:5,SCMFSA_4:def 5; then i = halt SCM+FSA by A1,TARSKI:def 1; hence i does_not_destroy intloc 0 by Th11; end; hence thesis by Def4; end; Lm9: SCM+FSA-Stop is parahalting proof now let s be State of SCM+FSA; assume A1: SCM+FSA-Stop +* Start-At insloc 0 c= s; dom SCM+FSA-Stop misses dom Start-At insloc 0 by SF_MASTR:64; then A2: SCM+FSA-Stop c= SCM+FSA-Stop +* Start-At insloc 0 by FUNCT_4:33; then A3: dom SCM+FSA-Stop c= dom (SCM+FSA-Stop +* Start-At insloc 0) by GRFUNC_1:8; dom SCM+FSA-Stop = {insloc 0} by CQC_LANG:5,SCMFSA_4:def 5; then A4: insloc 0 in dom SCM+FSA-Stop by TARSKI:def 1; A5: IC SCM+FSA in dom (SCM+FSA-Stop +* Start-At insloc 0) by SF_MASTR:65; CurInstr (Computation s).0 = CurInstr s by AMI_1:def 19 .= s.IC s by AMI_1:def 17 .= s.(s.IC SCM+FSA) by AMI_1:def 15 .= s.((SCM+FSA-Stop +* Start-At insloc 0).IC SCM+FSA) by A1,A5,GRFUNC_1:8 .= s.insloc 0 by SF_MASTR:66 .= (SCM+FSA-Stop +* Start-At insloc 0).insloc 0 by A1,A3,A4,GRFUNC_1:8 .= SCM+FSA-Stop.insloc 0 by A2,A4,GRFUNC_1:8 .= halt SCM+FSA by CQC_LANG:6,SCMFSA_4:def 5; hence s is halting by AMI_1:def 20; end; then SCM+FSA-Stop +* Start-At insloc 0 is halting by AMI_1:def 26; hence thesis by SCMFSA6B:def 3; end; definition cluster parahalting good Macro-Instruction; existence proof take SCM+FSA-Stop; thus thesis by Def5,Lm9,Th28; end; end; definition cluster SCM+FSA-Stop -> parahalting good; coherence by Def5,Lm9,Th28; end; definition cluster paraclosed good -> keeping_0 Macro-Instruction; correctness proof let I be Macro-Instruction; assume A1: I is paraclosed good; then A2: I does_not_destroy intloc 0 by Def5; now let s be State of SCM+FSA; assume A3: I +* Start-At insloc 0 c= s; let k be Nat; A4: I is_closed_on s by A1,Th24; s +* (I +* Start-At insloc 0) = s by A3,AMI_5:10; hence (Computation s).k.intloc 0 = s.intloc 0 by A2,A4,Th27; end; hence I is keeping_0 by SCMFSA6B:def 4; end; end; theorem Th29: ::TS3 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; now let x be set; assume A1: x in rng aSeq(a,k); per cases; suppose A2: k > 0 & k = 0 + 1; then consider k1 being Nat such that A3: k1 + 1 = k and A4: aSeq(a,k) = <* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0)) by SCMFSA_7:def 3; k1 = 0 by A2,A3,XCMPLX_1:2; then aSeq(a,k) = <* a := intloc 0 *> ^ {} by A4,FINSEQ_2:72 .= <* a := intloc 0 *> by FINSEQ_1:47; then rng aSeq(a,k) = {a := intloc 0} by FINSEQ_1:55; 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:14; suppose A5: k > 0 & k <> 1; then consider k1 being Nat such that A6: k1 + 1 = k and A7: aSeq(a,k) = <* a := intloc 0 *> ^ (k1 |-> AddTo(a,intloc 0)) by SCMFSA_7:def 3; k1 <> 0 by A5,A6; then A8: k1 in Seg k1 by FINSEQ_1:5; rng aSeq(a,k) = rng <* a := intloc 0 *> \/ rng (k1 |-> AddTo(a,intloc 0)) by A7,FINSEQ_1:44 .= {a := intloc 0} \/ rng (k1 |-> AddTo(a,intloc 0)) by FINSEQ_1:55 .= {a := intloc 0} \/ rng (Seg k1 --> AddTo(a,intloc 0)) by FINSEQ_2:def 2 .= {a := intloc 0} \/ {AddTo(a,intloc 0)} by A8,FUNCOP_1:14; then x in {a := intloc 0} or x in {AddTo(a,intloc 0)} by A1,XBOOLE_0:def 2 ; 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:14; suppose A9: not k > 0; then consider k1 being Nat such that A10: k1 + k = 1 and A11: aSeq(a,k) = <* a := intloc 0 *> ^ (k1 |-> SubFrom(a,intloc 0)) by SCMFSA_7:def 3; k1 <> 0 by A9,A10; then A12: k1 in Seg k1 by FINSEQ_1:5; rng aSeq(a,k) = rng <* a := intloc 0 *> \/ rng (k1 |-> SubFrom(a,intloc 0)) by A11,FINSEQ_1:44 .= {a := intloc 0} \/ rng (k1 |-> SubFrom(a,intloc 0)) by FINSEQ_1:55 .= {a := intloc 0} \/ rng (Seg k1 --> SubFrom(a,intloc 0)) by FINSEQ_2:def 2 .= {a := intloc 0} \/ {SubFrom(a,intloc 0)} by A12,FUNCOP_1:14; then x in {a := intloc 0} or x in {SubFrom(a,intloc 0)} by A1,XBOOLE_0:def 2; 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:14; end; hence rng aSeq(a,k) c= {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by TARSKI:def 3; end; theorem Th30: ::TS1 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; now let x be set; assume A1: x in rng (a := k); a := k = Load (aSeq(a,k) ^ <* halt SCM+FSA *>) by SCMFSA_7:33; then rng (a := k) = rng (aSeq(a,k) ^ <* halt SCM+FSA *>) by Th2 .= rng aSeq(a,k) \/ rng <* halt SCM+FSA *> by FINSEQ_1:44 .= rng aSeq(a,k) \/ {halt SCM+FSA} by FINSEQ_1:55; then A2: x in rng aSeq(a,k) or x in {halt SCM+FSA} by A1,XBOOLE_0:def 2; rng aSeq(a,k) c= {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by Th29; then x = a := intloc 0 or x = AddTo(a,intloc 0) or x = SubFrom(a,intloc 0) or x = halt SCM+FSA by A2,ENUMSET1:13,TARSKI:def 1; hence x in {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by ENUMSET1:19; end; hence rng (a := k) c= {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by TARSKI:def 3; end; definition let a be read-write Int-Location, k be Integer; cluster a := k -> good; correctness proof now let i be Instruction of SCM+FSA; assume A1: i in rng (a := k); A2: rng (a := k) c= {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by Th30; per cases by A1,A2,ENUMSET1:18; suppose i = halt SCM+FSA; hence i does_not_destroy intloc 0 by Th11; suppose i = a := intloc 0; hence i does_not_destroy intloc 0 by Th12; suppose i = AddTo(a,intloc 0); hence i does_not_destroy intloc 0 by Th13; suppose i = SubFrom(a,intloc 0); hence i does_not_destroy intloc 0 by Th14; end; then a := k does_not_destroy intloc 0 by Def4; hence thesis by Def5; end; end; definition let a be read-write Int-Location, k be Integer; cluster a := k -> keeping_0; correctness; end;