:: On a Mathematical Model of Programs
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 29, 1992
:: Copyright (c) 1992 Association of Mizar Users

environ

 vocabularies 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, ORDINAL2, MEMBERED, MATRIX_2;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
      MEMBERED, ABIAN,
      XCMPLX_0, XREAL_0, CARD_1, CARD_3, RELAT_1, FUNCT_1, FUNCT_2, XXREAL_0,
      BINOP_1, DOMAIN_1, INT_1, NAT_1, NAT_D, FUNCOP_1, FRAENKEL, FUNCT_4,
      CAT_2, FINSEQ_1, FINSEQ_4;
 constructors DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_4, CAT_2, AMI_1,
      MEMBERED, ABIAN, REAL_1;
 registrations XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, RELSET_1, FUNCOP_1,
      ARYTM_3, FRAENKEL, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1,
      CARD_3, AFINSQ_1, MEMBERED, RELAT_1, CARD_4, FINSET_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, FUNCOP_1, CARD_1;
 theorems ZFMISC_1, FUNCT_2, TARSKI, NAT_1, CAT_2, FUNCOP_1, GR_CY_1, SCHEME1,
      ENUMSET1, INT_1, CARD_3, FINSEQ_1, FINSEQ_4, MCART_1, FUNCT_4, AMI_1,
      XBOOLE_0, XBOOLE_1, NUMBERS, ORDINAL1, NAT_D, ABIAN, XREAL_1, RELAT_1,
      ARYTM_3;
 schemes FUNCT_2, BINOP_1, DOMAIN_1;

begin :: A small concrete machine

 reserve x,y,z for set;
 reserve i,j,k for Element of NAT;

notation
 synonym SCM-Halt for {};
end;

definition
 redefine func SCM-Halt -> Element of Segm 9;
 correctness by GR_CY_1:12;
end;

definition
 func SCM-Data-Loc equals
  [:{1},NAT:];
  coherence;
 func SCM-Instr-Loc equals
:::   { 2*k : not contradiction };
   NAT;
  coherence;
end;

definition
 func SCM-Memory equals
  {NAT} \/ SCM-Data-Loc \/ SCM-Instr-Loc;
 coherence;
end;

registration
 cluster SCM-Memory -> non empty;
 coherence;
end;

definition
  redefine func SCM-Data-Loc -> Subset of SCM-Memory;
  coherence
   proof
     SCM-Memory = {NAT} \/ SCM-Instr-Loc \/ SCM-Data-Loc by XBOOLE_1:4;
    hence thesis by XBOOLE_1:7;
   end;
   redefine func SCM-Instr-Loc -> Subset of SCM-Memory;
  coherence by XBOOLE_1:7;
end;

registration
 cluster SCM-Data-Loc -> non empty;
  coherence;
 cluster SCM-Instr-Loc -> non empty;
  coherence;
end;

registration
 cluster -> natural Element of SCM-Instr-Loc;
 coherence
  proof let x be Element of SCM-Instr-Loc;
    ex k st x = k;
   hence thesis;
  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 [: NAT, (union {INT} \/ SCM-Memory)* :] equals
  { [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: SCM-Memory c= union { INT } \/ SCM-Memory by XBOOLE_1:7;
A2: { [I,<*b,c*>] : I in { 1,2,3,4,5} }
     c= [: NAT, (union {INT} \/ SCM-Memory)* :]
     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} \/ SCM-Memory
                 by A1,TARSKI:def 3;
           <*b,c*> in (union {INT} \/ SCM-Memory)* by FINSEQ_1:def 11;
      hence x in [: NAT, (union {INT} \/ SCM-Memory)* :] by A3,ZFMISC_1:106;
     end;
A4: { [J,<*a*>] : J = 6 } c= [: NAT, (union {INT} \/ SCM-Memory)* :]
     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} \/ SCM-Memory
                  by A1,TARSKI:def 3;
           <*a*> in (union {INT} \/ SCM-Memory)* by FINSEQ_1:def 11;
      hence x in [: NAT, (union {INT} \/ SCM-Memory)* :] by A5,ZFMISC_1:106;
     end;
A6: { [K,<*a1,b1*>] : K in { 7,8 } } c= [: NAT, (union {INT} \/ SCM-Memory)* :]
     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} \/ SCM-Memory
               by A1,TARSKI:def 3;
           <*a1,b1*> in (union {INT} \/ SCM-Memory)* by FINSEQ_1:def 11;
      hence x in [: NAT, (union {INT} \/ SCM-Memory)* :] by A7,ZFMISC_1:106;
     end;
    SCM-Halt in Segm(9) & {} in (union {INT} \/ SCM-Memory)* by FINSEQ_1:66;
    then [SCM-Halt,{}] in [: NAT, (union {INT} \/ SCM-Memory)* :]
     by ZFMISC_1:106;
    then { [SCM-Halt,{}] }c= [: NAT, (union {INT} \/ SCM-Memory)* :]
     by ZFMISC_1:37;
    then { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 }
      c= [: NAT, (union {INT} \/ SCM-Memory)* :] by A4,XBOOLE_1:8;
    then { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/
         { [K,<*a1,b1*>] : K in { 7,8 } }
      c= [: NAT, (union {INT} \/ SCM-Memory)* :] by A6,XBOOLE_1:8;
   hence thesis by A2,XBOOLE_1:8;
  end;
end;

canceled;

theorem
  [0,{}] in SCM-Instr
proof
     [0,{}] in { [SCM-Halt,{}] } by 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 XBOOLE_0:def 2;
end;

registration
 cluster SCM-Instr -> non empty;
 coherence;
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 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 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:def 3;
   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 XBOOLE_0:def 2;
 end;

Lm1:
now let k be Element of SCM-Memory;
  k in {NAT} \/ SCM-Data-Loc or k in SCM-Instr-Loc by XBOOLE_0:def 2;
  then k in {NAT} or k in SCM-Data-Loc or k in SCM-Instr-Loc by XBOOLE_0:def 2;
 hence k = NAT or k in SCM-Data-Loc or k in SCM-Instr-Loc by TARSKI:def 1;
end;

Lm27:
 not NAT in SCM-Data-Loc
  proof assume NAT in SCM-Data-Loc;
    then ex x,y st NAT = [x,y] by RELAT_1:def 1;
   hence contradiction;
  end;

Lm29:
 SCM-Data-Loc misses SCM-Instr-Loc
  proof assume SCM-Data-Loc meets SCM-Instr-Loc;
    then consider x such that
W1:  x in SCM-Data-Loc and
W2:  x in SCM-Instr-Loc by XBOOLE_0:3;
    consider y,z such that
W3:  x = [y,z] by W1,RELAT_1:def 1;
    ex k st x = k by W2;
   hence contradiction by W3;
  end;

definition
 func SCM-OK -> Function of SCM-Memory, {INT} \/ { SCM-Instr, SCM-Instr-Loc }
     means
:Def5: for k being Element of SCM-Memory holds
   (k = NAT implies it.k = SCM-Instr-Loc) &
   (k in SCM-Data-Loc implies it.k = INT) &
   (k in SCM-Instr-Loc implies it.k = SCM-Instr);
 existence
  proof
   defpred P[set,set] means
    $1 = NAT & $2 = SCM-Instr-Loc or
    $1 in SCM-Data-Loc & $2 = INT or
    $1 in SCM-Instr-Loc & $2 = SCM-Instr;
A1:  now let k be Element of SCM-Memory;
      {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:def 1;
     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 SCM-Memory, {INT} \/ { SCM-Instr, SCM-Instr-Loc }
    such that
A3:   for a being Element of SCM-Memory holds P[a,h.a] from FUNCT_2:sch 3(A1);
   take h;
   let k be Element of SCM-Memory;
X:  P[k,h.k] by A3;
   thus k = NAT implies h.k = SCM-Instr-Loc by Lm27,X;
   thus k in SCM-Data-Loc implies h.k = INT by Lm27,Lm29,XBOOLE_0:3,X;
   thus k in SCM-Instr-Loc implies h.k = SCM-Instr
         by Lm29,XBOOLE_0:3,X;
  end;
 uniqueness
  proof
   let f,g be Function of SCM-Memory, {INT} \/ { SCM-Instr, SCM-Instr-Loc }
  such that
A4: for k being Element of SCM-Memory holds
   (k = NAT implies f.k = SCM-Instr-Loc) &
   (k in SCM-Data-Loc implies f.k = INT) &
   (k in SCM-Instr-Loc implies f.k = SCM-Instr)
    and
A5: for k being Element of SCM-Memory holds
   (k = NAT implies g.k = SCM-Instr-Loc) &
   (k in SCM-Data-Loc implies g.k = INT) &
   (k in SCM-Instr-Loc implies g.k = SCM-Instr);
        now let k be Element of SCM-Memory;
          now per cases by Lm1;
     suppose
S:    k = NAT;
        hence f.k = SCM-Instr-Loc by A4 .= g.k by A5,S;
       end;
       suppose A6: k in SCM-Data-Loc;
        hence f.k = INT by A4 .= g.k by A5,A6;
       end;
       suppose A7: k in SCM-Instr-Loc;

        hence f.k = SCM-Instr by A4 .= g.k by A5,A7;
      end;
      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
  hereby assume SCM-Instr-Loc = INT;
    then -1 in SCM-Instr-Loc by INT_1:def 1;
    then consider k such that
W:   -1 = k;
    k < 0 by W;
   hence contradiction;
  end;
   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 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;
   end;
  hence SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr
   by INT_1:def 2;
 end;

theorem Th7:
 for i being Element of SCM-Memory
 holds SCM-OK.i = SCM-Instr-Loc iff i = NAT
 proof let i be Element of SCM-Memory;
  thus SCM-OK.i = SCM-Instr-Loc implies i = NAT
   proof assume
A1:  SCM-OK.i = SCM-Instr-Loc;
    assume i <> NAT;
     then i in SCM-Data-Loc or i in SCM-Instr-Loc by Lm1;
    hence contradiction by A1,Def5,Th6;
   end;
  thus thesis by Def5;
 end;

theorem Th8:
 for i being Element of SCM-Memory
 holds SCM-OK.i = INT iff i in SCM-Data-Loc
 proof let i be Element of SCM-Memory;
  thus SCM-OK.i = INT implies i in SCM-Data-Loc
   proof assume
A1:   SCM-OK.i = INT;
    assume not i in SCM-Data-Loc;
     then i = NAT or i in SCM-Instr-Loc by Lm1;
    hence contradiction by A1,Def5,Th6;
   end;
  thus thesis by Def5;
 end;

theorem Th9:
 for i being Element of SCM-Memory
 holds SCM-OK.i = SCM-Instr iff i in SCM-Instr-Loc
 proof let i be Element of SCM-Memory;
  thus SCM-OK.i = SCM-Instr implies i in SCM-Instr-Loc
   proof assume
A1:   SCM-OK.i = SCM-Instr;
    assume not i in SCM-Instr-Loc;
     then i = NAT or i in SCM-Data-Loc 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 by Th8;

theorem Th11:
 for a being Element of SCM-Instr-Loc holds
  SCM-OK.a = SCM-Instr by Th9;

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;

LmX0: NAT in SCM-Memory
proof
 NAT in {NAT} by TARSKI:def 1;
 then NAT in {NAT} \/ SCM-Data-Loc by XBOOLE_0:def 2;
 hence thesis by XBOOLE_0:def 2;
end;

theorem Th13:
 pi(product SCM-OK,NAT) = SCM-Instr-Loc
 proof
   dom SCM-OK = SCM-Memory by FUNCT_2:def 1;
  hence pi(product SCM-OK,NAT) = SCM-OK.NAT by CARD_3:22,LmX0
       .= SCM-Instr-Loc by Th7,LmX0;
 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 = SCM-Memory 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 = SCM-Memory 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.NAT;
 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
   s +* (NAT .--> u);
 coherence
  proof
A1:  dom(SCM-OK) = SCM-Memory by FUNCT_2:def 1;
    then dom s = SCM-Memory by CARD_3:18;
then A2:  dom(s +* (NAT .--> u))
       = SCM-Memory \/ dom(NAT .--> u) by FUNCT_4:def 1
      .= SCM-Memory \/ {NAT} by FUNCOP_1:19
      .= dom(SCM-OK) by A1,ZFMISC_1:46,LmX0;
        now let x be set;
     assume
A3:    x in dom(SCM-OK);
         now per cases;
      suppose
A4:     x = NAT;
        {NAT} = dom(NAT .--> u) by FUNCOP_1:19;
        then NAT in dom(NAT .--> u) by TARSKI:def 1;
        then (s +* (NAT .--> u)).NAT = (NAT .--> u).NAT by FUNCT_4:14
          .= u by FUNCOP_1:87;
        then (s +* (NAT .--> u)).NAT in SCM-Instr-Loc;
       hence (s +* (NAT .--> u)).x in SCM-OK.x by A4,Th7,LmX0;
      end;
      suppose
A5:     x <> NAT;
        {NAT} = dom(NAT .--> u) by FUNCOP_1:19;
        then not x in dom(NAT .--> u) by A5,TARSKI:def 1;
        then (s +* (NAT .--> u)).x = s.x by FUNCT_4:12;
       hence (s +* (NAT .--> u)).x in SCM-OK.x by A3,CARD_3:18;
     end;
     end;
     hence (s +* (NAT .--> 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).NAT = u
 proof let s be SCM-State, u be Element of SCM-Instr-Loc;
      {NAT} = dom(NAT .--> u) by FUNCOP_1:19;
  then NAT in dom(NAT .--> u) by TARSKI:def 1;
  hence SCM-Chg(s,u).NAT = (NAT .--> u).NAT by FUNCT_4:14
    .= u by FUNCOP_1:87;
 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.NAT = SCM-Instr-Loc & SCM-OK.mk = INT by Th7,Th10,LmX0;
      {NAT} = dom(NAT .--> u) by FUNCOP_1:19;
then  not mk in dom(NAT .--> u) by A1,Th6,TARSKI:def 1;
  hence SCM-Chg(s,u).mk = s.mk by 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;
      {NAT} = dom(NAT .--> u) by FUNCOP_1:19;
then not v in dom(NAT .--> u) by TARSKI:def 1;
  hence SCM-Chg(s,u).v = s.v by 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
   s +* (t .--> u);
 coherence
  proof
A1:  dom(SCM-OK) = SCM-Memory by FUNCT_2:def 1;
    then dom s = SCM-Memory by CARD_3:18;
then A2:  dom(s +* (t .--> u)) = SCM-Memory \/ dom(t .--> u) by FUNCT_4:def 1
      .= SCM-Memory \/ {t} by FUNCOP_1:19
      .= 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 FUNCOP_1:19;
        then t in dom(t .--> u) by TARSKI:def 1;
        then (s +* (t .--> u)).t = (t .--> u).t by FUNCT_4:14
          .= u by FUNCOP_1:87;
        then (s +* (t .--> u)).t in INT by INT_1:def 2;
       hence (s +* (t .--> u)).x in SCM-OK.x by A4,Th10;
      end;
      suppose
A5:     x <> t;
            {t} = dom(t .--> u) by FUNCOP_1:19;
        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;
     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).NAT = s.NAT
proof let s be SCM-State, t be Element of SCM-Data-Loc, u be Integer;
A1:  SCM-OK.NAT = SCM-Instr-Loc & SCM-OK.t = INT by Th7,Th10,LmX0;
      {t} = dom(t .--> u) by FUNCOP_1:19;
then  not NAT in dom(t .--> u) by A1,Th6,TARSKI:def 1;
 hence SCM-Chg(s,t,u).NAT = s.NAT by 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 FUNCOP_1:19;
then t in dom(t .--> u) by TARSKI:def 1;
 hence SCM-Chg(s,t,u).t = (t .--> u).t by FUNCT_4:14
   .= u by FUNCOP_1:87;
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 FUNCOP_1:19;
then  not mk in dom(t .--> u) by A1,TARSKI:def 1;
 hence SCM-Chg(s,t,u).mk = s.mk by 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 FUNCOP_1:19;
then  not v in dom(t .--> u) by A1,Th6,TARSKI:def 1;
 hence SCM-Chg(s,t,u).v = s.v by 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;

registration 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:def 2;
  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 + 1;
 coherence
  proof
    consider k such that
A1:   d = k;
    k + 1 = (k+1);
    then d + 1 in NAT by A1;
   hence thesis;
  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
   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) = SCM-Exec-Res(x,y) from BINOP_1:sch 4;
   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;

begin :: Addenda

:: missing, 2007.07.27, A.T.

canceled;

theorem
 not NAT in SCM-Data-Loc by Lm27;

theorem
 not NAT in SCM-Instr-Loc;

theorem
 SCM-Data-Loc misses SCM-Instr-Loc by Lm29;

theorem
 NAT in SCM-Memory by LmX0;

theorem
 SCM-Instr-Loc <> INT by Th6;

theorem
 x in SCM-Data-Loc implies ex k being Element of NAT st x = [1,k]
 proof assume x in SCM-Data-Loc;
   then consider y,z such that
W1: y in {1} and
W2: z in NAT and
W3: x = [y,z] by ZFMISC_1:103;
   reconsider k = z as Element of NAT by W2;
  take k;
   y = 1 by W1, TARSKI:def 1;
  hence x = [1,k] by W3;
 end;

theorem
 for k being natural number holds [1,k] in SCM-Data-Loc
proof let k be natural number;
  1 in {1} & k in NAT by TARSKI:def 1,ORDINAL1:def 13;
 hence [1,k] in SCM-Data-Loc by ZFMISC_1:106;
end;