### The Mizar article:

### On a Mathematical Model of Programs

**by****Yatsuka Nakamura, and****Andrzej Trybulec**

- Received December 29, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: AMI_2
- [ MML identifier index ]

environ vocabulary GR_CY_1, TARSKI, INT_1, BOOLE, FINSEQ_1, NAT_1, FUNCT_1, CARD_3, RELAT_1, AMI_1, FUNCT_4, CAT_1, MCART_1, ARYTM_1, CQC_LANG, FUNCT_2, FUNCT_5, AMI_2, FINSEQ_4, ARYTM; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, CARD_3, RELAT_1, FUNCT_1, FUNCT_2, GR_CY_1, DOMAIN_1, INT_1, NAT_1, CQC_LANG, FRAENKEL, FUNCT_4, CAT_2, FINSEQ_1, FINSEQ_4; constructors GR_CY_1, DOMAIN_1, NAT_1, CAT_2, FINSEQ_4, AMI_1, MEMBERED, XBOOLE_0; clusters SUBSET_1, INT_1, AMI_1, FINSEQ_1, CQC_LANG, RELSET_1, XBOOLE_0, NAT_1, FRAENKEL, MEMBERED, ZFMISC_1, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions TARSKI; theorems ZFMISC_1, FUNCT_2, TARSKI, NAT_1, CAT_2, CQC_LANG, GR_CY_1, SCHEME1, ENUMSET1, INT_1, CARD_3, FINSEQ_1, FINSEQ_4, MCART_1, FUNCT_4, AMI_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes FUNCT_2; begin :: A small concrete machine reserve x for set; reserve i,j,k for Nat; definition func SCM-Halt -> Element of Segm 9 equals :Def1: 0; correctness by GR_CY_1:12; end; definition func SCM-Data-Loc -> Subset of NAT equals :Def2: { 2*k + 1: not contradiction }; coherence proof { 2*k + 1: not contradiction } c= NAT proof let x be set; assume x in { 2*k + 1: not contradiction }; then ex k st x = 2*k+1; hence x in NAT; end; hence thesis; end; func SCM-Instr-Loc -> Subset of NAT equals :Def3: { 2*k : k > 0 }; coherence proof { 2*k : k > 0 } c= NAT proof let x be set; assume x in { 2*k : k > 0 }; then ex k st x = 2*k & k > 0; hence x in NAT; end; hence thesis; end; end; definition cluster SCM-Data-Loc -> non empty; coherence proof 2*0+1 in { 2*k + 1: not contradiction }; hence thesis by Def2; end; cluster SCM-Instr-Loc -> non empty; coherence proof 2*1 in { 2*k:k > 0 }; hence thesis by Def3; end; end; reserve I,J,K for Element of Segm 9, a,a1,a2 for Element of SCM-Instr-Loc, b,b1,b2,c,c1 for Element of SCM-Data-Loc; definition func SCM-Instr -> Subset of [: Segm 9, (union {INT} \/ NAT)* :] equals :Def4: { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } \/ { [I,<*b,c*>] : I in { 1,2,3,4,5} }; coherence proof A1: NAT c= union { INT } \/ NAT by XBOOLE_1:7; A2: { [I,<*b,c*>] : I in { 1,2,3,4,5} } c= [: Segm 9, (union {INT} \/ NAT)* :] proof let x be set; assume x in { [I,<*b,c*>] : I in { 1,2,3,4,5} }; then consider I,b,c such that A3: x = [I,<*b,c*>] & I in { 1,2,3,4,5}; reconsider b, c as Element of union {INT} \/ NAT by A1,TARSKI:def 3; <*b,c*> in (union {INT} \/ NAT)* by FINSEQ_1:def 11; hence x in [: Segm 9, (union {INT} \/ NAT)* :] by A3,ZFMISC_1:106; end; A4: { [J,<*a*>] : J = 6 } c= [: Segm 9, (union {INT} \/ NAT)* :] proof let x be set; assume x in { [J,<*a*>] : J = 6 }; then consider J,a such that A5: x = [J,<*a*>] & J = 6; reconsider a as Element of union {INT} \/ NAT by A1,TARSKI:def 3; <*a*> in (union {INT} \/ NAT)* by FINSEQ_1:def 11; hence x in [: Segm 9, (union {INT} \/ NAT)* :] by A5,ZFMISC_1:106; end; A6: { [K,<*a1,b1*>] : K in { 7,8 } } c= [: Segm 9, (union {INT} \/ NAT)* :] proof let x be set; assume x in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A7: x = [K,<*a1,b1*>] & K in { 7,8 }; reconsider b1,a1 as Element of union {INT} \/ NAT by A1,TARSKI:def 3; <*a1,b1*> in (union {INT} \/ NAT)* by FINSEQ_1:def 11; hence x in [: Segm 9, (union {INT} \/ NAT)* :] by A7,ZFMISC_1:106; end; SCM-Halt in Segm(9) & {} in (union {INT} \/ NAT)* by FINSEQ_1:66; then [SCM-Halt,{}] in [: Segm 9, (union {INT} \/ NAT)* :] by ZFMISC_1:106; then { [SCM-Halt,{}] }c= [: Segm 9, (union {INT} \/ NAT)* :] by ZFMISC_1:37; then { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } c= [: Segm 9, (union {INT} \/ NAT)* :] by A4,XBOOLE_1:8; then { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } c= [: Segm 9, (union {INT} \/ NAT)* :] by A6,XBOOLE_1:8; hence thesis by A2,XBOOLE_1:8; end; end; canceled; theorem Th2: [0,{}] in SCM-Instr proof [0,{}] in { [SCM-Halt,{}] } by Def1,TARSKI:def 1; then [0,{}] in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by XBOOLE_0:def 2; then [0,{}] in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by XBOOLE_0:def 2; hence [0,{}] in SCM-Instr by Def4,XBOOLE_0:def 2; end; definition cluster SCM-Instr -> non empty; coherence by Th2; end; theorem [6,<*a2*>] in SCM-Instr proof reconsider x = 6 as Element of Segm 9 by GR_CY_1:10; [x,<*a2*>] in { [J,<*a*>] : J = 6 }; then [x,<*a2*>] in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by XBOOLE_0:def 2; then [x,<*a2*>] in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by XBOOLE_0:def 2; hence thesis by Def4,XBOOLE_0:def 2; end; theorem x in { 7, 8 } implies [x,<*a2,b2*>] in SCM-Instr proof assume A1: x in { 7, 8 }; then (x = 7 or x = 8) & 9 > 0 & 7 < 9 & 8 < 9 by TARSKI:def 2; then reconsider x as Element of Segm 9 by GR_CY_1:10; [x,<*a2,b2*>] in { [K,<*a1,b1*>] : K in { 7,8 } } by A1; then [x,<*a2,b2*>] in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by XBOOLE_0:def 2; hence thesis by Def4,XBOOLE_0:def 2; end; theorem x in { 1,2,3,4,5} implies [x,<*b1,c1*>] in SCM-Instr proof assume A1: x in { 1,2,3,4,5}; then x=1 or x=2 or x=3 or x=4 or x=5 by ENUMSET1:23; then reconsider x as Element of Segm 9 by GR_CY_1:10; [x,<*b1,c1*>] in { [J,<*b,c*>] : J in { 1,2,3,4,5 } } by A1; hence thesis by Def4,XBOOLE_0:def 2; end; Lm1: now let k; consider i such that A1: k = 2*i or k = 2*i+1 by SCHEME1:1; now assume A2: k = 2*i; A3: i = 0 or ex j st i = j + 1 by NAT_1:22; now given j such that A4: i = j + 1; take j; thus k = 2*j + 2*1 by A2,A4,XCMPLX_1:8; end; hence k = 0 or ex j st k = 2*j+2 by A2,A3; end; hence k= 0 or (ex j st k = 2*j+1) or (ex j st k = 2*j+2) by A1; end; Lm2: now let k; thus (ex j st k = 2*j+1) implies k<>0 ¬ (ex j st k = 2*j+2) proof given j such that A1: k = 2*j+1; thus k<>0 by A1; given i such that A2: k = 2*i+2; A3: (2*i+2*1) = 2*(i+1) + 0 by XCMPLX_1:8; 1 = (2*i+2) mod 2 by A1,A2,NAT_1:def 2 .= 0 by A3,NAT_1:def 2; hence thesis; end; given j such that A4: k = 2*j+(1+1); thus k<>0 by A4; given i such that A5: k = 2*i+1; A6: (2*j+2*1) = 2*(j+1) + 0 by XCMPLX_1:8; 1 = (2*j+2) mod 2 by A4,A5,NAT_1:def 2 .= 0 by A6,NAT_1:def 2; hence contradiction; end; definition func SCM-OK -> Function of NAT, {INT} \/ { SCM-Instr, SCM-Instr-Loc } means :Def5: it.0 = SCM-Instr-Loc & for k being Nat holds it.(2*k+1) = INT & it.(2*k+2) = SCM-Instr; existence proof defpred P[set,set] means ($1 = 0 & $2 = SCM-Instr-Loc)or ((ex j st $1 = 2*j+1) & $2 = INT)or ((ex j st $1 = 2*j+2) & $2 = SCM-Instr); A1: now let k be Nat; {INT} \/ { SCM-Instr, SCM-Instr-Loc } = {INT, SCM-Instr, SCM-Instr-Loc } by ENUMSET1:42; then A2: INT in {INT} \/ { SCM-Instr, SCM-Instr-Loc } & SCM-Instrin {INT} \/ { SCM-Instr, SCM-Instr-Loc } & SCM-Instr-Loc in {INT} \/ { SCM-Instr, SCM-Instr-Loc } by ENUMSET1:14; P[k,SCM-Instr-Loc] or P[k,INT] or P[k,SCM-Instr]by Lm1; hence ex b being Element of {INT} \/ { SCM-Instr, SCM-Instr-Loc } st P[k,b] by A2; end; consider h being Function of NAT, {INT} \/ { SCM-Instr, SCM-Instr-Loc } such that A3: for a being Element of NAT holds P[a,h.a] from FuncExD(A1); take h; P[0,h.0] by A3; hence h.0 = SCM-Instr-Loc; let k be Nat; P[2*k+1,h.(2*k+1)] & P[2*k+2,h.(2*k+2)] by A3; hence h.(2*k+1) = INT & h.(2*k+2) = SCM-Instr by Lm2; end; uniqueness proof let f,g be Function of NAT, {INT} \/ { SCM-Instr, SCM-Instr-Loc } such that A4: f.0 = SCM-Instr-Loc & for k being Nat holds f.(2*k+1) = INT & f.(2*k+2) = SCM-Instr and A5: g.0 = SCM-Instr-Loc & for k being Nat holds g.(2*k+1) = INT & g.(2*k+2) = SCM-Instr; now let k be Nat; now per cases by Lm1; suppose k = 0; hence f.k = g.k by A4,A5; suppose A6:ex i st k = 2*i+1; hence f.k = INT by A4 .= g.k by A5,A6; suppose A7:ex i st k = 2*i+2; hence f.k = SCM-Instr by A4 .= g.k by A5,A7; end; hence f.k = g.k; end; hence thesis by FUNCT_2:113; end; end; theorem Th6: SCM-Instr-Loc <> INT & SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr proof thus SCM-Instr-Loc <> INT by AMI_1:1,INT_1:14,XBOOLE_0:def 10; A1: 2*1 in { 2*k : k > 0 }; now assume 2 in SCM-Instr; then 2 in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } or 2 in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by Def4,XBOOLE_0:def 2; then 2 in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } or 2 in { [K,<*a1,b1*>] : K in { 7,8 } } or 2 in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then 2 in { [SCM-Halt,{}] } or 2 in { [J,<*a*>] : J = 6 } or 2 in { [K,<*a1,b1*>] : K in { 7,8 } } or 2 in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then 2 = [SCM-Halt,{}] or (ex J,a st 2 = [J,<*a*>] & J = 6) or (ex K,a1,b1 st 2 = [K,<*a1,b1*>] & K in { 7,8 }) or (ex I,b,c st 2 = [I,<*b,c*>] & I in { 1,2,3,4,5}) by TARSKI:def 1; hence contradiction by AMI_1:3; end; hence SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr by A1,Def3,INT_1:12; end; theorem Th7: SCM-OK.i = SCM-Instr-Loc iff i = 0 proof thus SCM-OK.i = SCM-Instr-Loc implies i = 0 proof assume A1: SCM-OK.i = SCM-Instr-Loc; assume i <> 0; then (ex j st i = 2*j+1) or (ex j st i = 2*j+2) by Lm1; hence contradiction by A1,Def5,Th6; end; thus thesis by Def5; end; theorem Th8: SCM-OK.i = INT iff ex k st i = 2*k+1 proof thus SCM-OK.i = INT implies ex k st i = 2*k+1 proof assume A1: SCM-OK.i = INT; assume not ex k st i = 2*k+1; then i = 0 or (ex j st i = 2*j+2) by Lm1; hence contradiction by A1,Def5,Th6; end; thus thesis by Def5; end; theorem Th9: SCM-OK.i = SCM-Instr iff ex k st i = 2*k+2 proof thus SCM-OK.i = SCM-Instr implies ex k st i = 2*k+2 proof assume A1: SCM-OK.i = SCM-Instr; assume not ex k st i = 2*k+2; then i = 0 or (ex j st i = 2*j+1) by Lm1; hence contradiction by A1,Def5,Th6; end; thus thesis by Def5; end; definition mode SCM-State is Element of product SCM-OK; end; theorem Th10: for a being Element of SCM-Data-Loc holds SCM-OK.a = INT proof let a be Element of SCM-Data-Loc; a in { 2*k + 1: not contradiction } by Def2; then ex k st a = 2*k+1; hence SCM-OK.a = INT by Th8; end; theorem Th11: for a being Element of SCM-Instr-Loc holds SCM-OK.a = SCM-Instr proof let a be Element of SCM-Instr-Loc; a in { 2*k : k > 0 } by Def3; then consider k such that A1: a = 2*k & k > 0; consider j such that A2: k = j+1 by A1,NAT_1:22; a = 2*j + 2*1 by A1,A2,XCMPLX_1:8; hence SCM-OK.a = SCM-Instr by Th9; end; theorem for a being Element of SCM-Instr-Loc, t being Element of SCM-Data-Loc holds a <> t proof let a be Element of SCM-Instr-Loc, t be Element of SCM-Data-Loc; SCM-OK.a = SCM-Instr & SCM-OK.t = INT by Th10,Th11; hence a <> t by Th6; end; theorem Th13: pi(product SCM-OK,0) = SCM-Instr-Loc proof dom SCM-OK = NAT by FUNCT_2:def 1; hence pi(product SCM-OK,0) = SCM-OK.0 by CARD_3:22 .= SCM-Instr-Loc by Th7; end; theorem Th14: for a being Element of SCM-Data-Loc holds pi(product SCM-OK,a) = INT proof let a be Element of SCM-Data-Loc; dom SCM-OK = NAT by FUNCT_2:def 1; hence pi(product SCM-OK,a) = SCM-OK.a by CARD_3:22 .= INT by Th10; end; theorem for a being Element of SCM-Instr-Loc holds pi(product SCM-OK,a) = SCM-Instr proof let a be Element of SCM-Instr-Loc; dom SCM-OK = NAT by FUNCT_2:def 1; hence pi(product SCM-OK,a) = SCM-OK.a by CARD_3:22 .= SCM-Instr by Th11; end; definition let s be SCM-State; func IC(s) -> Element of SCM-Instr-Loc equals s.0; coherence by Th13,CARD_3:def 6; end; definition let s be SCM-State, u be Element of SCM-Instr-Loc; func SCM-Chg(s,u) -> SCM-State equals :Def7: s +* (0 .--> u); coherence proof A1: dom(SCM-OK) = NAT by FUNCT_2:def 1; then dom s = NAT by CARD_3:18; then A2: dom(s +* (0 .--> u)) = NAT \/ dom(0 .--> u) by FUNCT_4:def 1 .= NAT \/ {0} by CQC_LANG:5 .= dom(SCM-OK) by A1,ZFMISC_1:46; now let x be set; assume A3: x in dom(SCM-OK); now per cases; suppose A4: x = 0; {0} = dom(0 .--> u) by CQC_LANG:5; then 0 in dom(0 .--> u) by TARSKI:def 1; then (s +* (0 .--> u)).0 = (0 .--> u).0 by FUNCT_4:14 .= u by CQC_LANG:6; then (s +* (0 .--> u)).0 in SCM-Instr-Loc; hence (s +* (0 .--> u)).x in SCM-OK.x by A4,Th7; suppose A5: x <> 0; {0} = dom(0 .--> u) by CQC_LANG:5; then not x in dom(0 .--> u) by A5,TARSKI:def 1; then (s +* (0 .--> u)).x = s.x by FUNCT_4:12; hence (s +* (0 .--> u)).x in SCM-OK.x by A3,CARD_3:18; end; hence (s +* (0 .--> u)).x in SCM-OK.x; end; hence thesis by A2,CARD_3:18; end; end; theorem for s being SCM-State, u being Element of SCM-Instr-Loc holds SCM-Chg(s,u).0 = u proof let s be SCM-State, u be Element of SCM-Instr-Loc; {0} = dom(0 .--> u) by CQC_LANG:5; then A1: 0 in dom(0 .--> u) by TARSKI:def 1; thus SCM-Chg(s,u).0 = (s +* (0 .--> u)).0 by Def7 .= (0 .--> u).0 by A1,FUNCT_4:14 .= u by CQC_LANG:6; end; theorem for s being SCM-State, u being Element of SCM-Instr-Loc, mk being Element of SCM-Data-Loc holds SCM-Chg(s,u).mk = s.mk proof let s be SCM-State, u be Element of SCM-Instr-Loc, mk be Element of SCM-Data-Loc; A1: SCM-OK.0 = SCM-Instr-Loc & SCM-OK.mk = INT by Th7,Th10; {0} = dom(0 .--> u) by CQC_LANG:5; then A2: not mk in dom(0 .--> u) by A1,Th6,TARSKI:def 1; thus SCM-Chg(s,u).mk = (s +* (0 .--> u)).mk by Def7 .= s.mk by A2,FUNCT_4:12; end; theorem for s being SCM-State, u,v being Element of SCM-Instr-Loc holds SCM-Chg(s,u).v = s.v proof let s be SCM-State, u,v be Element of SCM-Instr-Loc; A1: SCM-OK.0 = SCM-Instr-Loc & SCM-OK.v = SCM-Instr by Th7,Th11; {0} = dom(0 .--> u) by CQC_LANG:5; then A2: not v in dom(0 .--> u) by A1,Th6,TARSKI:def 1; thus SCM-Chg(s,u).v = (s +* (0 .--> u)).v by Def7 .= s.v by A2,FUNCT_4:12; end; definition let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer; func SCM-Chg(s,t,u) -> SCM-State equals :Def8: s +* (t .--> u); coherence proof A1: dom(SCM-OK) = NAT by FUNCT_2:def 1; then dom s = NAT by CARD_3:18; then A2: dom(s +* (t .--> u)) = NAT \/ dom(t .--> u) by FUNCT_4:def 1 .= NAT \/ {t} by CQC_LANG:5 .= dom(SCM-OK) by A1,ZFMISC_1:46; now let x be set; assume A3: x in dom(SCM-OK); now per cases; suppose A4: x = t; {t} = dom(t .--> u) by CQC_LANG:5; then t in dom(t .--> u) by TARSKI:def 1; then (s +* (t .--> u)).t = (t .--> u).t by FUNCT_4:14 .= u by CQC_LANG:6; then (s +* (t .--> u)).t in INT by INT_1:12; hence (s +* (t .--> u)).x in SCM-OK.x by A4,Th10; suppose A5: x <> t; {t} = dom(t .--> u) by CQC_LANG:5; then not x in dom(t .--> u) by A5,TARSKI:def 1; then (s +* (t .--> u)).x = s.x by FUNCT_4:12; hence (s +* (t .--> u)).x in SCM-OK.x by A3,CARD_3:18; end; hence (s +* (t .--> u)).x in SCM-OK.x; end; hence thesis by A2,CARD_3:18; end; end; theorem for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer holds SCM-Chg(s,t,u).0 = s.0 proof let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer; A1: SCM-OK.0 = SCM-Instr-Loc & SCM-OK.t = INT by Th7,Th10; {t} = dom(t .--> u) by CQC_LANG:5; then A2: not 0 in dom(t .--> u) by A1,Th6,TARSKI:def 1; thus SCM-Chg(s,t,u).0 = (s +* (t .--> u)).0 by Def8 .= s.0 by A2,FUNCT_4:12; end; theorem for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer holds SCM-Chg(s,t,u).t = u proof let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer; {t} = dom(t .--> u) by CQC_LANG:5; then A1: t in dom(t .--> u) by TARSKI:def 1; thus SCM-Chg(s,t,u).t = (s +* (t .--> u)).t by Def8 .= (t .--> u).t by A1,FUNCT_4:14 .= u by CQC_LANG:6; end; theorem for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer, mk being Element of SCM-Data-Loc st mk <> t holds SCM-Chg(s,t,u).mk = s.mk proof let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer, mk be Element of SCM-Data-Loc such that A1: mk <> t; {t} = dom(t .--> u) by CQC_LANG:5; then A2: not mk in dom(t .--> u) by A1,TARSKI:def 1; thus SCM-Chg(s,t,u).mk = (s +* (t .--> u)).mk by Def8 .= s.mk by A2,FUNCT_4:12; end; theorem for s being SCM-State, t being Element of SCM-Data-Loc, u being Integer, v being Element of SCM-Instr-Loc holds SCM-Chg(s,t,u).v = s.v proof let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer, v be Element of SCM-Instr-Loc; A1: SCM-OK.v = SCM-Instr & SCM-OK.t = INT by Th10,Th11; {t} = dom(t .--> u) by CQC_LANG:5; then A2: not v in dom(t .--> u) by A1,Th6,TARSKI:def 1; thus SCM-Chg(s,t,u).v = (s +* (t .--> u)).v by Def8 .= s.v by A2,FUNCT_4:12; end; definition let x be Element of SCM-Instr; given mk, ml being Element of SCM-Data-Loc, I such that A1: x = [ I, <*mk, ml*>]; func x address_1 -> Element of SCM-Data-Loc means :Def9: ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.1; existence proof take mk,<*mk, ml*>; thus thesis by A1,FINSEQ_4:26,MCART_1:7; end; uniqueness; func x address_2 -> Element of SCM-Data-Loc means :Def10: ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.2; existence proof take ml,<*mk, ml*>; thus thesis by A1,FINSEQ_4:26,MCART_1:7; end; correctness; end; theorem for x being Element of SCM-Instr, mk, ml being Element of SCM-Data-Loc, I st x = [ I, <*mk, ml*>] holds x address_1 = mk & x address_2 = ml proof let x be Element of SCM-Instr, mk,ml be Element of SCM-Data-Loc, I; assume A1: x = [ I, <*mk,ml*>]; then consider f being FinSequence of SCM-Data-Loc such that A2: f = x`2 & x address_1 = f/.1 by Def9; f = <*mk,ml*> by A1,A2,MCART_1:7; hence x address_1 = mk by A2,FINSEQ_4:26; consider f being FinSequence of SCM-Data-Loc such that A3: f = x`2 & x address_2 = f/.2 by A1,Def10; f = <*mk,ml*> by A1,A3,MCART_1:7; hence x address_2 = ml by A3,FINSEQ_4:26; end; definition let x be Element of SCM-Instr; given mk being Element of SCM-Instr-Loc, I such that A1: x = [ I, <*mk*>]; func x jump_address -> Element of SCM-Instr-Loc means :Def11: ex f being FinSequence of SCM-Instr-Loc st f = x`2 & it = f/.1; existence proof take mk,<*mk*>; thus thesis by A1,FINSEQ_4:25,MCART_1:7; end; correctness; end; theorem for x being Element of SCM-Instr, mk being Element of SCM-Instr-Loc, I st x = [ I, <*mk*>] holds x jump_address = mk proof let x be Element of SCM-Instr, mk be Element of SCM-Instr-Loc, I; assume A1: x = [ I, <*mk*>]; then consider f being FinSequence of SCM-Instr-Loc such that A2: f = x`2 & x jump_address = f/.1 by Def11; f = <*mk*> by A1,A2,MCART_1:7; hence x jump_address = mk by A2,FINSEQ_4:25; end; definition let x be Element of SCM-Instr; given mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc, I such that A1: x = [ I, <*mk,ml*>]; func x cjump_address -> Element of SCM-Instr-Loc means :Def12: ex mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc st <*mk,ml*> = x`2 & it = <*mk,ml*>/.1; existence proof take mk,mk,ml; thus thesis by A1,FINSEQ_4:26,MCART_1:7; end; correctness; func x cond_address -> Element of SCM-Data-Loc means :Def13: ex mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc st <*mk,ml*> = x`2 & it = <*mk,ml*>/.2; existence proof take ml,mk,ml; thus thesis by A1,FINSEQ_4:26,MCART_1:7; end; correctness; end; theorem for x being Element of SCM-Instr, mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc, I st x = [ I, <*mk,ml*>] holds x cjump_address = mk & x cond_address = ml proof let x be Element of SCM-Instr, mk be Element of SCM-Instr-Loc, ml be Element of SCM-Data-Loc, I; assume A1: x = [ I, <*mk,ml*>]; then consider mk' being Element of SCM-Instr-Loc, ml' being Element of SCM-Data-Loc such that A2: <*mk',ml'*> = x`2 & x cjump_address = <*mk',ml'*>/.1 by Def12; <*mk',ml'*> = <*mk,ml*> by A1,A2,MCART_1:7; hence x cjump_address = mk by A2,FINSEQ_4:26; consider mk' being Element of SCM-Instr-Loc, ml' being Element of SCM-Data-Loc such that A3: <*mk',ml'*> = x`2 & x cond_address = <*mk',ml'*>/.2 by A1,Def13; <*mk',ml'*> = <*mk,ml*> by A1,A3,MCART_1:7; hence x cond_address = ml by A3,FINSEQ_4:26; end; definition let s be SCM-State, a be Element of SCM-Data-Loc; cluster s.a -> integer; coherence proof s.a in pi(product SCM-OK,a) by CARD_3:def 6; then s.a in INT by Th14; hence s.a is integer by INT_1:12; end; end; definition let D be non empty set; let x,y be real number, a,b be Element of D; func IFGT(x,y,a,b) -> Element of D equals a if x > y otherwise b; correctness; end; definition let d be Element of SCM-Instr-Loc; func Next d -> Element of SCM-Instr-Loc equals d + 2; coherence proof d in { 2*k : k > 0 } by Def3; then consider k such that A1: d = 2*k and k > 0; 2*k + 2*1 = 2*(k+1) & k+1 >0 by NAT_1:19,XCMPLX_1:8; then d + 2 in { 2*i : i > 0 } by A1; hence thesis by Def3; end; end; definition let x be Element of SCM-Instr, s be SCM-State; func SCM-Exec-Res(x,s) -> SCM-State equals SCM-Chg(SCM-Chg(s, x address_1,s.(x address_2)), Next IC s) if ex mk, ml being Element of SCM-Data-Loc st x = [ 1, <*mk, ml*>], SCM-Chg(SCM-Chg(s,x address_1, s.(x address_1)+s.(x address_2)),Next IC s) if ex mk, ml being Element of SCM-Data-Loc st x = [ 2, <*mk, ml*>], SCM-Chg(SCM-Chg(s,x address_1, s.(x address_1)-s.(x address_2)),Next IC s) if ex mk, ml being Element of SCM-Data-Loc st x = [ 3, <*mk, ml*>], SCM-Chg(SCM-Chg(s,x address_1, s.(x address_1)*s.(x address_2)),Next IC s) if ex mk, ml being Element of SCM-Data-Loc st x = [ 4, <*mk, ml*>], SCM-Chg(SCM-Chg( SCM-Chg(s,x address_1,s.(x address_1) div s.(x address_2)), x address_2,s.(x address_1) mod s.(x address_2)),Next IC s) if ex mk, ml being Element of SCM-Data-Loc st x = [ 5, <*mk, ml*>], SCM-Chg(s,x jump_address) if ex mk being Element of SCM-Instr-Loc st x = [ 6, <*mk*>], SCM-Chg(s,IFEQ(s.(x cond_address),0,x cjump_address,Next IC s)) if ex mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc st x = [ 7, <*mk,ml*>], SCM-Chg(s,IFGT(s.(x cond_address),0,x cjump_address,Next IC s)) if ex mk being Element of SCM-Instr-Loc, ml being Element of SCM-Data-Loc st x = [ 8, <*mk,ml*>] otherwise s; consistency by ZFMISC_1:33; coherence; end; definition func SCM-Exec -> Function of SCM-Instr, Funcs(product SCM-OK, product SCM-OK) means for x being Element of SCM-Instr, y being SCM-State holds (it.x).y = SCM-Exec-Res(x,y); existence proof deffunc F(Element of SCM-Instr, SCM-State) = SCM-Exec-Res($1,$2); consider f being Function of [:SCM-Instr,product SCM-OK:], product SCM-OK such that A1: for x being Element of SCM-Instr, y being SCM-State holds f.[x,y] = F(x,y) from Lambda2D; take curry f; let x be Element of SCM-Instr, y be SCM-State; thus (curry f).x.y = f.[x,y] by CAT_2:3 .= SCM-Exec-Res(x,y) by A1; end; uniqueness proof let f,g be Function of SCM-Instr, Funcs(product SCM-OK, product SCM-OK) such that A2: for x being Element of SCM-Instr, y being SCM-State holds (f.x).y = SCM-Exec-Res(x,y) and A3: for x being Element of SCM-Instr, y being SCM-State holds (g.x).y = SCM-Exec-Res(x,y); now let x be Element of SCM-Instr; reconsider gx=g.x, fx=f.x as Function of product SCM-OK, product SCM-OK; now let y be SCM-State; thus fx.y = SCM-Exec-Res(x,y) by A2 .= gx.y by A3; end; hence f.x = g.x by FUNCT_2:113; end; hence f = g by FUNCT_2:113; end; end;

Back to top