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

definition
  canceled;
  func SCM-Memory equals

  {NAT} \/ SCM-Data-Loc \/ NAT;
  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} \/ NAT \/ SCM-Data-Loc by XBOOLE_1:4;
    hence thesis by XBOOLE_1:7;
  end;
  redefine func NAT -> Subset of SCM-Memory;
  coherence by XBOOLE_1:7;
end;

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

reserve I,J,K for Element of Segm 9,
  a,a1,a2 for Element of NAT,
  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 NAT by XBOOLE_0:def 2;
  then k in {NAT} or k in SCM-Data-Loc or k in NAT by XBOOLE_0:def 2;
  hence k = NAT or k in SCM-Data-Loc or k in NAT by TARSKI:def 1;
end;

Lm2: 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;

Lm3: SCM-Data-Loc misses NAT
proof
  assume SCM-Data-Loc meets NAT;
  then consider x such that
A1: x in SCM-Data-Loc and
A2: x in NAT by XBOOLE_0:3;
  consider y,z such that
A3: x = [y,z] by A1,RELAT_1:def 1;
  ex k st x = k by A2;
  hence contradiction by A3;
end;

definition
  func SCM-OK -> Function of SCM-Memory, {INT} \/ { SCM-Instr, NAT }
  means
  :Def5:
  for k being Element of SCM-Memory holds
  (k = NAT implies it.k = NAT) &
  (k in SCM-Data-Loc implies it.k = INT) &
  (k in NAT implies it.k = SCM-Instr);
  existence
  proof
    defpred P[set,set] means $1 = NAT & $2 = NAT or
    $1 in SCM-Data-Loc & $2 = INT or $1 in NAT & $2 = SCM-Instr;
A1: now
      let k be Element of SCM-Memory;
      {INT} \/ { SCM-Instr, NAT } = {INT, SCM-Instr, NAT}
      by ENUMSET1:42;
      then
A2:   INT in {INT} \/ { SCM-Instr, NAT } &
      SCM-Instrin {INT} \/ { SCM-Instr, NAT } &
      NAT in {INT} \/ { SCM-Instr, NAT } by ENUMSET1:def 1;
      P[k,NAT] or P[k,INT] or P[k,SCM-Instr]by Lm1;
      hence ex b being Element of {INT} \/ { SCM-Instr, NAT }
      st P[k,b] by A2;
    end;
    consider h being
    Function of SCM-Memory, {INT} \/ { SCM-Instr, NAT } 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;
A4: P[k,h.k] by A3;
    hence k = NAT implies h.k = NAT by Lm2;
    thus k in SCM-Data-Loc implies h.k = INT by A4,Lm2,Lm3,XBOOLE_0:3;
    thus k in NAT implies h.k = SCM-Instr by A4,Lm3,XBOOLE_0:3;
  end;
  uniqueness
  proof
    let f,g be Function of SCM-Memory, {INT} \/ { SCM-Instr, NAT }
    such that
A5: for k being Element of SCM-Memory holds
    (k = NAT implies f.k = NAT) &
    (k in SCM-Data-Loc implies f.k = INT) &
    (k in NAT implies f.k = SCM-Instr) and
A6: for k being Element of SCM-Memory holds
    (k = NAT implies g.k = NAT) &
    (k in SCM-Data-Loc implies g.k = INT) &
    (k in NAT implies g.k = SCM-Instr);
    now
      let k be Element of SCM-Memory;
      now per cases by Lm1;
        suppose
A7:       k = NAT;
          hence f.k = NAT by A5
            .= g.k by A6,A7;
        end;
        suppose
A8:       k in SCM-Data-Loc;
          hence f.k = INT by A5
            .= g.k by A6,A8;
        end;
        suppose
A9:       k in NAT;
          hence f.k = SCM-Instr by A5
            .= g.k by A6,A9;
        end;
      end;
      hence f.k = g.k;
    end;
    hence thesis by FUNCT_2:113;
  end;
end;

theorem Th6:
  SCM-Instr <> INT & NAT <> SCM-Instr
proof
  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 & NAT <> SCM-Instr by INT_1:def 2;
end;

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

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

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

theorem
  for a being Element of NAT,
  t being Element of SCM-Data-Loc holds a <> t
proof
  let a be Element of NAT, t be Element of SCM-Data-Loc;
  SCM-OK.a = SCM-Instr & SCM-OK.t = INT by Th8,Th9;
  hence a <> t by Th6;
end;

Lm4: 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) = NAT
proof
  dom SCM-OK = SCM-Memory by FUNCT_2:def 1;
  hence pi(product SCM-OK,NAT) = SCM-OK.NAT by Lm4,CARD_3:22
    .= NAT by Lm4,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 = SCM-Memory by FUNCT_2:def 1;
  hence pi(product SCM-OK,a) = SCM-OK.a by CARD_3:22
    .= INT by Th8;
end;

theorem
  for a being Element of NAT holds pi(product SCM-OK,a) = SCM-Instr
proof
  let a be Element of NAT;
  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 Th9;
end;

definition
  let s be SCM-State;
  func IC(s) -> Element of NAT equals

  s.NAT;
  coherence by Th13,CARD_3:def 6;
end;

definition
  let s be SCM-State, u be Nat;
  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,Lm4,ZFMISC_1:46;
    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 NAT by ORDINAL1:def 13;
          hence (s +* (NAT .--> u)).x in SCM-OK.x by A4,Lm4,Th7;
        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 Nat
  holds SCM-Chg(s,u).NAT = u
proof
  let s be SCM-State, u be Nat;
  {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 Nat,
  mk being Element of SCM-Data-Loc holds SCM-Chg(s,u).mk = s.mk
proof
  let s be SCM-State, u be Nat,
  mk be Element of SCM-Data-Loc;
A1: SCM-OK.NAT = NAT & SCM-OK.mk = INT by Lm4,Th7,Th8;
  {NAT} = dom(NAT .--> u) by FUNCOP_1:19;
  then not mk in dom(NAT .--> u) by A1,TARSKI:def 1,NUMBERS:27;
  hence SCM-Chg(s,u).mk = s.mk by FUNCT_4:12;
end;

theorem
  for s being SCM-State, u,v being Nat
  holds SCM-Chg(s,u).v = s.v
proof
  let s be SCM-State, u,v be Nat;
  {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,Th8;
        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 = NAT & SCM-OK.t = INT by Lm4,Th7,Th8;
  {t} = dom(t .--> u) by FUNCOP_1:19;
  then not NAT in dom(t .--> u) by A1,TARSKI:def 1,NUMBERS:27;
  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 NAT 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 NAT;
A1: SCM-OK.v = SCM-Instr & SCM-OK.t = INT by Th8,Th9;
  {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 NAT, I such that
A1: x = [ I, <*mk*>];
  func x jump_address -> Element of NAT means
  :Def11:
  ex f being FinSequence of NAT 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 NAT, I
  st x = [ I, <*mk*>] holds x jump_address = mk
proof
  let x be Element of SCM-Instr, mk be Element of NAT, I;
  assume
A1: x = [ I, <*mk*>];
  then consider f being FinSequence of NAT 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 NAT,
  ml being Element of SCM-Data-Loc, I such that
A1: x = [ I, <*mk,ml*>];
  func x cjump_address -> Element of NAT means
  :Def12:
  ex mk being Element of NAT,
  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 NAT,
  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 NAT,
  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 NAT,
  ml be Element of SCM-Data-Loc, I;
  assume
A1: x = [ I, <*mk,ml*>];
  then consider mk' being Element of NAT,
  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 NAT,
  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
 canceled 2;
  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)), succ 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)),succ 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)),succ 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)),succ 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)),succ 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 NAT st x = [ 6, <*mk*>],
  SCM-Chg(s,IFEQ(s.(x cond_address),0,x cjump_address,succ IC s))
  if ex mk being Element of NAT,
  ml being Element of SCM-Data-Loc st x = [ 7, <*mk,ml*>],
  SCM-Chg(s,IFGT(s.(x cond_address),0,x cjump_address,succ IC s))
  if ex mk being Element of NAT,
  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 Lm2;

theorem
  not NAT in NAT;

theorem
  SCM-Data-Loc misses NAT by Lm3;

theorem
  NAT in SCM-Memory by Lm4;

canceled;

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
A1: y in {1} and
A2: z in NAT and
A3: x = [y,z] by ZFMISC_1:103;
  reconsider k = z as Element of NAT by A2;
  take k;
  thus x = [1,k] by A1,A3,TARSKI:def 1;
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 ORDINAL1:def 13,TARSKI:def 1;
  hence [1,k] in SCM-Data-Loc by ZFMISC_1:106;
end;