Copyright (c) 1993 Association of Mizar Users
environ vocabulary AMI_1, INT_1, AMI_2, GR_CY_1, RELAT_1, FUNCT_1, CAT_1, FINSEQ_1, FUNCT_2, CARD_3, ARYTM_1, NAT_1, CQC_LANG, BOOLE, MCART_1, FUNCT_4, PARTFUN1, FUNCOP_1, FINSET_1, ORDINAL2, AMI_3, ARYTM; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, FUNCT_2, INT_1, NAT_1, MCART_1, CQC_LANG, CARD_3, GR_CY_1, RELAT_1, FUNCT_4, PARTFUN1, FINSET_1, FINSEQ_1, STRUCT_0, AMI_1, CAT_3, AMI_2; constructors DOMAIN_1, REAL_1, NAT_1, CAT_2, FINSEQ_4, AMI_1, AMI_2, CAT_3, MEMBERED, XBOOLE_0; clusters INT_1, AMI_1, FUNCT_1, RELSET_1, AMI_2, CQC_LANG, NAT_1, FINSET_1, XBOOLE_0, FRAENKEL, MEMBERED, ZFMISC_1, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions AMI_1, TARSKI, INT_1, XBOOLE_0; theorems NAT_1, PARTFUN1, FUNCT_1, SUBSET_1, GRFUNC_1, TARSKI, ZFMISC_1, ENUMSET1, AMI_2, CQC_LANG, FUNCT_4, AMI_1, FUNCOP_1, CARD_3, FUNCT_2, MCART_1, FINSEQ_3, TREES_1, INT_1, RELAT_1, RELSET_1, GR_CY_1, STRUCT_0, ORDINAL2, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1; begin :: A small concrete machine reserve i,j,k for Nat; definition func SCM -> strict AMI-Struct over { INT } equals :Def1: AMI-Struct(#NAT,0,SCM-Instr-Loc,Segm 9,SCM-Instr,SCM-OK,SCM-Exec#); coherence; end; definition cluster SCM -> non empty non void; coherence by Def1,AMI_1:def 3,STRUCT_0:def 1; end; theorem Th1: SCM is data-oriented proof set A = SCM; let x be set; assume A1: x in (the Object-Kind of A)"{ the Instructions of A }; then reconsider x as Nat by Def1,FUNCT_2:46; SCM-OK.x in { SCM-Instr } by A1,Def1,FUNCT_2:46; then SCM-OK.x = SCM-Instr by TARSKI:def 1; then consider k such that A2: x = 2*k+2*1 by AMI_2:9; x = 2*(k + 1) & k + 1 > 0 by A2,NAT_1:19,XCMPLX_1:8; hence thesis by Def1,AMI_2:def 3; end; theorem Th2: SCM is definite proof let l be Instruction-Location of SCM; reconsider L = l as Element of SCM-Instr-Loc by Def1; thus ObjectKind l = SCM-OK.L by Def1,AMI_1:def 6 .= the Instructions of SCM by Def1,AMI_2:11; end; definition cluster SCM -> IC-Ins-separated data-oriented definite; coherence proof SCM is IC-Ins-separated proof A1: IC SCM = 0 by Def1,AMI_1:def 5; ObjectKind IC SCM = SCM-OK.IC SCM by Def1,AMI_1:def 6 .= the Instruction-Locations of SCM by A1,Def1,AMI_2:def 5; hence thesis by AMI_1:def 11; end; hence thesis by Th1,Th2; end; end; definition mode Data-Location -> Object of SCM means :Def2: it in SCM-Data-Loc; existence proof consider x being Element of SCM-Data-Loc; reconsider x as Object of SCM by Def1; take x; thus thesis; end; end; definition let s be State of SCM, d be Data-Location; redefine func s.d -> Integer; coherence proof reconsider S = s as SCM-State by Def1; reconsider D = d as Element of SCM-Data-Loc by Def2; S.D = s.d; hence thesis; end; end; reserve a,b,c for Data-Location, loc for Instruction-Location of SCM, I for Instruction of SCM; definition let a,b; func a := b -> Instruction of SCM equals :Def3: [ 1, <*a, b*>]; correctness proof reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2; 1 in { 1,2,3,4,5} by ENUMSET1:24; then [ 1, <*mk, ml*>] in SCM-Instr by AMI_2:5; hence thesis by Def1; end; func AddTo(a,b) -> Instruction of SCM equals :Def4: [ 2, <*a, b*>]; correctness proof reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2; 2 in { 1,2,3,4,5} by ENUMSET1:24; then [ 2, <*mk, ml*>] in SCM-Instr by AMI_2:5; hence thesis by Def1; end; func SubFrom(a,b) -> Instruction of SCM equals :Def5: [ 3, <*a, b*>]; correctness proof reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2; 3 in { 1,2,3,4,5} by ENUMSET1:24; then [ 3, <*mk, ml*>] in SCM-Instr by AMI_2:5; hence thesis by Def1; end; func MultBy(a,b) -> Instruction of SCM equals :Def6: [ 4, <*a, b*>]; correctness proof reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2; 4 in { 1,2,3,4,5} by ENUMSET1:24; then [ 4, <*mk, ml*>] in SCM-Instr by AMI_2:5; hence thesis by Def1; end; func Divide(a,b) -> Instruction of SCM equals :Def7: [ 5, <*a, b*>]; correctness proof reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2; 5 in { 1,2,3,4,5} by ENUMSET1:24; then [ 5, <*mk, ml*>] in SCM-Instr by AMI_2:5; hence thesis by Def1; end; end; definition let loc; func goto loc -> Instruction of SCM equals :Def8: [ 6, <*loc*>]; correctness by Def1, AMI_2:3; let a; func a=0_goto loc -> Instruction of SCM equals :Def9: [ 7, <*loc,a*>]; correctness proof reconsider loc as Element of SCM-Instr-Loc by Def1; reconsider a as Element of SCM-Data-Loc by Def2; 7 in { 7,8 } by TARSKI:def 2; then [ 7, <*loc,a*>] in SCM-Instr by AMI_2:4; hence thesis by Def1; end; func a>0_goto loc -> Instruction of SCM equals :Def10: [ 8, <*loc,a*>]; correctness proof reconsider loc as Element of SCM-Instr-Loc by Def1; reconsider a as Element of SCM-Data-Loc by Def2; 8 in { 7,8 } by TARSKI:def 2; then [ 8, <*loc,a*>] in SCM-Instr by AMI_2:4; hence thesis by Def1; end; end; reserve s for State of SCM; canceled; theorem Th4: IC SCM = 0 by Def1,AMI_1:def 5; theorem Th5: for S being SCM-State st S = s holds IC s = IC S proof let S be SCM-State; assume S = s; hence IC s = S.0 by Th4,AMI_1:def 15 .= IC S by AMI_2:def 6; end; definition let loc be Instruction-Location of SCM; func Next loc -> Instruction-Location of SCM means :Def11: ex mj being Element of SCM-Instr-Loc st mj = loc & it = Next mj; existence proof reconsider loc as Element of SCM-Instr-Loc by Def1; Next loc is Instruction-Location of SCM by Def1; hence thesis; end; correctness; end; theorem Th6: for loc being Instruction-Location of SCM, mj being Element of SCM-Instr-Loc st mj = loc holds Next mj = Next loc proof let loc be Instruction-Location of SCM, mj be Element of SCM-Instr-Loc; ex mj being Element of SCM-Instr-Loc st mj = loc & Next loc= Next mj by Def11; hence thesis; end; theorem Th7: for i being Element of SCM-Instr st i = I for S being SCM-State st S = s holds Exec(I,s) = SCM-Exec-Res(i,S) proof let i be Element of SCM-Instr such that A1: i = I; let S be SCM-State; assume S = s; hence Exec(I,s) = (SCM-Exec.i qua Element of Funcs(product SCM-OK, product SCM-OK)).S by A1,Def1,AMI_1:def 7 .= SCM-Exec-Res(i,S) by AMI_2:def 17; end; begin :: Users guide theorem Th8: Exec(a:=b, s).IC SCM = 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 mk = a, ml = b as Element of SCM-Data-Loc by Def2; reconsider I = a:=b as Element of SCM-Instr by Def1; reconsider S = s as SCM-State by Def1; set S1 = SCM-Chg(S, I address_1,S.(I address_2)); reconsider i = 1 as Element of Segm 9 by GR_CY_1:10; A1: I = [ i, <*mk, ml*>] by Def3; A2: IC s = IC S by Th5; A3: Exec(a:=b, s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16; A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23; thus Exec(a:=b, s).IC SCM = Next IC S by A3,Th4,AMI_2:16 .= Next IC s by A2,Th6; thus Exec(a:=b, s).a = S1.mk by A3,AMI_2:17 .= s.b by A4,AMI_2:20; let c; reconsider mn = c as Element of SCM-Data-Loc by Def2; assume A5: c <> a; thus Exec(a:=b, s).c = S1.mn by A3,AMI_2:17 .= s.c by A4,A5,AMI_2:21; end; theorem Th9: Exec(AddTo(a,b), s).IC SCM = 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 mk = a, ml = b as Element of SCM-Data-Loc by Def2; reconsider I = AddTo(a,b) as Element of SCM-Instr by Def1; reconsider S = s as SCM-State 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 9 by GR_CY_1:10; A1: I = [ i, <*mk, ml*>] by Def4; A2: IC s = IC S by Th5; A3: Exec(AddTo(a,b), s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16; A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23; thus Exec(AddTo(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16 .= Next IC s by A2,Th6; thus Exec(AddTo(a,b), s).a = S1.mk by A3,AMI_2:17 .= s.a + s.b by A4,AMI_2:20; let c; reconsider mn = c as Element of SCM-Data-Loc by Def2; assume A5: c <> a; thus Exec(AddTo(a,b), s).c = S1.mn by A3,AMI_2:17 .= s.c by A4,A5,AMI_2:21; end; theorem Th10: Exec(SubFrom(a,b), s).IC SCM = 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 mk = a, ml = b as Element of SCM-Data-Loc by Def2; reconsider I = SubFrom(a,b) as Element of SCM-Instr by Def1; reconsider S = s as SCM-State 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 9 by GR_CY_1:10; A1: I = [ i, <*mk, ml*>] by Def5; A2: IC s = IC S by Th5; A3: Exec(SubFrom(a,b), s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16; A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23; thus Exec(SubFrom(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16 .= Next IC s by A2,Th6; thus Exec(SubFrom(a,b), s).a = S1.mk by A3,AMI_2:17 .= s.a - s.b by A4,AMI_2:20; let c; reconsider mn = c as Element of SCM-Data-Loc by Def2; assume A5: c <> a; thus Exec(SubFrom(a,b), s).c = S1.mn by A3,AMI_2:17 .= s.c by A4,A5,AMI_2:21; end; theorem Th11: Exec(MultBy(a,b), s).IC SCM = 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 mk = a, ml = b as Element of SCM-Data-Loc by Def2; reconsider I = MultBy(a,b) as Element of SCM-Instr by Def1; reconsider S = s as SCM-State 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 9 by GR_CY_1:10; A1: I = [ i, <*mk, ml*>] by Def6; A2: IC s = IC S by Th5; A3: Exec(MultBy(a,b), s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16; A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23; thus Exec(MultBy(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16 .= Next IC s by A2,Th6; thus Exec(MultBy(a,b), s).a = S1.mk by A3,AMI_2:17 .= s.a * s.b by A4,AMI_2:20; let c; reconsider mn = c as Element of SCM-Data-Loc by Def2; assume A5: c <> a; thus Exec(MultBy(a,b), s).c = S1.mn by A3,AMI_2:17 .= s.c by A4,A5,AMI_2:21; end; theorem Th12: Exec(Divide(a,b), s).IC SCM = Next IC s & (a <> b implies Exec(Divide(a,b), s).a = s.a div s.b) & Exec(Divide(a,b), s).b = s.a mod s.b & for c st c <> a & c <> b holds Exec(Divide(a,b), s).c = s.c proof reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2; reconsider I = Divide(a,b) as Element of SCM-Instr by Def1; reconsider S = s as SCM-State by Def1; set S1 = SCM-Chg(S, I address_1,S.(I address_1) div S.(I address_2)); set S1' = SCM-Chg(S1, I address_2,S.(I address_1) mod S.(I address_2)); reconsider i = 5 as Element of Segm 9 by GR_CY_1:10; A1: I = [ i, <*mk, ml*>] by Def7; A2: IC s = IC S by Th5; A3: Exec(Divide(a,b), s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1', Next IC S)) by A1,AMI_2:def 16; A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23; thus Exec(Divide(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16 .= Next IC s by A2,Th6; hereby assume A5: a <> b; thus Exec(Divide(a,b), s).a = S1'.mk by A3,AMI_2:17 .= S1.mk by A4,A5,AMI_2:21 .= s.a div s.b by A4,AMI_2:20; end; thus Exec(Divide(a,b), s).b = S1'.ml by A3,AMI_2:17 .= s.a mod s.b by A4,AMI_2:20; let c; reconsider mn = c as Element of SCM-Data-Loc by Def2; assume A6: c <> a & c <> b; thus Exec(Divide(a,b), s).c = S1'.mn by A3,AMI_2:17 .= S1.mn by A4,A6,AMI_2:21 .= s.c by A4,A6,AMI_2:21; end; theorem Exec(goto loc, s).IC SCM = loc & Exec(goto loc, s).c = s.c proof reconsider mj = loc as Element of SCM-Instr-Loc by Def1; reconsider I = goto loc as Element of SCM-Instr by Def1; reconsider S = s as SCM-State by Def1; reconsider i = 6 as Element of Segm 9 by GR_CY_1:10; A1: I = [ i, <*mj*>] by Def8; A2: Exec(goto loc, s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S,I jump_address)) by A1,AMI_2:def 16; I jump_address = mj by A1,AMI_2:24; hence Exec(goto loc, s).IC SCM = loc by A2,Th4,AMI_2:16; reconsider mn = c as Element of SCM-Data-Loc by Def2; thus Exec(goto loc, s).c = S.mn by A2,AMI_2:17 .= s.c; end; theorem Th14: (s.a = 0 implies Exec(a =0_goto loc, s).IC SCM = loc) & (s.a <> 0 implies Exec(a=0_goto loc, s).IC SCM = Next IC s) & Exec(a=0_goto loc, s).c = s.c proof reconsider mj = loc as Element of SCM-Instr-Loc by Def1; reconsider a' = a as Element of SCM-Data-Loc by Def2; reconsider I = a=0_goto loc as Element of SCM-Instr by Def1; reconsider S = s as SCM-State by Def1; reconsider i = 7 as Element of Segm 9 by GR_CY_1:10; A1: I = [ i, <*mj,a'*>] by Def9; A2: IC s = IC S by Th5; A3: Exec(a=0_goto loc, s) = SCM-Exec-Res(I,S) by Th7 .= SCM-Chg(S,IFEQ(S.(I cond_address),0,I cjump_address,Next IC S)) by A1,AMI_2:def 16; thus s.a = 0 implies Exec(a=0_goto loc, s).IC SCM = loc proof assume s.a = 0; then A4: S.(I cond_address)=0 by A1,AMI_2:25; thus Exec(a=0_goto loc, s).IC SCM = IFEQ(S.(I cond_address),0,I cjump_address,Next IC S) by A3,Th4,AMI_2:16 .= I cjump_address by A4,CQC_LANG:def 1 .= loc by A1,AMI_2:25; end; thus s.a <> 0 implies Exec(a=0_goto loc, s).IC SCM = Next IC s proof assume s.a <> 0; then A5: S.(I cond_address) <> 0 by A1,AMI_2:25; thus Exec(a=0_goto loc, s).IC SCM = IFEQ(S.(I cond_address),0,I cjump_address,Next IC S) by A3,Th4,AMI_2:16 .= Next IC S by A5,CQC_LANG:def 1 .= Next IC s by A2,Th6; end; reconsider mn = c as Element of SCM-Data-Loc by Def2; thus Exec(a=0_goto loc, s).c = S.mn by A3,AMI_2:17 .= s.c; end; theorem Th15: (s.a > 0 implies Exec(a >0_goto loc, s).IC SCM = loc) & (s.a <= 0 implies Exec(a>0_goto loc, s).IC SCM = Next IC s) & Exec(a>0_goto loc, s).c = s.c proof reconsider mj = loc as Element of SCM-Instr-Loc by Def1; reconsider a' = a as Element of SCM-Data-Loc by Def2; reconsider I = a>0_goto loc as Element of SCM-Instr by Def1; reconsider S = s as SCM-State by Def1; reconsider i = 8 as Element of Segm 9 by GR_CY_1:10; A1: I = [ i, <*mj,a'*>] by Def10; A2: IC s = IC S by Th5; A3: Exec(a>0_goto loc, s) = SCM-Exec-Res(I,S) by Th7 .= SCM-Chg(S,IFGT(S.(I cond_address),0,I cjump_address,Next IC S)) by A1,AMI_2:def 16; thus s.a > 0 implies Exec(a>0_goto loc, s).IC SCM = loc proof assume s.a > 0; then A4: S.(I cond_address) > 0 by A1,AMI_2:25; thus Exec(a>0_goto loc, s).IC SCM = IFGT(S.(I cond_address),0,I cjump_address,Next IC S) by A3,Th4,AMI_2:16 .= I cjump_address by A4,AMI_2:def 14 .= loc by A1,AMI_2:25; end; thus s.a <= 0 implies Exec(a>0_goto loc, s).IC SCM = Next IC s proof assume s.a <= 0; then A5: S.(I cond_address) <= 0 by A1,AMI_2:25; thus Exec(a>0_goto loc, s).IC SCM = IFGT(S.(I cond_address),0,I cjump_address,Next IC S) by A3,Th4,AMI_2:16 .= Next IC S by A5,AMI_2:def 14 .= Next IC s by A2,Th6; end; reconsider mn = c as Element of SCM-Data-Loc by Def2; thus Exec(a>0_goto loc, s).c = S.mn by A3,AMI_2:17 .= s.c; end; reserve Y,K,T for Element of Segm 9, a1,a2,a3 for Element of SCM-Instr-Loc, b1,b2,c1,c2,c3 for Element of SCM-Data-Loc; Lm1: for I being Instruction of SCM st ex s st Exec(I,s).IC SCM = Next IC s holds I is non halting proof let I be Instruction of SCM; given s such that A1: Exec(I, s).IC SCM = Next IC s; assume A2: I is halting; reconsider t = s as SCM-State by Def1; A3: IC t = IC s by Th5; A4: IC t = t.0 by AMI_2:def 6; A5: Exec(I,s).IC SCM = s.IC SCM by A2,AMI_1:def 8 .= t.0 by A3,A4,AMI_1:def 15; reconsider w = t.0 as Instruction-Location of SCM by A4,Def1; consider mj being Element of SCM-Instr-Loc such that A6: mj = w & Next w = Next mj by Def11; A7: Exec(I,s).IC SCM = Next w by A1,A4,Th5; Next w = mj + 2 by A6,AMI_2:def 15; hence contradiction by A5,A6,A7,XCMPLX_1:3; end; Lm2: for I being Instruction of SCM st I = [0,{}] holds I is halting proof let I be Instruction of SCM such that A1: I = [0,{}]; let s be State of SCM; reconsider L = I as Element of SCM-Instr by A1,AMI_2:2; A2: I`2 = {} by A1,MCART_1:7; A3: now let i; let mk, ml be Element of SCM-Data-Loc; assume I = [ i, <*mk, ml*>]; then I`2 = <*mk, ml*> by MCART_1:7; hence contradiction by A2,FINSEQ_3:38; end; A4: now let i; let mk be Element of SCM-Instr-Loc; assume I = [ i, <*mk*>]; then I`2 = <*mk*> by MCART_1:7; hence contradiction by A2,TREES_1:4; end; now let i; let mk be Element of SCM-Instr-Loc, ml be Element of SCM-Data-Loc; assume I = [ i, <*mk, ml*>]; then I`2 = <*mk, ml*> by MCART_1:7; hence contradiction by A2,FINSEQ_3:38; end; then A5: 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, ml being Element of SCM-Data-Loc st I = [ 5, <*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-Instr-Loc, ml being Element of SCM-Data-Loc st I = [ 8, <*mk,ml*>]) by A3,A4; reconsider t = s as SCM-State by Def1; thus Exec(I,s) = SCM-Exec-Res(L,t) by Th7 .= s by A5,AMI_2:def 16; end; Lm3: a := b is non halting proof consider s; Exec(a:=b,s).IC SCM = Next IC s by Th8; hence thesis by Lm1; end; Lm4: AddTo(a,b) is non halting proof consider s; Exec(AddTo(a,b),s).IC SCM = Next IC s by Th9; hence thesis by Lm1; end; Lm5: SubFrom(a,b) is non halting proof consider s; Exec(SubFrom(a,b),s).IC SCM = Next IC s by Th10; hence thesis by Lm1; end; Lm6: MultBy(a,b) is non halting proof consider s; Exec(MultBy(a,b),s).IC SCM = Next IC s by Th11; hence thesis by Lm1; end; Lm7: Divide(a,b) is non halting proof consider s; Exec(Divide(a,b),s).IC SCM = Next IC s by Th12; hence thesis by Lm1; end; Lm8: goto loc is non halting proof assume A1: goto loc is halting; reconsider V = goto loc as Element of SCM-Instr by Def1; reconsider a3 = loc as Element of SCM-Instr-Loc by Def1; A2: goto loc = [ 6, <*loc*>] by Def8; consider s being SCM-State; set t = s +* (0.--> Next a3); set f = the Object-Kind of SCM; A3: dom(0 .--> Next a3) = {0} by CQC_LANG:5; then 0 in dom (0.--> Next a3) by TARSKI:def 1; then A4: t.0 = (0.--> Next a3).0 by FUNCT_4:14 .= Next a3 by CQC_LANG:6; then A5: t.0 = a3 + 2 by AMI_2:def 15; A6: {0} c= NAT by ZFMISC_1:37; A7: dom s = dom SCM-OK by CARD_3:18; A8: dom t = dom s \/ dom (0.--> Next a3) by FUNCT_4:def 1 .= NAT \/ dom (0.--> Next a3) by A7,FUNCT_2:def 1 .= NAT \/ {0} by CQC_LANG:5 .= NAT by A6,XBOOLE_1:12; A9: dom f = NAT by Def1,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 Def1,AMI_2:7; hence t.x in f.x by A4,A11; suppose x <> 0; then not x in dom (0.--> Next a3) by A3,TARSKI:def 1; then t.x = s.x by FUNCT_4:12; hence t.x in f.x by A10,Def1,CARD_3:18; end; then reconsider t as State of SCM by A8,A9,CARD_3:18; reconsider w = t as SCM-State by Def1; dom(0 .--> loc) = {0} by CQC_LANG:5; then 0 in dom (0 .--> loc) by TARSKI:def 1; then A12: (w +* (0 .--> loc)).0 = (0 .--> loc).0 by FUNCT_4:14 .= loc by CQC_LANG:6; A13: 6 is Element of Segm 9 by GR_CY_1:10; w +* (0 .--> loc) = SCM-Chg(w,a3) by AMI_2:def 7 .= SCM-Chg(w,V jump_address) by A2,A13,AMI_2:24 .= SCM-Exec-Res(V,w) by A2,AMI_2:def 16 .= Exec(goto loc,t) by Th7 .= t by A1,AMI_1:def 8; hence contradiction by A5,A12,XCMPLX_1:3; end; Lm9: a=0_goto loc is non halting proof reconsider V = a=0_goto loc as Element of SCM-Instr by Def1; reconsider a3 = loc as Element of SCM-Instr-Loc by Def1; A1: a=0_goto loc = [ 7, <*loc,a*>] by Def9; consider s being SCM-State; set t = s +* (0.--> Next a3); set f = the Object-Kind of SCM; A2: dom(0 .--> Next a3) = {0} by CQC_LANG:5; then 0 in dom (0.--> Next a3) by TARSKI:def 1; then A3: t.0 = (0.--> Next a3).0 by FUNCT_4:14 .= Next a3 by CQC_LANG:6; then A4: t.0 = a3 + 2 by AMI_2:def 15; A5: {0} c= NAT by ZFMISC_1:37; A6: dom s = dom SCM-OK by CARD_3:18; A7: dom t = dom s \/ dom (0.--> Next a3) by FUNCT_4:def 1 .= NAT \/ dom (0.--> Next a3) by A6,FUNCT_2:def 1 .= NAT \/ {0} by CQC_LANG:5 .= NAT by A5,XBOOLE_1:12; A8: dom f = NAT by Def1,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 A9: x in dom f; per cases; suppose A10: x = 0; then f.x = SCM-Instr-Loc by Def1,AMI_2:7; hence t.x in f.x by A3,A10; suppose x <> 0; then not x in dom (0.--> Next a3) by A2,TARSKI:def 1; then t.x = s.x by FUNCT_4:12; hence t.x in f.x by A9,Def1,CARD_3:18; end; then reconsider t as State of SCM by A7,A8,CARD_3:18; reconsider w = t as SCM-State by Def1; dom(0 .--> loc) = {0} by CQC_LANG:5; then 0 in dom (0 .--> loc) by TARSKI:def 1; then A11: (w +* (0 .--> loc)).0 = (0 .--> loc).0 by FUNCT_4:14 .= loc by CQC_LANG:6; A12: 7 is Element of Segm 9 by GR_CY_1:10; A13: a is Element of SCM-Data-Loc by Def2; assume A14: a=0_goto loc is halting; per cases; suppose A15: w.(V cond_address) <> 0; A16: IC t = IC w by Th5; A17: IC w = w.0 by AMI_2:def 6; A18: Exec(a=0_goto loc,t).IC SCM = t.IC SCM by A14,AMI_1:def 8 .= w.0 by A16,A17,AMI_1:def 15; reconsider e = w.0 as Instruction-Location of SCM by A17,Def1; t.a <> 0 by A1,A12,A13,A15,AMI_2:25; then A19: Exec(a=0_goto loc,t).IC SCM = Next e by A16,A17,Th14; consider mj being Element of SCM-Instr-Loc such that A20: mj = e & Next e = Next mj by Def11; Next e = mj + 2 by A20,AMI_2:def 15; hence contradiction by A18,A19,A20,XCMPLX_1:3; suppose w.(V cond_address) = 0; then A21: IFEQ(w.(V cond_address),0,V cjump_address,Next IC w) = V cjump_address by CQC_LANG:def 1; w +* (0 .--> loc) = SCM-Chg(w,a3) by AMI_2:def 7 .= SCM-Chg(w,IFEQ(w.(V cond_address),0,V cjump_address,Next IC w)) by A1, A12,A13,A21,AMI_2:25 .= SCM-Exec-Res(V,w) by A1,A13,AMI_2:def 16 .= Exec(a=0_goto loc,t) by Th7 .= t by A14,AMI_1:def 8; hence contradiction by A4,A11,XCMPLX_1:3; end; Lm10: a>0_goto loc is non halting proof reconsider V = a>0_goto loc as Element of SCM-Instr by Def1; reconsider a3 = loc as Element of SCM-Instr-Loc by Def1; A1: a>0_goto loc = [ 8, <*loc,a*>] by Def10; consider s being SCM-State; set t = s +* (0.--> Next a3); set f = the Object-Kind of SCM; A2: dom(0 .--> Next a3) = {0} by CQC_LANG:5; then 0 in dom (0.--> Next a3) by TARSKI:def 1; then A3: t.0 = (0.--> Next a3).0 by FUNCT_4:14 .= Next a3 by CQC_LANG:6; then A4: t.0 = a3 + 2 by AMI_2:def 15; A5: {0} c= NAT by ZFMISC_1:37; A6: dom s = dom SCM-OK by CARD_3:18; A7: dom t = dom s \/ dom (0.--> Next a3) by FUNCT_4:def 1 .= NAT \/ dom (0.--> Next a3) by A6,FUNCT_2:def 1 .= NAT \/ {0} by CQC_LANG:5 .= NAT by A5,XBOOLE_1:12; A8: dom f = NAT by Def1,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 A9: x in dom f; per cases; suppose A10: x = 0; then f.x = SCM-Instr-Loc by Def1,AMI_2:7; hence t.x in f.x by A3,A10; suppose x <> 0; then not x in dom (0.--> Next a3) by A2,TARSKI:def 1; then t.x = s.x by FUNCT_4:12; hence t.x in f.x by A9,Def1,CARD_3:18; end; then reconsider t as State of SCM by A7,A8,CARD_3:18; reconsider w = t as SCM-State by Def1; dom(0 .--> loc) = {0} by CQC_LANG:5; then 0 in dom (0 .--> loc) by TARSKI:def 1; then A11: (w +* (0 .--> loc)).0 = (0 .--> loc).0 by FUNCT_4:14 .= loc by CQC_LANG:6; A12: 8 is Element of Segm 9 by GR_CY_1:10; A13: a is Element of SCM-Data-Loc by Def2; assume A14: a>0_goto loc is halting; per cases; suppose A15: w.(V cond_address) <= 0; A16: IC t = IC w by Th5; A17: IC w = w.0 by AMI_2:def 6; A18: Exec(a>0_goto loc,t).IC SCM = t.IC SCM by A14,AMI_1:def 8 .= w.0 by A16,A17,AMI_1:def 15; reconsider e = w.0 as Instruction-Location of SCM by A17,Def1; t.a <= 0 by A1,A12,A13,A15,AMI_2:25; then A19: Exec(a>0_goto loc,t).IC SCM = Next e by A16,A17,Th15; consider mj being Element of SCM-Instr-Loc such that A20: mj = e & Next e = Next mj by Def11; Next e = mj + 2 by A20,AMI_2:def 15; hence contradiction by A18,A19,A20,XCMPLX_1:3; suppose w.(V cond_address) > 0; then A21: IFGT(w.(V cond_address),0,V cjump_address,Next IC w) = V cjump_address by AMI_2:def 14; w +* (0 .--> loc) = SCM-Chg(w,a3) by AMI_2:def 7 .= SCM-Chg(w,IFGT(w.(V cond_address),0,V cjump_address,Next IC w)) by A1, A12,A13,A21,AMI_2:25 .= SCM-Exec-Res(V,w) by A1,A13,AMI_2:def 16 .= Exec(a>0_goto loc,t) by Th7 .= t by A14,AMI_1:def 8; hence contradiction by A4,A11,XCMPLX_1:3; end; Lm11: for I being set holds I is Instruction of SCM 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 a,b st I = Divide(a,b)) or (ex loc st I = goto loc) or (ex a,loc st I = a=0_goto loc) or ex a,loc st I = a>0_goto loc proof let I be set; thus I is Instruction of SCM implies 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 a,b st I = Divide(a,b)) or (ex loc st I = goto loc) or (ex a,loc st I = a=0_goto loc) or ex a,loc st I = a>0_goto loc proof assume I is Instruction of SCM; then I in { [SCM-Halt,{}] } \/ { [Y,<*a3*>] : Y = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } or I in { [T,<*c2,c3*>] : T in { 1,2,3,4,5 } } by Def1,AMI_2:def 4, XBOOLE_0:def 2; then A1: I in { [SCM-Halt,{}] } \/ { [Y,<*a3*>] : Y = 6 } or I in { [K,<*a1,b1*>] : K in { 7,8 } } or I in { [T,<*c2,c3*>] : T in { 1,2,3,4,5 } } by XBOOLE_0:def 2; per cases by A1,XBOOLE_0:def 2; suppose I in { [SCM-Halt,{}] }; hence thesis by AMI_2:def 1,TARSKI:def 1; suppose I in { [Y,<*a3*>] : Y = 6 }; then consider Y, a3 such that A2: I = [Y,<*a3*>] & Y = 6; reconsider loc = a3 as Instruction-Location of SCM by Def1; I = goto loc by A2,Def8; hence thesis; suppose I in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K, a1, b1 such that A3: I = [K,<*a1,b1*>] & K in { 7,8 }; reconsider loc = a1 as Instruction-Location of SCM by Def1; reconsider a = b1 as Data-Location by Def1,Def2; K = 7 or K = 8 by A3,TARSKI:def 2; then I = a=0_goto loc or I = a>0_goto loc by A3,Def9,Def10; hence thesis; suppose I in { [T,<*c2,c3*>] : T in { 1,2,3,4,5 } }; then consider T, c2, c3 such that A4: I = [T,<*c2,c3*>] & T in { 1,2,3,4,5 }; reconsider a = c2, b = c3 as Data-Location by Def1,Def2; T = 1 or T = 2 or T = 3 or T = 4 or T = 5 by A4,ENUMSET1:23; then I = a:=b or I = AddTo(a,b) or I = SubFrom(a,b) or I = MultBy(a,b) or I = Divide(a,b) by A4,Def3,Def4,Def5,Def6,Def7; hence thesis; end; thus thesis by Def1,AMI_2:2; end; definition cluster SCM -> halting; coherence proof reconsider I = [0,{}] as Instruction of SCM by Def1,AMI_2:2; take I; thus I is halting by Lm2; let W be Instruction of SCM such that A1: W is halting; assume A2: I <> W; per cases by Lm11; suppose W = [0,{}]; hence thesis by A2; suppose ex a,b st W = a:=b; hence thesis by A1,Lm3; suppose ex a,b st W = AddTo(a,b); hence thesis by A1,Lm4; suppose ex a,b st W = SubFrom(a,b); hence thesis by A1,Lm5; suppose ex a,b st W = MultBy(a,b); hence thesis by A1,Lm6; suppose ex a,b st W = Divide(a,b); hence thesis by A1,Lm7; suppose ex loc st W = goto loc; hence thesis by A1,Lm8; suppose ex a,loc st W = a=0_goto loc; hence thesis by A1,Lm9; suppose ex a,loc st W = a>0_goto loc; hence thesis by A1,Lm10; end; end; Lm12: for I being Instruction of SCM st I is halting holds I = halt SCM proof let I be Instruction of SCM such that A1: I is halting; consider K being Instruction of SCM such that K is halting and A2: for J being Instruction of SCM st J is halting holds K = J by AMI_1:def 9; thus I = K by A1,A2 .= halt SCM by A2; end; Lm13: halt SCM = [0,{}] proof reconsider I = [0,{}] as Instruction of SCM by Def1,AMI_2:2; I is halting by Lm2; hence thesis by Lm12; end; begin :: Preliminaries canceled 2; theorem Th18: for m,j being Integer holds m*j, 0 are_congruent_mod m proof let m,j be Integer; take j; thus m*j = m*j - 0; end; scheme INDI{ k,n() -> Nat, P[set] }: P[n()] provided A1: P[0] and A2: k() > 0 and A3: for i,j st P[k()*i] & j <> 0 & j <= k() holds P[k()*i+j] proof defpred R[Nat] means P[k()*$1]; A4: R[0] by A1; A5: now let i; assume A6: R[i]; k()*(i+1) = k()*i + k()*1 by XCMPLX_1:8 .= k()*i + k(); hence R[i+1] by A2,A3,A6; end; A7: for i holds R[i] from Ind(A4,A5); then A8: P[k()*(n() div k())]; per cases; suppose n() mod k() = 0; then n() = k() * (n() div k()) + 0 by A2,NAT_1:47; hence thesis by A7; suppose A9: n() mod k() <> 0; A10: n() = k() * (n() div k()) + (n() mod k()) by A2,NAT_1:47; n() mod k() <= k() by A2,NAT_1:46; hence thesis by A3,A8,A9,A10; end; theorem Th19: for X,Y being non empty set, f,g being PartFunc of X,Y st for x being Element of X, y being Element of Y holds [x,y] in f iff [x,y] in g holds f = g proof let X,Y be non empty set, f,g be PartFunc of X,Y such that A1: for x being Element of X, y being Element of Y holds [x,y] in f iff [x,y] in g; reconsider df = dom f, dg = dom g as Subset of X by RELSET_1:12; now let x be Element of X; hereby assume x in df; then [x,f.x] in f & f.x in Y by FUNCT_1:8,PARTFUN1:27; then [x,f.x] in g by A1; hence x in dg by FUNCT_1:8; end; assume x in dg; then [x,g.x] in g & g.x in Y by FUNCT_1:8,PARTFUN1:27; then [x,g.x] in f by A1; hence x in df by FUNCT_1:8; end; then A2: df = dg by SUBSET_1:8; now let x be Element of X; assume x in dom f; then [x,f.x] in f & f.x in Y by FUNCT_1:8,PARTFUN1:27; then [x,f.x] in g by A1; hence f.x = g.x by FUNCT_1:8; end; hence f = g by A2,PARTFUN1:34; end; theorem Th20: for f,g being Function, A,B being set st f|A = g|A & f|B = g|B holds f|(A \/ B) = g|(A \/ B) proof let f,g be Function, A,B be set; assume f|A = g|A & f|B = g|B; hence f|(A \/ B) = g|A \/ g|B by RELAT_1:107 .= g|(A \/ B) by RELAT_1:107; end; theorem for X being set, f,g being Function st dom g c= X & g c= f holds g c= f|X proof let X be set, f,g be Function; assume dom g c= X & g c= f; then g|dom g c= f|X by RELAT_1:106; hence g c= f|X by RELAT_1:97; end; theorem Th22: for f being Function, x being set st x in dom f holds f|{x} = {[x,f.x]} proof let f be Function, x be set such that A1: x in dom f; A2: x in {x} by TARSKI:def 1; dom(f|{x} qua Function) = dom f /\ {x} by RELAT_1:90 .= {x} by A1,ZFMISC_1:52; hence f|{x} = {[x,(f|{x}).x]} by GRFUNC_1:18 .= {[x,f.x]} by A2,FUNCT_1:72; end; theorem Th23: for f being Function, X being set st X misses dom f holds f|X = {} proof let f be Function, X be set such that A1: X /\ dom f = {}; thus f|X = (f|dom f)|X by RELAT_1:97 .= f|{} by A1,RELAT_1:100 .= {} by RELAT_1:110; end; theorem Th24: for f,g being Function, x being set st dom f = dom g & f.x = g.x holds f|{x} = g|{x} proof let f,g be Function, x be set such that A1: dom f = dom g and A2: f.x = g.x; per cases; suppose A3: x in dom f; hence f|{x} = {[x,g.x]} by A2,Th22 .= g|{x} by A1,A3,Th22; suppose not x in dom f; then A4: {x} misses dom f by ZFMISC_1:56; hence f|{x} = {} by Th23 .= g|{x} by A1,A4,Th23; end; theorem Th25: for f,g being Function, x,y being set st dom f = dom g & f.x = g.x & f.y = g.y holds f|{x,y} = g|{x,y} proof let f,g be Function, x,y be set such that A1: dom f = dom g and A2: f.x = g.x and A3: f.y = g.y; A4: f|{x} = g|{x} by A1,A2,Th24; A5: f|{y} = g|{y} by A1,A3,Th24; {x,y} = {x} \/ {y} by ENUMSET1:41; hence f|{x,y} = g|{x,y} by A4,A5,Th20; end; theorem for f,g being Function, x,y,z being set st dom f = dom g & f.x = g.x & f.y = g.y & f.z = g.z holds f|{x,y,z} = g|{x,y,z} proof let f,g be Function, x,y,z be set such that A1: dom f = dom g and A2: f.x = g.x & f.y = g.y and A3: f.z = g.z; A4: f|{x,y} = g|{x,y} by A1,A2,Th25; A5: f|{z} = g|{z} by A1,A3,Th24; {x,y,z} = {x,y} \/ {z} by ENUMSET1:43; hence f|{x,y,z} = g|{x,y,z} by A4,A5,Th20; end; theorem Th27: for a,b being set, f being Function st a in dom f & f.a = b holds a .--> b c= f proof let a,b be set, f be Function; assume a in dom f & f.a = b; then [a,b] in f by FUNCT_1:8; then {[a,b]} c= f by ZFMISC_1:37; hence a .--> b c= f by AMI_1:19; end; canceled; theorem for a,b,c,d being set, f being Function st a in dom f & c in dom f & f.a = b & f.c = d holds (a,c) --> (b,d) c= f proof let a,b,c,d be set, f be Function; assume A1: a in dom f & c in dom f & f.a = b & f.c = d; per cases; suppose A2: a <> c; [a,b] in f & [c,d] in f by A1,FUNCT_1:8; then { [a,b], [c,d]} c= f by ZFMISC_1:38; hence (a,c) --> (b,d) c= f by A2,FUNCT_4:71; suppose a = c; then (a,c) --> (b,d) = c .--> d by AMI_1:20; hence (a,c) --> (b,d) c= f by A1,Th27; end; begin :: Some Remarks on AMI-Struct reserve N for set; canceled; theorem Th31: for S being AMI-Struct over N, p being FinPartState of S holds p in FinPartSt S proof let S be AMI-Struct over N; let p be FinPartState of S; A1: FinPartSt S = { q where q is Element of sproduct the Object-Kind of S: q is finite } by AMI_1:def 23; p is finite by AMI_1:def 24; hence p in FinPartSt S by A1; end; definition let N be set; let S be AMI-Struct over N; cluster FinPartSt S -> non empty; coherence by Th31; end; theorem Th32: for S being AMI-Struct over N, p being Element of FinPartSt S holds p is FinPartState of S proof let S be AMI-Struct over N; let p be Element of FinPartSt S; A1: FinPartSt S = { q where q is Element of sproduct the Object-Kind of S: q is finite } by AMI_1:def 23; p in FinPartSt S; then ex q being Element of sproduct the Object-Kind of S st q = p & q is finite by A1; hence p is FinPartState of S by AMI_1:def 24; end; theorem Th33: for S being AMI-Struct over N, F1,F2 being PartFunc of FinPartSt S, FinPartSt S st for p,q being FinPartState of S holds [p,q] in F1 iff [p,q] in F2 holds F1 = F2 proof let S be AMI-Struct over N, F1,F2 be PartFunc of FinPartSt S, FinPartSt S such that A1: for p,q being FinPartState of S holds [p,q] in F1 iff [p,q] in F2; now let p,q be Element of FinPartSt S; reconsider p' = p, q' = q as FinPartState of S by Th32; [p',q'] in F1 iff [p',q'] in F2 by A1; hence [p,q] in F1 iff [p,q] in F2; end; hence F1 = F2 by Th19; end; scheme EqFPSFunc{ N() -> non empty with_non-empty_elements set, S() -> AMI-Struct over N(), P[set,set], IT1,IT2()->PartFunc of FinPartSt S(), FinPartSt S()}: IT1() = IT2() provided A1: for p,q being FinPartState of S() holds [p,q] in IT1() iff P[p,q] and A2: for p,q being FinPartState of S() holds [p,q] in IT2() iff P[p,q] proof now let p,q be FinPartState of S(); [p,q] in IT1() iff P[p,q] by A1; hence [p,q] in IT1() iff [p,q] in IT2() by A2; end; hence thesis by Th33; end; definition let N be with_non-empty_elements set; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let l be Instruction-Location of S; func Start-At l -> FinPartState of S equals :Def12: IC S .--> l; correctness proof ObjectKind IC S = the Instruction-Locations of S by AMI_1:def 11; hence thesis by AMI_1:59; end; end; reserve N for with_non-empty_elements set; theorem for S being IC-Ins-separated definite (non empty non void AMI-Struct over N) for l being Instruction-Location of S holds dom(Start-At l) = {IC S} proof let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let l be Instruction-Location of S; Start-At l = IC S .--> l by Def12 .= {IC S} --> l by CQC_LANG:def 2; hence thesis by FUNCOP_1:19; end; definition let N be set; let S be AMI-Struct over N; let IT be FinPartState of S; attr IT is programmed means :Def13: dom IT c= the Instruction-Locations of S; end; definition let N be set; let S be AMI-Struct over N; cluster programmed FinPartState of S; existence proof {} in sproduct the Object-Kind of S & {} is finite by AMI_1:26; then reconsider Z = {} as FinPartState of S by AMI_1:def 24; take Z; thus dom Z c= the Instruction-Locations of S by RELAT_1:60,XBOOLE_1:2; end; end; theorem for N being set for S being AMI-Struct over N for p1,p2 being programmed FinPartState of S holds p1 +* p2 is programmed proof let N be set, S be AMI-Struct over N; let p1,p2 be programmed FinPartState of S; A1: dom p1 c= the Instruction-Locations of S & dom p2 c= the Instruction-Locations of S by Def13; dom(p1 +* p2) = dom p1 \/ dom p2 by FUNCT_4:def 1; hence dom(p1 +* p2) c= the Instruction-Locations of S by A1,XBOOLE_1:8; end; theorem Th36: for S being non void AMI-Struct over N, s being State of S holds dom s = the carrier of S proof let S be non void AMI-Struct over N, s be State of S; thus dom s = dom the Object-Kind of S by CARD_3:18 .= the carrier of S by FUNCT_2:def 1; end; theorem Th37: for S being AMI-Struct over N, p being FinPartState of S holds dom p c= the carrier of S proof let S be AMI-Struct over N, p be FinPartState of S; sproduct the Object-Kind of S <> {}; then dom p c= dom the Object-Kind of S by AMI_1:25; hence dom p c= the carrier of S by FUNCT_2:def 1; end; theorem for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for p being programmed FinPartState of S for s being State of S st p c= s for k holds p c= (Computation s).k proof let S be steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N); let p be programmed FinPartState of S, s be State of S such that A1: p c= s; let k; dom s = the carrier of S by Th36 .= dom((Computation s).k) by Th36; then A2: dom p c= dom((Computation s).k) by A1,GRFUNC_1:8; A3: dom p c= the Instruction-Locations of S by Def13; now let x be set; assume A4: x in dom p; then s.x = ((Computation s).k).x by A3,AMI_1:54; hence p.x = ((Computation s).k).x by A1,A4,GRFUNC_1:8; end; hence p c= (Computation s).k by A2,GRFUNC_1:8; end; definition let N; let S be IC-Ins-separated (non empty non void AMI-Struct over N); let s be State of S, l be Instruction-Location of S; pred s starts_at l means IC s = l; end; definition let N; let S be IC-Ins-separated halting (non empty non void AMI-Struct over N); let s be State of S, l be Instruction-Location of S; pred s halts_at l means :Def15: s.l = halt S; end; theorem Th39: for S being non void AMI-Struct over N, p being FinPartState of S ex s being State of S st p c= s proof let S be non void AMI-Struct over N, p be FinPartState of S; consider h being State of S; sproduct the Object-Kind of S <> {}; then reconsider s = h +* p as State of S by AMI_1:29; take s; thus p c= s by FUNCT_4:26; end; definition let N; let S be definite IC-Ins-separated (non empty non void AMI-Struct over N); let p be FinPartState of S such that A1: IC S in dom p; func IC p -> Instruction-Location of S equals :Def16: p.IC S; coherence proof consider s being State of S such that A2: p c= s by Th39; IC s is Instruction-Location of S; then s.IC S is Instruction-Location of S by AMI_1:def 15; hence thesis by A1,A2,GRFUNC_1:8; end; end; definition let N; let S be definite IC-Ins-separated (non empty non void AMI-Struct over N); let p be FinPartState of S, l be Instruction-Location of S; pred p starts_at l means IC S in dom p & IC p = l; end; definition let N; let S be definite IC-Ins-separated halting (non empty non void AMI-Struct over N); let p be FinPartState of S, l be Instruction-Location of S; pred p halts_at l means l in dom p & p.l = halt S; end; theorem Th40: for S being IC-Ins-separated definite steady-programmed halting (non empty non void AMI-Struct over N), s being State of S holds s is halting iff ex k st s halts_at IC (Computation s).k proof let S be IC-Ins-separated definite steady-programmed halting (non empty non void AMI-Struct over N); let s be State of S; hereby assume s is halting; then consider k such that A1: CurInstr((Computation s).k) = halt S by AMI_1:def 20; take k; s.IC (Computation s).k = (Computation s).k.IC ((Computation s).k) by AMI_1:54 .= halt S by A1,AMI_1:def 17; hence s halts_at IC (Computation s).k by Def15; end; given k such that A2: s halts_at IC (Computation s).k; take k; thus CurInstr((Computation s).k) = (Computation s).k.IC ((Computation s).k) by AMI_1:def 17 .= s.IC (Computation s).k by AMI_1:54 .= halt S by A2,Def15; end; theorem for S being IC-Ins-separated definite steady-programmed halting (non empty non void AMI-Struct over N), s being State of S, p being FinPartState of S, l being Instruction-Location of S st p c= s & p halts_at l holds s halts_at l proof let S be IC-Ins-separated definite steady-programmed halting (non empty non void AMI-Struct over N); let s be State of S, p be FinPartState of S, l be Instruction-Location of S such that A1: p c= s; assume l in dom p & p.l = halt S; hence s.l = halt S by A1,GRFUNC_1:8; end; theorem Th42: for S being halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of S, k st s is halting holds Result s = (Computation s).k iff s halts_at IC (Computation s).k proof let S be halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S, k such that A1: s is halting; hereby assume Result s = (Computation s).k; then ex i st (Computation s).k = (Computation s).i & CurInstr((Computation s).k) = halt S by A1,AMI_1:def 22; then (Computation s).k.IC (Computation s).k = halt S by AMI_1:def 17; then s.IC (Computation s).k = halt S by AMI_1:54; hence s halts_at IC (Computation s).k by Def15; end; assume s.IC (Computation s).k = halt S; then (Computation s).k.IC (Computation s).k = halt S by AMI_1:54; then CurInstr((Computation s).k) = halt S by AMI_1:def 17; hence Result s = (Computation s).k by A1,AMI_1:def 22; end; theorem for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of S, p being programmed FinPartState of S, k holds p c= s iff p c= (Computation s).k proof let S be steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S, p be programmed FinPartState of S, k; dom s = the carrier of S & dom((Computation s).k) = the carrier of S by Th36 ; then A1: dom p c= dom s & dom p c= dom((Computation s).k) by Th37; A2: dom p c= the Instruction-Locations of S by Def13; now hereby assume A3: for x being set st x in dom p holds p.x = s.x; let x be set; assume A4: x in dom p; hence (Computation s).k.x = s.x by A2,AMI_1:54 .= p.x by A3,A4; end; assume A5: for x being set st x in dom p holds p.x = (Computation s).k.x; let x be set; assume A6: x in dom p; hence s.x = (Computation s).k.x by A2,AMI_1:54 .= p.x by A5,A6; end; hence p c= s iff p c= (Computation s).k by A1,GRFUNC_1:8; end; theorem Th44: for S being halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of S, k st s halts_at IC (Computation s).k holds Result s = (Computation s).k proof let S be halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), s be State of S, k; assume A1: s halts_at IC (Computation s).k; then s is halting by Th40; hence Result s = (Computation s).k by A1,Th42; end; theorem Th45: i <= j implies for S being halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S st s halts_at IC (Computation s).i holds s halts_at IC (Computation s).j proof assume A1: i <= j; let S be halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S; assume A2: s.IC (Computation s).i = halt S; CurInstr((Computation s).i) = (Computation s).i.IC (Computation s).i by AMI_1:def 17 .= halt S by A2,AMI_1:54; hence s.IC (Computation s).j = halt S by A1,A2,AMI_1:52; end; theorem :: AMI_1:46 i <= j implies for S being halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S st s halts_at IC (Computation s).i holds (Computation s).j = (Computation s).i proof assume A1: i <= j; let S be halting steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), s be State of S; assume A2: s halts_at IC (Computation s).i; then s halts_at IC (Computation s).j by A1,Th45; hence (Computation s).j = Result s by Th44 .= (Computation s).i by A2,Th44; end; theorem :: AMI_2:46 for S being steady-programmed IC-Ins-separated halting definite (non empty non void AMI-Struct over N) for s being State of S st ex k st s halts_at IC (Computation s).k for i holds Result s = Result (Computation s).i proof let S be steady-programmed IC-Ins-separated halting definite (non empty non void AMI-Struct over N), s be State of S; given k such that A1: s halts_at IC (Computation s).k; let i; s.IC (Computation s).k = halt S by A1,Def15; hence Result s = Result (Computation s).i by AMI_1:57; end; theorem for S being steady-programmed IC-Ins-separated definite halting (non empty non void AMI-Struct over N) for s being State of S,l being Instruction-Location of S,k holds s halts_at l iff (Computation s).k halts_at l proof let S be steady-programmed IC-Ins-separated definite halting (non empty non void AMI-Struct over N), s be State of S, l be Instruction-Location of S,k; hereby assume s halts_at l; then s.l = halt S by Def15; then (Computation s).k.l = halt S by AMI_1:54; hence (Computation s).k halts_at l by Def15; end; assume (Computation s).k.l = halt S; hence s.l = halt S by AMI_1:54; end; theorem for S being definite IC-Ins-separated (non empty non void AMI-Struct over N) , p being FinPartState of S, l being Instruction-Location of S st p starts_at l for s being State of S st p c= s holds s starts_at l proof let S be definite IC-Ins-separated (non empty non void AMI-Struct over N), p be FinPartState of S, l be Instruction-Location of S such that A1: IC S in dom p & IC p = l; let s be State of S such that A2: p c= s; thus IC s = s.IC S by AMI_1:def 15 .= p.IC S by A1,A2,GRFUNC_1:8 .= l by A1,Def16; end; theorem for S being IC-Ins-separated definite (non empty non void AMI-Struct over N) , l being Instruction-Location of S holds (Start-At l).IC S = l proof let S be IC-Ins-separated definite (non empty non void AMI-Struct over N), l be Instruction-Location of S; thus (Start-At l).IC S = (IC S .--> l).IC S by Def12 .= l by CQC_LANG:6; end; definition let N; let S be definite IC-Ins-separated (non empty non void AMI-Struct over N); let l be Instruction-Location of S, I be Element of the Instructions of S; redefine func l .--> I -> programmed FinPartState of S; coherence proof ObjectKind l = the Instructions of S by AMI_1:def 14; then reconsider L = l .--> I as FinPartState of S by AMI_1:59; dom L = {l} by CQC_LANG:5; then dom L c= the Instruction-Locations of S by ZFMISC_1:37; hence thesis by Def13; end; end; begin :: Small concrete model Lm14: for s being State of SCM, i being Instruction of SCM, l being Instruction-Location of SCM holds Exec(i,s).l = s.l proof let s be State of SCM, i be Instruction of SCM, l be Instruction-Location of SCM; reconsider c = i as Element of SCM-Instr by Def1; c in { [SCM-Halt,{}] } \/ { [Y,<*a2*>] : Y = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } or c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} } by AMI_2:def 4,XBOOLE_0:def 2; then A1: c in { [SCM-Halt,{}] } \/ { [Y,<*a2*>] : Y = 6 } or c in { [K,<*a1,b1*>] : K in { 7,8 } } or c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} } by XBOOLE_0:def 2; reconsider S = s as Element of product SCM-OK by Def1; reconsider l' = l as Element of SCM-Instr-Loc by Def1; A2: Exec(i,s) = SCM-Exec.c.S by Def1,AMI_1:def 7 .= SCM-Exec-Res(c,S) by AMI_2:def 17; now per cases by A1,XBOOLE_0:def 2; case c in { [SCM-Halt,{}] }; then c = [SCM-Halt,{}] by TARSKI:def 1; then A3: c`2 = {} by MCART_1:7; A4: now let l be Nat; let mk, ml be Element of SCM-Data-Loc; assume c = [ l, <*mk, ml*>]; then c`2 = <*mk, ml*> by MCART_1:7; hence contradiction by A3,FINSEQ_3:38; end; A5: now let l be Nat; let mk be Element of SCM-Instr-Loc; assume c = [ l, <*mk*>]; then c`2 = <*mk*> by MCART_1:7; hence contradiction by A3,TREES_1:4; end; now let l be Nat; let mk be Element of SCM-Instr-Loc, ml be Element of SCM-Data-Loc; assume c = [ l, <*mk, ml*>]; then c`2 = <*mk, ml*> by MCART_1:7; hence contradiction by A3,FINSEQ_3:38; end; 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, ml being Element of SCM-Data-Loc st c = [ 5, <*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-Instr-Loc, ml being Element of SCM-Data-Loc st c = [ 8, <*mk,ml*>]) by A4,A5; hence SCM-Exec-Res(c,S).l' = S.l' by AMI_2:def 16; case c in { [Y,<*a2*>] : Y = 6 }; then consider Y,a2 such that A6: c = [Y,<*a2*>] & Y = 6; thus SCM-Exec-Res(c,S).l' = SCM-Chg(S,c jump_address).l' by A6,AMI_2:def 16 .= S.l' by AMI_2:18; case c in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A7: c = [K,<*a1,b1*>] & K in { 7,8 }; now per cases by A7,TARSKI:def 2; case K=7; hence SCM-Exec-Res(c,S).l' = SCM-Chg(S,IFEQ(S.(c cond_address),0,c cjump_address,Next IC S)).l' by A7,AMI_2:def 16 .= S.l' by AMI_2:18; case K=8; hence SCM-Exec-Res(c,S).l' = SCM-Chg(S,IFGT(S.(c cond_address),0,c cjump_address,Next IC S)).l' by A7,AMI_2:def 16 .= S.l' by AMI_2:18; end; hence SCM-Exec-Res(c,S).l' = S.l'; case c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} }; then consider T,b2,c1 such that A8: c = [T,<*b2,c1*>] & T in { 1,2,3,4,5}; now per cases by A8,ENUMSET1:23; case T = 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 A8,AMI_2:def 16 .= SCM-Chg(S, c address_1,S.(c address_2)).l' by AMI_2:18 .= S.l' by AMI_2:22; case T = 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 A8,AMI_2:def 16 .= SCM-Chg(S,c address_1,S.(c address_1)+S.(c address_2)).l' by AMI_2:18 .= S.l' by AMI_2:22; case T = 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 A8,AMI_2:def 16 .= SCM-Chg(S,c address_1,S.(c address_1)-S.(c address_2)).l' by AMI_2:18 .= S.l' by AMI_2:22; case T = 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 A8,AMI_2:def 16 .= SCM-Chg(S,c address_1,S.(c address_1)*S.(c address_2)).l' by AMI_2:18 .= S.l' by AMI_2:22; case T = 5; hence SCM-Exec-Res(c,S).l' = SCM-Chg(SCM-Chg( SCM-Chg(S,c address_1,S.(c address_1) div S.(c address_2)), c address_2,S.(c address_1) mod S.(c address_2)),Next IC S).l' by A8,AMI_2:def 16 .= SCM-Chg( SCM-Chg(S,c address_1,S.(c address_1) div S.(c address_2)), c address_2,S.(c address_1) mod S.(c address_2)).l' by AMI_2:18 .= SCM-Chg(S,c address_1,S.(c address_1) div S.(c address_2)).l' by AMI_2:22 .= S.l' by AMI_2:22; end; hence SCM-Exec-Res(c,S).l' = S.l'; end; hence s.l = Exec(i,s).l by A2; end; theorem SCM is realistic by Def1,AMI_1:def 21,AMI_2:6; definition cluster SCM -> steady-programmed realistic; coherence proof SCM is steady-programmed proof let s be State of SCM, i be Instruction of SCM, l be Instruction-Location of SCM; thus Exec(i,s).l = s.l by Lm14; end; hence thesis by Def1,AMI_1:def 21,AMI_2:6; end; end; definition let k be natural number; func dl.k -> Data-Location equals :Def19: 2*k +1; coherence proof reconsider k as Nat by ORDINAL2:def 21; reconsider d = 2*k+1 as Object of SCM by Def1; 2*k +1 in SCM-Data-Loc by AMI_2:def 2; then d is Data-Location by Def2; hence thesis; end; func il.k -> Instruction-Location of SCM equals :Def20: 2*k +2; coherence proof reconsider k as Nat by ORDINAL2:def 21; SCM-Instr-Loc = { 2*i : i > 0 } & k+1 > 0 by AMI_2:def 3,NAT_1:19; then 2*(k +1) in SCM-Instr-Loc; then 2*k +2*1 in SCM-Instr-Loc by XCMPLX_1:8; hence thesis by Def1; end; end; reserve i,j,k for natural number; theorem i <> j implies dl.i <> dl.j proof A1: dl.j = 2*j +1 & dl.i = 2*i + 1 by Def19; assume i <> j; then 2*i <> 2*j by XCMPLX_1:5; hence dl.i <> dl.j by A1,XCMPLX_1:2; end; theorem i <> j implies il.i <> il.j proof A1: il.j = 2*j +2 & il.i = 2*i + 2 by Def20; assume i <> j; then 2*i <> 2*j by XCMPLX_1:5; hence il.i <> il.j by A1,XCMPLX_1:2; end; theorem Next il.k = il.(k+1) proof reconsider loc = il.k as Element of SCM-Instr-Loc by Def1; thus Next il.k = Next loc by Th6 .= loc +2 by AMI_2:def 15 .= 2*k+2*1 +2 by Def20 .= 2*(k+1)+2 by XCMPLX_1:8 .= il.(k+1) by Def20; end; theorem Th55: for l being Data-Location holds ObjectKind l = INT proof let l be Data-Location; A1: l in SCM-Data-Loc by Def2; thus ObjectKind l = (the Object-Kind of SCM).l by AMI_1:def 6 .= INT by A1,Def1,AMI_2:10; end; definition let la be Data-Location; let a be Integer; redefine func la .--> a -> FinPartState of SCM; coherence proof a is Element of INT & ObjectKind la = INT by Th55,INT_1:def 2; hence thesis by AMI_1:59; end; end; definition let la,lb be Data-Location; let a, b be Integer; redefine func (la,lb) --> (a,b) -> FinPartState of SCM; coherence proof a is Element of INT & b is Element of INT & ObjectKind la = INT & ObjectKind lb = INT by Th55,INT_1:def 2; hence thesis by AMI_1:58; end; end; theorem dl.i <> il.j proof A1: il.j = 2*j +2 & dl.i = 2*i + 1 by Def19,Def20; now assume 2*j + 2, 2*i + 1 are_congruent_mod 2; then 2*j, 1 + 2*i are_congruent_mod 2 by INT_1:42; then 1 + 2*i, 2*j are_congruent_mod 2 by INT_1:35; then 1, 2*j - 2*i are_congruent_mod 2 by INT_1:40; then A2: 1, 2*(j - i) are_congruent_mod 2 by XCMPLX_1:40; 2*(j - i), 0 are_congruent_mod 2 by Th18; then 1, 0 are_congruent_mod 2 by A2,INT_1:36; then consider k being Integer such that A3: 2*k = 1 - 0 by INT_1:def 3; thus contradiction by A3,INT_1:22; end; hence dl.i <> il.j by A1,INT_1:32; end; theorem IC SCM <> dl.i & IC SCM <> il.i proof hereby assume IC SCM = dl.i; then 0 = 2*i + 1 by Def19,Th4; hence contradiction; end; assume IC SCM = il.i; then 0 = 2*i + (1 + 1) by Def20,Th4 .= 2*i + 1 + 1 by XCMPLX_1:1; hence contradiction; end; begin :: Halt Instruction theorem for I being Instruction of SCM st ex s st Exec(I,s).IC SCM = Next IC s holds I is non halting by Lm1; theorem for I being Instruction of SCM st I = [0,{}] holds I is halting by Lm2; theorem a := b is non halting by Lm3; theorem AddTo(a,b) is non halting by Lm4; theorem SubFrom(a,b) is non halting by Lm5; theorem MultBy(a,b) is non halting by Lm6; theorem Divide(a,b) is non halting by Lm7; theorem goto loc is non halting by Lm8; theorem a=0_goto loc is non halting by Lm9; theorem a>0_goto loc is non halting by Lm10; theorem [0,{}] is Instruction of SCM by Def1,AMI_2:2; theorem for I being set holds I is Instruction of SCM 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 a,b st I = Divide(a,b)) or (ex loc st I = goto loc) or (ex a,loc st I = a=0_goto loc) or ex a,loc st I = a>0_goto loc by Lm11; theorem for I being Instruction of SCM st I is halting holds I = halt SCM by Lm12; theorem halt SCM = [0,{}] by Lm13;