### The Mizar article:

### The Basic Properties of \SCM over Ring

**by****Artur Kornilowicz**

- Received November 29, 1998
Copyright (c) 1998 Association of Mizar Users

- MML identifier: SCMRING2
- [ MML identifier index ]

environ vocabulary GR_CY_1, SCMFSA7B, FUNCSDOM, AMI_3, AMI_1, AMI_2, FUNCT_1, CAT_1, BOOLE, FINSEQ_1, FUNCT_2, CARD_3, ARYTM_1, RLVECT_1, CQC_LANG, SCMRING1, MCART_1, FUNCT_4, RELAT_1; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, GR_CY_1, STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, MCART_1, NUMBERS, XREAL_0, CARD_3, NAT_1, FINSEQ_1, CQC_LANG, FUNCT_4, AMI_1, AMI_2, AMI_3, SCMRING1; constructors AMI_3, CAT_2, DOMAIN_1, FINSEQ_4, NAT_1, REALSET1, SCMRING1, MEMBERED; clusters AMI_1, CQC_LANG, SCMRING1, STRUCT_0, RELSET_1, AMI_5, AMI_3, FINSEQ_5, XBOOLE_0, FRAENKEL, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions TARSKI, STRUCT_0, AMI_1; theorems AMI_1, AMI_2, AMI_3, AMI_5, AXIOMS, CARD_3, CQC_LANG, ENUMSET1, FUNCT_2, FUNCT_4, GR_CY_1, MCART_1, NAT_1, REAL_1, SCMRING1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1; begin :: { \bf SCM } over ring reserve i for Nat, I for Element of Segm 8, S for non empty 1-sorted, t for Element of S, x for set; definition let R be good Ring; func SCM R -> strict AMI-Struct over { the carrier of R } means :Def1: the carrier of it = NAT & the Instruction-Counter of it = 0 & the Instruction-Locations of it = SCM-Instr-Loc & the Instruction-Codes of it = Segm 8 & the Instructions of it = SCM-Instr R & the Object-Kind of it = SCM-OK R & the Execution of it = SCM-Exec R; existence proof take AMI-Struct (#NAT,0,SCM-Instr-Loc,Segm 8,SCM-Instr R,SCM-OK R,SCM-Exec R #); thus thesis; end; uniqueness; end; definition let R be good Ring; cluster SCM R -> non empty non void; coherence proof thus the carrier of SCM R is non empty by Def1; thus the Instruction-Locations of SCM R is non empty by Def1; end; end; definition let R be good Ring, s be State of SCM R, a be Element of SCM-Data-Loc; redefine func s.a -> Element of R; coherence proof reconsider S = s as SCM-State of R by Def1; S.a in the carrier of R; hence thesis; end; end; definition let R be good Ring; mode Data-Location of R -> Object of SCM R means :Def2: it in (the carrier of SCM R) \ (SCM-Instr-Loc \/ {0}); existence proof A1: now assume 1 in { 2*k where k is Nat: k > 0 }; then consider k being Nat such that A2: 1 = 2*k & k > 0; defpred P[Nat] means $1 > 0 implies 2*$1 > 1; A3: P[0]; A4: for m being Nat st P[m] holds P[m+1] proof let m be Nat; assume A5: P[m]; assume m+1 > 0; per cases; suppose m = 0; hence 2*(m+1) > 1; suppose m <> 0; then 2*m+2*1 > 1+2*1 by A5,NAT_1:19,REAL_1:53; then 2*m+2*1 > 1 by AXIOMS:22; hence 2*(m+1) > 1 by XCMPLX_1:8; end; for m being Nat holds P[m] from Ind(A3,A4); hence contradiction by A2; end; reconsider a = 1 as Object of SCM R by Def1; take a; not a in {0} by TARSKI:def 1; then not a in { 2*k where k is Nat: k > 0 } \/ {0} by A1,XBOOLE_0:def 2; hence thesis by AMI_2:def 3,XBOOLE_0:def 4; end; end; reserve R for good Ring, r for Element of R, a, b, c, d1, d2 for Data-Location of R, i1 for Instruction-Location of SCM R; theorem Th1: x is Data-Location of R iff x in SCM-Data-Loc proof A1:the carrier of SCM R = {IC SCM} \/ SCM-Data-Loc \/ SCM-Instr-Loc by Def1,AMI_3:def 1,AMI_5:23; A2:the carrier of SCM R = NAT by Def1; hereby assume x is Data-Location of R; then x in (the carrier of SCM R) \ (SCM-Instr-Loc \/ {0}) by Def2; then A3: x in the carrier of SCM R & not x in SCM-Instr-Loc \/ {0} by XBOOLE_0: def 4 ; then A4: not x in SCM-Instr-Loc & not x in {0} by XBOOLE_0:def 2; then x in {IC SCM} \/ SCM-Data-Loc by A1,A3,XBOOLE_0:def 2; hence x in SCM-Data-Loc by A4,AMI_3:4,XBOOLE_0:def 2; end; assume A5: x in SCM-Data-Loc; then x is Data-Location by AMI_5:16; then x <> 0 by AMI_3:4,AMI_5:20; then not x in SCM-Instr-Loc & not x in {0} by A5,AMI_5:33,TARSKI:def 1,XBOOLE_0:3; then not x in SCM-Instr-Loc \/ {0} by XBOOLE_0:def 2; then x in (the carrier of SCM R) \ (SCM-Instr-Loc \/ {0}) by A2,A5,XBOOLE_0: def 4 ; hence thesis by A2,A5,Def2; end; definition let R be good Ring, s be State of SCM R, a be Data-Location of R; redefine func s.a -> Element of R; coherence proof reconsider A = a as Element of SCM-Data-Loc by Th1; s.A in the carrier of R; hence thesis; end; end; theorem Th2: [0,{}] in SCM-Instr S proof A1: SCM-Instr S = { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*i,r*>] where i is Element of SCM-Data-Loc, r is Element of S: not contradiction } by SCMRING1:def 1; [0,{}] in {[0,{}]} by TARSKI:def 1; then [0,{}] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } by XBOOLE_0:def 2; then [0,{}] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } by XBOOLE_0:def 2; then [0,{}] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } by XBOOLE_0:def 2; hence thesis by A1,XBOOLE_0:def 2; end; theorem Th3: [0,{}] is Instruction of SCM R proof [0,{}] in SCM-Instr R & SCM-Instr R = the Instructions of SCM R by Def1,Th2; hence thesis ; end; theorem Th4: x in {1,2,3,4} implies [x,<*d1,d2*>] in SCM-Instr S proof assume A1: x in {1,2,3,4}; then x=1 or x=2 or x=3 or x=4 by ENUMSET1:18; then reconsider x as Element of Segm 8 by GR_CY_1:10; A2: SCM-Instr S = { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*i,r*>] where i is Element of SCM-Data-Loc, r is Element of S: not contradiction } by SCMRING1:def 1; reconsider D1 = d1, D2 = d2 as Element of SCM-Data-Loc by Th1; [x,<*D1,D2*>] in { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } by A1; then [x,<*D1,D2*>] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } by XBOOLE_0:def 2; then [x,<*D1,D2*>] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } by XBOOLE_0:def 2; then [x,<*D1,D2*>] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } by XBOOLE_0:def 2; hence thesis by A2,XBOOLE_0:def 2; end; theorem Th5: [5,<*d1,t*>] in SCM-Instr S proof A1: SCM-Instr S = { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of S: not contradiction } by SCMRING1:def 1; reconsider D1 = d1 as Element of SCM-Data-Loc by Th1; [5,<*D1,t*>] in { [5,<*i,a*>] where i is Element of SCM-Data-Loc, a is Element of S : not contradiction }; hence thesis by A1,XBOOLE_0:def 2; end; theorem Th6: [6,<*i1*>] in SCM-Instr S proof A1: SCM-Instr S = { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*i,r*>] where i is Element of SCM-Data-Loc, r is Element of S: not contradiction } by SCMRING1:def 1; reconsider I1 = i1 as Element of SCM-Instr-Loc by Def1; [6,<*I1*>] in {[6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction}; then [6,<*I1*>] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ {[6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction} by XBOOLE_0:def 2; then [6,<*I1*>] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ {[6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction} \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } by XBOOLE_0:def 2; hence thesis by A1,XBOOLE_0:def 2; end; theorem Th7: [7,<*i1,d1*>] in SCM-Instr S proof A1: SCM-Instr S = { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*i,r*>] where i is Element of SCM-Data-Loc, r is Element of S: not contradiction } by SCMRING1:def 1; reconsider I1 = i1 as Element of SCM-Instr-Loc by Def1; reconsider D1 = d1 as Element of SCM-Data-Loc by Th1; [7,<*I1,D1*>] in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction }; then [7,<*I1,D1*>] in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ {[6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction} \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } by XBOOLE_0:def 2; hence thesis by A1,XBOOLE_0:def 2; end; definition let R be good Ring, a, b be Data-Location of R; func a := b -> Instruction of SCM R equals :Def3: [ 1, <*a, b*>]; coherence proof 1 in { 1,2,3,4} by ENUMSET1:19; then [ 1, <*a,b*>] in SCM-Instr R by Th4; then [ 1, <*a,b*>] in the Instructions of SCM R by Def1; hence thesis ; end; func AddTo(a,b) -> Instruction of SCM R equals :Def4: [ 2, <*a, b*>]; coherence proof 2 in { 1,2,3,4} by ENUMSET1:19; then [ 2, <*a,b*>] in SCM-Instr R by Th4; then [ 2, <*a,b*>] in the Instructions of SCM R by Def1; hence thesis ; end; func SubFrom(a,b) -> Instruction of SCM R equals :Def5: [ 3, <*a, b*>]; coherence proof 3 in { 1,2,3,4} by ENUMSET1:19; then [ 3, <*a,b*>] in SCM-Instr R by Th4; then [ 3, <*a,b*>] in the Instructions of SCM R by Def1; hence thesis ; end; func MultBy(a,b) -> Instruction of SCM R equals :Def6: [ 4, <*a, b*>]; coherence proof 4 in { 1,2,3,4} by ENUMSET1:19; then [ 4, <*a,b*>] in SCM-Instr R by Th4; then [ 4, <*a,b*>] in the Instructions of SCM R by Def1; hence thesis ; end; end; definition let R be good Ring, a be Data-Location of R, r be Element of R; func a := r -> Instruction of SCM R equals :Def7: [ 5, <*a,r*>]; coherence proof [ 5, <*a,r*>] in SCM-Instr R by Th5; then [ 5, <*a,r*>] in the Instructions of SCM R by Def1; hence thesis ; end; end; definition let R be good Ring, l be Instruction-Location of SCM R; func goto l -> Instruction of SCM R equals :Def8: [ 6, <*l*>]; coherence proof [ 6, <*l*>] in SCM-Instr R by Th6; then [ 6, <*l*>] in the Instructions of SCM R by Def1; hence thesis ; end; end; definition let R be good Ring, l be Instruction-Location of SCM R, a be Data-Location of R; func a=0_goto l -> Instruction of SCM R equals :Def9: [ 7, <*l,a*>]; coherence proof [ 7, <*l,a*>] in SCM-Instr R by Th7; then [ 7, <*l,a*>] in the Instructions of SCM R by Def1; hence thesis ; end; end; theorem Th8: for I being set holds I is Instruction of SCM R iff I = [0,{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or (ex i1 st I = goto i1) or (ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r proof let J be set; A1: the Instructions of SCM R = SCM-Instr R by Def1; A2: SCM-Instr R = { [0,{}] } \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by SCMRING1:def 1; thus J is Instruction of SCM R implies J = [0,{}] or (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or ex a,r st J = a:=r proof assume J is Instruction of SCM R; then J in { [0,{}] } \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } or J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by A1,A2,XBOOLE_0:def 2; then J in { [0,{}] } \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } or J in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } or J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by XBOOLE_0:def 2; then A3: J in { [0,{}] } \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } or J in { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } or J in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } or J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by XBOOLE_0:def 2; per cases by A3,XBOOLE_0:def 2; suppose J in { [0,{}] }; hence thesis by TARSKI:def 1; suppose J in { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction }; then consider i being Element of SCM-Instr-Loc such that A4: J = [6,<*i*>] and not contradiction; reconsider i as Instruction-Location of SCM R by Def1; J = goto i by A4,Def8; hence thesis; suppose J in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction }; then consider i being Element of SCM-Instr-Loc, a being Element of SCM-Data-Loc such that A5: J = [7,<*i,a*>] and not contradiction; reconsider I = i as Instruction-Location of SCM R by Def1; reconsider A = a as Data-Location of R by Th1; J = A=0_goto I by A5,Def9; hence thesis; suppose J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction }; then consider a being Element of SCM-Data-Loc, r being Element of R such that A6: J = [5,<*a,r*>] and not contradiction; reconsider A = a as Data-Location of R by Th1; J = A:=r by A6,Def7; hence thesis; suppose J in { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } }; then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that A7: J = [I,<*a,b*>] & I in { 1,2,3,4 }; reconsider A = a, B = b as Data-Location of R by Th1; I = 1 or I = 2 or I = 3 or I = 4 by A7,ENUMSET1:18; then J = A:=B or J = AddTo(A,B) or J = SubFrom(A,B) or J = MultBy(A,B) by A7,Def3,Def4,Def5,Def6; hence thesis; end; [0,{}] in SCM-Instr R by Th2; hence thesis by A1; end; reserve s for State of SCM R; definition let R; cluster SCM R -> IC-Ins-separated; coherence proof thus ObjectKind IC SCM R = (the Object-Kind of SCM R).IC SCM R by AMI_1:def 6 .= (SCM-OK R).IC SCM R by Def1 .= (SCM-OK R).the Instruction-Counter of SCM R by AMI_1:def 5 .= (SCM-OK R).0 by Def1 .= SCM-Instr-Loc by SCMRING1:def 3 .= the Instruction-Locations of SCM R by Def1; end; end; theorem Th9: IC SCM R = 0 proof thus IC SCM R = the Instruction-Counter of SCM R by AMI_1:def 5 .= 0 by Def1; end; theorem Th10: for S being SCM-State of R st S = s holds IC s = IC S proof let S be SCM-State of R such that A1: S = s; thus IC s = s.IC SCM R by AMI_1:def 15 .= S.0 by A1,Th9 .= IC S by SCMRING1:def 4; end; definition let R be good Ring, i1 be Instruction-Location of SCM R; func Next i1 -> Instruction-Location of SCM R means :Def10: ex mj being Element of SCM-Instr-Loc st mj = i1 & it = Next mj; existence proof reconsider i1 as Element of SCM-Instr-Loc by Def1; Next i1 is Instruction-Location of SCM R by Def1; hence thesis; end; uniqueness; end; theorem Th11: for i1 being Instruction-Location of SCM R, mj being Element of SCM-Instr-Loc st mj = i1 holds Next mj = Next i1 proof let i1 be Instruction-Location of SCM R, mj be Element of SCM-Instr-Loc; ex mj being Element of SCM-Instr-Loc st mj = i1 & Next i1= Next mj by Def10; hence thesis; end; theorem Th12: for I being Instruction of SCM R for i being Element of SCM-Instr R st i = I for S being SCM-State of R st S = s holds Exec(I,s) = SCM-Exec-Res(i,S) proof let I be Instruction of SCM R, i be Element of SCM-Instr R such that A1: i = I; let S be SCM-State of R; assume A2: S = s; thus Exec(I,s) = (((the Execution of SCM R) qua Function of the Instructions of SCM R, Funcs(product the Object-Kind of SCM R, product the Object-Kind of SCM R)).I).s by AMI_1:def 7 .= ((SCM-Exec R).i qua Element of Funcs(product SCM-OK R, product SCM-OK R)).S by A1,A2,Def1 .= SCM-Exec-Res(i,S) by SCMRING1:def 15; end; begin :: Users guide theorem Th13: Exec(a := b, s).IC SCM R = Next IC s & Exec(a := b, s).a = s.b & for c st c <> a holds Exec(a := b, s).c = s.c proof reconsider I = a := b as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; set S1 = SCM-Chg(S, I address_1,S.(I address_2)); reconsider i = 1 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*a, b*>] by Def3; A2: IC s = IC S by Th10; A3: a is Element of SCM-Data-Loc & b is Element of SCM-Data-Loc by Th1; A4: Exec(a := b, s) = SCM-Exec-Res(I,S) by Th12 .= (SCM-Chg(S1, Next IC S)) by A1,A3,SCMRING1:def 14; A5: I address_1 = a & I address_2 = b by A1,A3,SCMRING1:17; thus Exec(a := b, s).IC SCM R = Exec(a := b, s).0 by Th9 .= Next IC S by A4,SCMRING1:10 .= Next IC s by A2,Th11; thus Exec(a := b, s).a = S1.a by A3,A4,SCMRING1:11 .= s.b by A5,SCMRING1:14; let c; assume A6: c <> a; A7: c is Element of SCM-Data-Loc by Th1; hence Exec(a := b, s).c = S1.c by A4,SCMRING1:11 .= s.c by A5,A6,A7,SCMRING1:15; end; theorem Th14: Exec(AddTo(a,b), s).IC SCM R = Next IC s & Exec(AddTo(a,b), s).a = s.a + s.b & for c st c <> a holds Exec(AddTo(a,b), s).c = s.c proof reconsider I = AddTo(a,b) as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; set S1 = SCM-Chg(S, I address_1,S.(I address_1)+S.(I address_2)); reconsider i = 2 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*a, b*>] by Def4; A2: IC s = IC S by Th10; A3: a is Element of SCM-Data-Loc & b is Element of SCM-Data-Loc by Th1; A4: Exec(AddTo(a,b), s) = SCM-Exec-Res(I,S) by Th12 .= (SCM-Chg(S1, Next IC S)) by A1,A3,SCMRING1:def 14; A5: I address_1 = a & I address_2 = b by A1,A3,SCMRING1:17; thus Exec(AddTo(a,b), s).IC SCM R = Exec(AddTo(a,b), s).0 by Th9 .= Next IC S by A4,SCMRING1:10 .= Next IC s by A2,Th11; thus Exec(AddTo(a,b), s).a = S1.a by A3,A4,SCMRING1:11 .= s.a + s.b by A5,SCMRING1:14; let c; assume A6: c <> a; A7: c is Element of SCM-Data-Loc by Th1; hence Exec(AddTo(a,b), s).c = S1.c by A4,SCMRING1:11 .= s.c by A5,A6,A7,SCMRING1:15; end; theorem Th15: Exec(SubFrom(a,b), s).IC SCM R = Next IC s & Exec(SubFrom(a,b), s).a = s.a - s.b & for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c proof reconsider I = SubFrom(a,b) as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; set S1 = SCM-Chg(S, I address_1,S.(I address_1)-S.(I address_2)); reconsider i = 3 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*a, b*>] by Def5; A2: IC s = IC S by Th10; A3: a is Element of SCM-Data-Loc & b is Element of SCM-Data-Loc by Th1; A4: Exec(SubFrom(a,b), s) = SCM-Exec-Res(I,S) by Th12 .= (SCM-Chg(S1, Next IC S)) by A1,A3,SCMRING1:def 14; A5: I address_1 = a & I address_2 = b by A1,A3,SCMRING1:17; thus Exec(SubFrom(a,b), s).IC SCM R = Exec(SubFrom(a,b), s).0 by Th9 .= Next IC S by A4,SCMRING1:10 .= Next IC s by A2,Th11; thus Exec(SubFrom(a,b), s).a = S1.a by A3,A4,SCMRING1:11 .= s.a - s.b by A5,SCMRING1:14; let c; assume A6: c <> a; A7: c is Element of SCM-Data-Loc by Th1; hence Exec(SubFrom(a,b), s).c = S1.c by A4,SCMRING1:11 .= s.c by A5,A6,A7,SCMRING1:15; end; theorem Th16: Exec(MultBy(a,b), s).IC SCM R = Next IC s & Exec(MultBy(a,b), s).a = s.a * s.b & for c st c <> a holds Exec(MultBy(a,b), s).c = s.c proof reconsider I = MultBy(a,b) as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; set S1 = SCM-Chg(S, I address_1,S.(I address_1)*S.(I address_2)); reconsider i = 4 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*a, b*>] by Def6; A2: IC s = IC S by Th10; A3: a is Element of SCM-Data-Loc & b is Element of SCM-Data-Loc by Th1; A4: Exec(MultBy(a,b), s) = SCM-Exec-Res(I,S) by Th12 .= (SCM-Chg(S1, Next IC S)) by A1,A3,SCMRING1:def 14; A5: I address_1 = a & I address_2 = b by A1,A3,SCMRING1:17; thus Exec(MultBy(a,b), s).IC SCM R = Exec(MultBy(a,b), s).0 by Th9 .= Next IC S by A4,SCMRING1:10 .= Next IC s by A2,Th11; thus Exec(MultBy(a,b), s).a = S1.a by A3,A4,SCMRING1:11 .= s.a * s.b by A5,SCMRING1:14; let c; assume A6: c <> a; A7: c is Element of SCM-Data-Loc by Th1; hence Exec(MultBy(a,b), s).c = S1.c by A4,SCMRING1:11 .= s.c by A5,A6,A7,SCMRING1:15; end; theorem Exec(goto i1, s).IC SCM R = i1 & Exec(goto i1, s).c = s.c proof reconsider I = goto i1 as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; reconsider i = 6 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*i1*>] by Def8; A2: i1 is Element of SCM-Instr-Loc by Def1; A3: Exec(goto i1, s) = SCM-Exec-Res(I,S) by Th12 .= (SCM-Chg(S,I jump_address)) by A1,A2,SCMRING1:def 14; A4:I jump_address = i1 by A1,A2,SCMRING1:18; thus Exec(goto i1, s).IC SCM R = Exec(goto i1, s).0 by Th9 .= i1 by A3,A4,SCMRING1:10; c is Element of SCM-Data-Loc by Th1; hence Exec(goto i1, s).c = s.c by A3,SCMRING1:11; end; theorem Th18: (s.a = 0.R implies Exec(a =0_goto i1, s).IC SCM R = i1) & (s.a <> 0.R implies Exec(a =0_goto i1, s).IC SCM R = Next IC s) & Exec(a =0_goto i1, s).c = s.c proof reconsider I = a =0_goto i1 as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; reconsider i = 7 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*i1,a*>] by Def9; A2: IC s = IC S by Th10; A3: a is Element of SCM-Data-Loc & i1 is Element of SCM-Instr-Loc by Def1,Th1; A4: Exec(a =0_goto i1, s) = SCM-Exec-Res(I,S) by Th12 .= SCM-Chg(S,IFEQ(S.(I cond_address),0.R,I cjump_address,Next IC S)) by A1,A3,SCMRING1:def 14; thus s.a = 0.R implies Exec(a =0_goto i1, s).IC SCM R = i1 proof assume s.a = 0.R; then A5: S.(I cond_address)=0.R by A1,A3,SCMRING1:19; thus Exec(a =0_goto i1, s).IC SCM R = Exec(a =0_goto i1, s).0 by Th9 .= IFEQ(S.(I cond_address),0.R,I cjump_address,Next IC S) by A4,SCMRING1:10 .= I cjump_address by A5,CQC_LANG:def 1 .= i1 by A1,A3,SCMRING1:19; end; thus s.a <> 0.R implies Exec(a =0_goto i1, s).IC SCM R = Next IC s proof assume s.a <> 0.R; then A6: S.(I cond_address) <> 0.R by A1,A3,SCMRING1:19; thus Exec(a =0_goto i1, s).IC SCM R = Exec(a =0_goto i1, s).0 by Th9 .= IFEQ(S.(I cond_address),0.R,I cjump_address,Next IC S) by A4,SCMRING1:10 .= Next IC S by A6,CQC_LANG:def 1 .= Next IC s by A2,Th11; end; c is Element of SCM-Data-Loc by Th1; hence Exec(a =0_goto i1, s).c = s.c by A4,SCMRING1:11; end; theorem Th19: Exec(a := r, s).IC SCM R = Next IC s & Exec(a := r, s).a = r & for c st c <> a holds Exec(a := r, s).c = s.c proof reconsider I = a := r as Element of SCM-Instr R by Def1; reconsider S = s as SCM-State of R by Def1; set S1 = SCM-Chg(S, I const_address, I const_value); reconsider i = 5 as Element of Segm 8 by GR_CY_1:10; A1: I = [ i, <*a, r*>] by Def7; A2: IC s = IC S by Th10; A3: a is Element of SCM-Data-Loc by Th1; A4: Exec(a := r, s) = SCM-Exec-Res(I,S) by Th12 .= (SCM-Chg(S1, Next IC S)) by A1,A3,SCMRING1:def 14; A5: I const_address = a & I const_value = r by A1,A3,SCMRING1:20; thus Exec(a := r, s).IC SCM R = Exec(a := r, s).0 by Th9 .= Next IC S by A4,SCMRING1:10 .= Next IC s by A2,Th11; thus Exec(a := r, s).a = S1.a by A3,A4,SCMRING1:11 .= r by A5,SCMRING1:14; let c; assume A6: c <> a; A7:c is Element of SCM-Data-Loc by Th1; hence Exec(a := r, s).c = S1.c by A4,SCMRING1:11 .= s.c by A5,A6,A7,SCMRING1:15; end; begin :: Halt instruction theorem Th20: for I being Instruction of SCM R st ex s st Exec(I,s).IC SCM R = Next IC s holds I is non halting proof let I be Instruction of SCM R; given s such that A1: Exec(I, s).IC SCM R = Next IC s; assume A2: I is halting; reconsider t = s as SCM-State of R by Def1; A3: IC t = IC s by Th10; A4: IC t = t.0 by SCMRING1:def 4; A5: Exec(I,s).IC SCM R = s.IC SCM R by A2,AMI_1:def 8 .= IC s by AMI_1:def 15 .= t.0 by A3,SCMRING1:def 4; reconsider w = t.0 as Instruction-Location of SCM R by A4,Def1; consider mj being Element of SCM-Instr-Loc such that A6: mj = w & Next w = Next mj by Def10; A7: Exec(I,s).IC SCM R = Next w by A1,A3,SCMRING1:def 4; Next w = mj + 2 by A6,AMI_2:def 15; hence contradiction by A5,A6,A7,XCMPLX_1:3; end; theorem Th21: for I being Instruction of SCM R st I = [0,{}] holds I is halting proof let I be Instruction of SCM R such that A1: I = [0,{}]; let s be State of SCM R; reconsider L = I as Element of SCM-Instr R by A1,Th2; I`2 = {} by A1,MCART_1:7; then A2:not (ex mk, ml being Element of SCM-Data-Loc st I = [ 1, <*mk, ml*>]) & not (ex mk, ml being Element of SCM-Data-Loc st I = [ 2, <*mk, ml*>]) & not (ex mk, ml being Element of SCM-Data-Loc st I = [ 3, <*mk, ml*>]) & not (ex mk, ml being Element of SCM-Data-Loc st I = [ 4, <*mk, ml*>]) & not (ex mk being Element of SCM-Instr-Loc st I = [ 6, <*mk*>]) & not (ex mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc st I = [ 7, <*mk,ml*>]) & not (ex mk being Element of SCM-Data-Loc, r being Element of R st I = [ 5, <*mk,r*>]) by MCART_1:7; reconsider t = s as SCM-State of R by Def1; thus Exec(I,s) = SCM-Exec-Res(L,t) by Th12 .= s by A2,SCMRING1:def 14; end; Lm1: a := b is non halting proof consider s; Exec(a := b,s).IC SCM R = Next IC s by Th13; hence thesis by Th20; end; Lm2: AddTo(a,b) is non halting proof consider s; Exec(AddTo(a,b),s).IC SCM R = Next IC s by Th14; hence thesis by Th20; end; Lm3: SubFrom(a,b) is non halting proof consider s; Exec(SubFrom(a,b),s).IC SCM R = Next IC s by Th15; hence thesis by Th20; end; Lm4: MultBy(a,b) is non halting proof consider s; Exec(MultBy(a,b),s).IC SCM R = Next IC s by Th16; hence thesis by Th20; end; Lm5: goto i1 is non halting proof assume A1: goto i1 is halting; reconsider V = goto i1 as Element of SCM-Instr R by Def1; reconsider i5 = i1 as Element of SCM-Instr-Loc by Def1; A2: goto i1 = [ 6, <*i1*>] by Def8; consider s being SCM-State of R; set t = s +* (0 .--> Next i1); set f = the Object-Kind of SCM R; A3: f = SCM-OK R by Def1; A4: dom(0 .--> Next i1) = {0} by CQC_LANG:5; then 0 in dom (0 .--> Next i1) by TARSKI:def 1; then A5: t.0 = (0 .--> Next i1).0 by FUNCT_4:14 .= Next i1 by CQC_LANG:6 .= Next i5 by Th11; then A6: t.0 = i5 + 2 by AMI_2:def 15; A7: {0} c= NAT by ZFMISC_1:37; A8: dom s = dom (SCM-OK R) by CARD_3:18; A9: dom t = dom s \/ dom (0 .--> Next i1) by FUNCT_4:def 1 .= NAT \/ dom (0 .--> Next i1) by A8,FUNCT_2:def 1 .= NAT \/ {0} by CQC_LANG:5 .= NAT by A7,XBOOLE_1:12; A10: dom f = NAT by A3,FUNCT_2:def 1; for x being set st x in dom f holds t.x in f.x proof let x be set such that A11: x in dom f; per cases; suppose A12: x = 0; then f.x = SCM-Instr-Loc by A3,SCMRING1:2; hence t.x in f.x by A5,A12; suppose x <> 0; then not x in dom (0 .--> Next i1) by A4,TARSKI:def 1; then t.x = s.x by FUNCT_4:12; hence t.x in f.x by A3,A11,CARD_3:18; end; then reconsider t as State of SCM R by A9,A10,CARD_3:18; reconsider w = t as SCM-State of R by Def1; dom(0 .--> i1) = {0} by CQC_LANG:5; then 0 in dom (0 .--> i1) by TARSKI:def 1; then A13: (w +* (0 .--> i1)).0 = (0 .--> i1).0 by FUNCT_4:14 .= i1 by CQC_LANG:6; A14: 6 is Element of Segm 8 by GR_CY_1:10; A15: the Instruction-Locations of SCM R = SCM-Instr-Loc by Def1; w +* (0 .--> i1) = SCM-Chg(w,i5) by SCMRING1:def 5 .= SCM-Chg(w,V jump_address) by A2,A14,SCMRING1:18 .= SCM-Exec-Res(V,w) by A2,A15,SCMRING1:def 14 .= Exec(goto i1,t) by Th12 .= t by A1,AMI_1:def 8; hence contradiction by A6,A13,XCMPLX_1:3; end; Lm6: a =0_goto i1 is non halting proof reconsider V = a =0_goto i1 as Element of SCM-Instr R by Def1; reconsider i5 = i1 as Element of SCM-Instr-Loc by Def1; A1: a =0_goto i1 = [ 7, <*i1,a*>] by Def9; consider s being SCM-State of R; set t = s +* (0 .--> Next i1); set f = the Object-Kind of SCM R; A2: f = SCM-OK R by Def1; A3: dom(0 .--> Next i1) = {0} by CQC_LANG:5; then 0 in dom (0 .--> Next i1) by TARSKI:def 1; then A4: t.0 = (0 .--> Next i1).0 by FUNCT_4:14 .= Next i1 by CQC_LANG:6 .= Next i5 by Th11; then A5: t.0 = i5 + 2 by AMI_2:def 15; A6: {0} c= NAT by ZFMISC_1:37; A7: dom s = dom (SCM-OK R) by CARD_3:18; A8: dom t = dom s \/ dom (0 .--> Next i1) by FUNCT_4:def 1 .= NAT \/ dom (0 .--> Next i1) by A7,FUNCT_2:def 1 .= NAT \/ {0} by CQC_LANG:5 .= NAT by A6,XBOOLE_1:12; A9: dom f = NAT by A2,FUNCT_2:def 1; for x being set st x in dom f holds t.x in f.x proof let x be set such that A10: x in dom f; per cases; suppose A11: x = 0; then f.x = SCM-Instr-Loc by A2,SCMRING1:2; hence t.x in f.x by A4,A11; suppose x <> 0; then not x in dom (0 .--> Next i1) by A3,TARSKI:def 1; then t.x = s.x by FUNCT_4:12; hence t.x in f.x by A2,A10,CARD_3:18; end; then reconsider t as State of SCM R by A8,A9,CARD_3:18; reconsider w = t as SCM-State of R by Def1; dom(0 .--> i1) = {0} by CQC_LANG:5; then 0 in dom (0 .--> i1) by TARSKI:def 1; then A12: (w +* (0 .--> i1)).0 = (0 .--> i1).0 by FUNCT_4:14 .= i1 by CQC_LANG:6; A13: 7 is Element of Segm 8 by GR_CY_1:10; A14: a is Element of SCM-Data-Loc by Th1; A15: the Instruction-Locations of SCM R = SCM-Instr-Loc by Def1; assume A16: a =0_goto i1 is halting; per cases; suppose A17: w.(V cond_address) <> 0.R; A18: IC t = IC w by Th10; A19: IC w = w.0 by SCMRING1:def 4; A20: Exec(a =0_goto i1,t).IC SCM R = t.IC SCM R by A16,AMI_1:def 8 .= IC t by AMI_1:def 15 .= w.0 by A18,SCMRING1:def 4; reconsider e = w.0 as Instruction-Location of SCM R by A19,Def1; a is Element of SCM-Data-Loc by Th1; then t.a <> 0.R by A1,A13,A15,A17,SCMRING1:19; then Exec(a =0_goto i1, t).IC SCM R = Next IC t by Th18; then A21: Exec(a =0_goto i1,t).IC SCM R = Next e by A18,SCMRING1:def 4; consider mj being Element of SCM-Instr-Loc such that A22: mj = e & Next e = Next mj by Def10; Next e = mj + 2 by A22,AMI_2:def 15; hence contradiction by A20,A21,A22,XCMPLX_1:3; suppose A23: w.(V cond_address) = 0.R; w +* (0 .--> i1) = SCM-Chg(w,i5) by SCMRING1:def 5 .= SCM-Chg(w,V cjump_address) by A1,A13,A14,SCMRING1:19 .= SCM-Chg(w,IFEQ(w.(V cond_address),0.R,V cjump_address,Next IC w)) by A23,CQC_LANG:def 1 .= SCM-Exec-Res(V,w) by A1,A14,A15,SCMRING1:def 14 .= Exec(a =0_goto i1,t) by Th12 .= t by A16,AMI_1:def 8; hence contradiction by A5,A12,XCMPLX_1:3; end; Lm7: a := r is non halting proof consider s; Exec(a := r,s).IC SCM R = Next IC s by Th19; hence thesis by Th20; end; definition let R, a, b; cluster a:=b -> non halting; coherence by Lm1; cluster AddTo(a,b) -> non halting; coherence by Lm2; cluster SubFrom(a,b) -> non halting; coherence by Lm3; cluster MultBy(a,b) -> non halting; coherence by Lm4; end; definition let R, i1; cluster goto i1 -> non halting; coherence by Lm5; end; definition let R, a, i1; cluster a =0_goto i1 -> non halting; coherence by Lm6; end; definition let R, a, r; cluster a:=r -> non halting; coherence by Lm7; end; definition let R; cluster SCM R -> halting definite data-oriented steady-programmed realistic; coherence proof thus SCM R is halting proof reconsider I = [0,{}] as Instruction of SCM R by Th3; take I; thus I is halting by Th21; let W be Instruction of SCM R such that A1: W is halting; assume A2: I <> W; per cases by Th8; suppose W = [0,{}]; hence thesis by A2; suppose ex a,b st W = a := b; hence thesis by A1; suppose ex a,b st W = AddTo(a,b); hence thesis by A1; suppose ex a,b st W = SubFrom(a,b); hence thesis by A1; suppose ex a,b st W = MultBy(a,b); hence thesis by A1; suppose ex i1 st W = goto i1; hence thesis by A1; suppose ex a,i1 st W = a =0_goto i1; hence thesis by A1; suppose ex a,r st W = a := r; hence thesis by A1; end; thus SCM R is definite proof let l be Instruction-Location of SCM R; reconsider L = l as Element of SCM-Instr-Loc by Def1; thus ObjectKind l = (the Object-Kind of SCM R).l by AMI_1:def 6 .= (SCM-OK R).L by Def1 .= SCM-Instr R by SCMRING1:6 .= the Instructions of SCM R by Def1; end; thus SCM R is data-oriented proof let x be set; assume A3: x in (the Object-Kind of SCM R)"{ the Instructions of SCM R }; then x in (the Object-Kind of SCM R)"{ SCM-Instr R } by Def1; then A4: x in (SCM-OK R)"{ SCM-Instr R} by Def1; reconsider x as Nat by A3,Def1; (SCM-OK R).x in { SCM-Instr R } by A4,FUNCT_2:46; then (SCM-OK R).x = SCM-Instr R by TARSKI:def 1; then consider i such that A5: x = 2*i+2*1 by SCMRING1:4; x = 2*(i + 1) & i + 1 > 0 by A5,NAT_1:19,XCMPLX_1:8; then x in SCM-Instr-Loc by AMI_2:def 3; hence thesis by Def1; end; thus SCM R is steady-programmed proof let s be State of SCM R, j be Instruction of SCM R, l be Instruction-Location of SCM R; reconsider c = j as Element of SCM-Instr R by Def1; SCM-Instr R = { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } \/ { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by SCMRING1:def 1; then c in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by XBOOLE_0:def 2; then c in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/ { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } or c in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by XBOOLE_0:def 2; then A6: c in { [0,{}] } \/ { [I,<*a,b*>] where a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } or c in { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } or c in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction } by XBOOLE_0:def 2; reconsider S = s as SCM-State of R by Def1; reconsider l' = l as Element of SCM-Instr-Loc by Def1; A7: Exec(j,s) = (((the Execution of SCM R) qua Function of the Instructions of SCM R, Funcs(product the Object-Kind of SCM R, product the Object-Kind of SCM R)).j).s by AMI_1:def 7 .= (SCM-Exec R).c.S by Def1 .= SCM-Exec-Res(c,S) by SCMRING1:def 15; now per cases by A6,XBOOLE_0:def 2; case c in { [0,{}] }; then c = [0,{}] by TARSKI:def 1; then c`2 = {} by MCART_1:7; then not (ex mk, ml being Element of SCM-Data-Loc st c = [ 1, <*mk, ml*>] ) & not (ex mk, ml being Element of SCM-Data-Loc st c = [ 2, <*mk, ml*>]) & not (ex mk, ml being Element of SCM-Data-Loc st c = [ 3, <*mk, ml*>]) & not (ex mk, ml being Element of SCM-Data-Loc st c = [ 4, <*mk, ml*>]) & not (ex mk being Element of SCM-Instr-Loc st c = [ 6, <*mk*>]) & not (ex mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc st c = [ 7, <*mk,ml*>]) & not (ex mk being Element of SCM-Data-Loc, r being Element of R st c = [ 5, <*mk,r*>]) by MCART_1:7; hence SCM-Exec-Res(c,S).l' = S.l' by SCMRING1:def 14; case c in { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction }; then consider i being Element of SCM-Instr-Loc such that A8: c = [6,<*i*>] and not contradiction; thus SCM-Exec-Res(c,S).l' = SCM-Chg(S,c jump_address).l' by A8,SCMRING1:def 14 .= S.l' by SCMRING1:12; case c in { [7,<*i,a*>] where i is Element of SCM-Instr-Loc, a is Element of SCM-Data-Loc: not contradiction }; then consider i being Element of SCM-Instr-Loc, a being Element of SCM-Data-Loc such that A9: c = [7,<*i,a*>] and not contradiction; thus SCM-Exec-Res(c,S).l' = SCM-Chg(S,IFEQ(S.(c cond_address),0.R,c cjump_address,Next IC S)).l' by A9,SCMRING1:def 14 .= S.l' by SCMRING1:12; case c in { [I,<*a,b*>] where I is Element of Segm 8, a,b is Element of SCM-Data-Loc: I in { 1,2,3,4 } }; then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that A10: c = [I,<*a,b*>] & I in {1,2,3,4}; now per cases by A10,ENUMSET1:18; case I = 1; hence SCM-Exec-Res(c,S).l' = SCM-Chg(SCM-Chg(S, c address_1,S.(c address_2)), Next IC S).l' by A10,SCMRING1:def 14 .= SCM-Chg(S, c address_1,S.(c address_2)).l' by SCMRING1:12 .= S.l' by SCMRING1:16; case I = 2; hence SCM-Exec-Res(c,S).l' = SCM-Chg(SCM-Chg(S,c address_1, S.(c address_1)+S.(c address_2)),Next IC S).l' by A10,SCMRING1:def 14 .= SCM-Chg(S,c address_1,S.(c address_1)+S.(c address_2)).l' by SCMRING1:12 .= S.l' by SCMRING1:16; case I = 3; hence SCM-Exec-Res(c,S).l' = SCM-Chg(SCM-Chg(S,c address_1, S.(c address_1)-S.(c address_2)),Next IC S).l' by A10,SCMRING1:def 14 .= SCM-Chg(S,c address_1,S.(c address_1)-S.(c address_2)).l' by SCMRING1:12 .= S.l' by SCMRING1:16; case I = 4; hence SCM-Exec-Res(c,S).l' = SCM-Chg(SCM-Chg(S,c address_1, S.(c address_1)*S.(c address_2)),Next IC S).l' by A10,SCMRING1:def 14 .= SCM-Chg(S,c address_1,S.(c address_1)*S.(c address_2)).l' by SCMRING1:12 .= S.l' by SCMRING1:16; end; hence SCM-Exec-Res(c,S).l' = S.l'; case c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc, r is Element of R: not contradiction }; then consider a being Element of SCM-Data-Loc, r being Element of R such that A11: c = [5,<*a,r*>] and not contradiction; thus SCM-Exec-Res(c,S).l' = SCM-Chg(SCM-Chg(S, c const_address, c const_value), Next IC S).l' by A11,SCMRING1:def 14 .= SCM-Chg(S, c const_address, c const_value).l' by SCMRING1:12 .= S.l' by SCMRING1:16; end; hence s.l = Exec(j,s).l by A7; end; the Instruction-Locations of SCM R = SCM-Instr-Loc & the Instructions of SCM R = SCM-Instr R by Def1; hence the Instructions of SCM R <> the Instruction-Locations of SCM R by SCMRING1:1; end; end; canceled 7; theorem Th29: for I being Instruction of SCM R st I is halting holds I = halt SCM R proof let I be Instruction of SCM R such that A1: I is halting; consider K being Instruction of SCM R such that K is halting and A2: for J being Instruction of SCM R st J is halting holds K = J by AMI_1:def 9; thus I = K by A1,A2 .= halt SCM R by A2; end; theorem halt SCM R = [0,{}] proof reconsider I = [0,{}] as Instruction of SCM R by Th3; I is halting by Th21; hence thesis by Th29; end;

Back to top