:: The SCMPDS Computer and the Basic Semantics of Its Instructions
::  by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, STRUCT_0, AMI_1, AMI_2, FUNCT_7, SCMPDS_1,
      RELAT_1, FINSEQ_1, CARD_1, XBOOLE_0, TARSKI, FSM_1, CAT_1, AMI_3, INT_1,
      XXREAL_0, FUNCT_1, COMPLEX1, ARYTM_3, GRAPHSP, ARYTM_1, NAT_1, FUNCOP_1,
      FUNCT_4, GLIB_000, SCMPDS_2, MEMSTR_0, GOBRD13, PARTFUN1;
 notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, XCMPLX_0, RELAT_1,
      PARTFUN1, FUNCT_1, FUNCT_2, INT_1, ORDINAL1, NAT_1, FUNCOP_1, CARD_1,
      STRUCT_0, FUNCT_4, FUNCT_7, FINSEQ_1, FINSEQ_4, NUMBERS, MEMSTR_0,
      COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, INT_2, XXREAL_0, SCMPDS_I,
      SCMPDS_1;
 constructors DOMAIN_1, REAL_1, FINSEQ_4, AMI_3, SCMPDS_1, RELSET_1, FUNCT_7,
      NAT_D, VALUED_0;
 registrations XBOOLE_0, SETFAM_1, RELAT_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1,
      CARD_3, AMI_2, XXREAL_0, FUNCT_1, FUNCT_2, EXTPRO_1, AMI_3, MEASURE6,
      COMPOS_0, SCM_INST, SCMPDS_I, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions EXTPRO_1, MEMSTR_0;
 equalities TARSKI, COMPOS_1, EXTPRO_1, FUNCOP_1, AMI_2, CARD_1, SCMPDS_1,
      NAT_1, MEMSTR_0, STRUCT_0, COMPOS_0, SCMPDS_I, ORDINAL1;
 expansions EXTPRO_1, AMI_2, MEMSTR_0, STRUCT_0;
 theorems NAT_1, FUNCT_1, TARSKI, ZFMISC_1, ENUMSET1, AMI_2, FUNCOP_1, FUNCT_4,
      CARD_3, FUNCT_2, INT_1, SCMPDS_1, AMI_3, ABSVALUE, XBOOLE_0, XBOOLE_1,
      RELAT_1, XREAL_1, NUMBERS, XXREAL_0, PARTFUN1, MEMSTR_0, SCMPDS_I,
      SUBSET_1, ORDINAL1;

begin :: The SCMPDS Computer

reserve x for set,
  k for Element of NAT;

definition
  func SCMPDS -> strict AMI-Struct over Segm 2 equals
  AMI-Struct(#
    SCM-Memory,In(NAT,SCM-Memory),
    SCMPDS-Instr,
    SCM-OK,SCM-VAL,SCMPDS-Exec#);
  correctness;
end;

registration
  cluster SCMPDS -> non empty;
  coherence;
end;

registration
  cluster SCMPDS -> with_non-empty_values IC-Ins-separated;
  coherence
  by AMI_2:22,SUBSET_1:def 8,AMI_2:6;
end;

reserve s for State of SCMPDS;

::$CT

theorem Th1:
  IC SCMPDS = NAT by AMI_2:22,SUBSET_1:def 8;

begin :: The Memory Structure

registration
 cluster Int-like for Object of SCMPDS;
  existence
  proof
    reconsider x = the Element of SCM-Data-Loc as Object of SCMPDS;
    take x;
    thus thesis;
  end;
end;

definition
  mode Int_position is Int-like Object of SCMPDS;
::$CD
end;

::$CT 2

theorem Th2:
  for l being Int_position holds Values l = INT
proof
  let l be Int_position;
  l in SCM-Data-Loc by AMI_2:def 16;
  hence thesis by AMI_2:8;
end;

begin :: The Instruction Structure

reserve d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
  k1,k2,k3,k4,k5,k6 for Integer;

reserve I for Instruction of SCMPDS;

set S1=the set of all  [14,{},<*k1*>] where k1 is Element of INT;
set S2=the set of all  [1,{},<*d1*>];
set S3={ [I1,{},<*d2,k2*>] where I1 is Element of Segm 15,
d2 is Element of SCM-Data-Loc, k2 is Element of INT : I1 in {2,3}},
    S4={ [I2,{},<*
d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc, k3,
k4 is Element of INT: I2 in {4,5,6,7,8} },
     S5={ [I3,{},<*d4,d5,k5,k6*>] where I3
is Element of Segm 15, d4,d5 is Element of SCM-Data-Loc, k5,k6 is Element of
INT: I3 in {9,10,11,12,13} };

Lm1: I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4 or I in S5
proof
  I in {[0,{},{}]} \/ S1 \/ S2 \/ S3 \/ S4 or I in S5 by XBOOLE_0:def 3;
  then I in {[0,{},{}]} \/ S1 \/ S2 \/ S3 or I in S4 or I in S5
        by XBOOLE_0:def 3;
  then I in {[0,{},{}]} \/ S1 \/ S2 or I in S3 or I in S4 or I in S5
  by XBOOLE_0:def 3;
  then I in {[0,{},{}]} \/ S1 or I in S2 or I in S3 or I in S4 or I in S5
  by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  for I being Instruction of SCMPDS holds InsCode I <= 14
proof
  let I be Instruction of SCMPDS;
  InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or
  InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or
  InsCode I = 8 or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or
  InsCode I = 12 or InsCode I = 13 or InsCode I = 14 by SCMPDS_I:8;
 hence thesis;
end;

registration
  let s be State of SCMPDS, d be Int_position;
  cluster s.d -> integer;
  coherence
  proof
    reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;
    reconsider S = s as SCM-State by CARD_3:107;
    S.D = s.d;
    hence thesis;
  end;
end;

definition
  let m,n be Integer;
  func DataLoc(m,n) -> Int_position equals
  [1,|.m+n.|];
  coherence
  proof
    [1,|.m+n.|] in SCM-Data-Loc by AMI_2:24;
    hence thesis by AMI_2:def 16;
  end;
end;

theorem Th4:
  [14,{},<*k1*>] in SCMPDS-Instr
proof
  k1 is Element of INT by INT_1:def 2;
  then [14,{},<*k1*>] in S1;
  then [14,{},<*k1*>] in {[0,{},{}]} \/ S1 by XBOOLE_0:def 3;
  then [14,{},<*k1*>] in {[0,{},{}]} \/ S1 \/ S2 by XBOOLE_0:def 3;
  then [14,{},<*k1*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 by XBOOLE_0:def 3;
  then [14,{},<*k1*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 \/ S4 by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th5:
  [1,{},<*d1*>] in SCMPDS-Instr
proof
  [1,{},<*d1*>] in S2;
  then [1,{},<*d1*>] in {[0,{},{}]} \/ S1 \/ S2 by XBOOLE_0:def 3;
  then [1,{},<*d1*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 by XBOOLE_0:def 3;
  then [1,{},<*d1*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 \/ S4 by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th6:
  x in { 2,3 } implies [x,{},<*d2,k2*>] in SCMPDS-Instr
proof
  assume
A1: x in { 2,3 };
  then x = 2 or x = 3 by TARSKI:def 2;
  then reconsider x as Element of Segm 15 by NAT_1:44;
  k2 is Element of INT by INT_1:def 2;
  then [x,{},<*d2,k2*>] in S3 by A1;
  then [x,{},<*d2,k2*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 by XBOOLE_0:def 3;
  then [x,{},<*d2,k2*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 \/ S4
     by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th7:
  x in { 4,5,6,7,8 } implies [x,{},<*d2,k3,k4*>] in SCMPDS-Instr
proof
  assume
A1: x in { 4,5,6,7,8 };
  then x = 4 or x = 5 or x=6 or x=7 or x=8 by ENUMSET1:def 3;
  then reconsider x as Element of Segm 15 by NAT_1:44;
  k3 is Element of INT & k4 is Element of INT by INT_1:def 2;
  then [x,{},<*d2,k3,k4*>] in S4 by A1;
  then [x,{},<*d2,k3,k4*>] in {[0,{},{}]} \/ S1 \/ S2 \/ S3 \/ S4
  by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th8:
  x in { 9,10,11,12,13 } implies [x,{},<*d4,d5,k5,k6*>] in
  SCMPDS-Instr
proof
  assume
A1: x in { 9,10,11,12,13 };
  then x = 9 or x=10 or x=11 or x=12 or x=13 by ENUMSET1:def 3;
  then reconsider x as Element of Segm 15 by NAT_1:44;
  k5 is Element of INT & k6 is Element of INT by INT_1:def 2;
  then [x,{},<*d4,d5,k5,k6*>] in S5 by A1;
  hence thesis by XBOOLE_0:def 3;
end;

reserve a,b,c for Int_position;

definition
  let k1 be Integer;
  func goto k1 -> Instruction of SCMPDS equals
  [14,{},<*k1*>];
  correctness by Th4;
end;

definition
  let a;
  func return a -> Instruction of SCMPDS equals
  [1,{},<*a*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    [1,{},<*v*>] in SCMPDS-Instr by Th5;
    hence thesis;
  end;
end;

definition
  let a; let k1 be Integer;
  func a := k1 -> Instruction of SCMPDS equals
  [2,{},<*a,k1*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    2 in {2,3} by TARSKI:def 2;
    then [2,{},<*v,k1*>] in SCMPDS-Instr by Th6;
    hence thesis;
  end;
  func saveIC(a,k1) -> Instruction of SCMPDS equals
  [3,{},<*a,k1*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    3 in {2,3} by TARSKI:def 2;
    then [3,{},<*v,k1*>] in SCMPDS-Instr by Th6;
    hence thesis;
  end;
end;

definition
  let a; let k1,k2 be Integer;
  func (a,k1)<>0_goto k2 -> Instruction of SCMPDS equals
  [4,{},<*a,k1,k2*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    4 in { 4,5,6,7,8 } by ENUMSET1:def 3;
    then [4,{},<*v,k1,k2*>] in SCMPDS-Instr by Th7;
    hence thesis;
  end;
  func (a,k1)<=0_goto k2 -> Instruction of SCMPDS equals
  [5,{},<*a,k1,k2*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    5 in { 4,5,6,7,8 } by ENUMSET1:def 3;
    then [5,{},<*v,k1,k2*>] in SCMPDS-Instr by Th7;
    hence thesis;
  end;
  func (a,k1)>=0_goto k2 -> Instruction of SCMPDS equals
  [6,{},<*a,k1,k2*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    6 in { 4,5,6,7,8 } by ENUMSET1:def 3;
    then [6,{},<*v,k1,k2*>]in SCMPDS-Instr by Th7;
    hence thesis;
  end;
  func (a,k1) := k2 -> Instruction of SCMPDS equals
  [7,{},<*a,k1,k2*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    7 in { 4,5,6,7,8 } by ENUMSET1:def 3;
    then [7,{},<*v,k1,k2*>] in SCMPDS-Instr by Th7;
    hence thesis;
  end;
  func AddTo(a,k1,k2) -> Instruction of SCMPDS equals
  [8,{},<*a,k1,k2*>];
  correctness
  proof
    reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
    8 in { 4,5,6,7,8 } by ENUMSET1:def 3;
    then [8,{},<*v,k1,k2*>] in SCMPDS-Instr by Th7;
    hence thesis;
  end;
end;

definition
  let a,b; let k1,k2 be Integer;
  func AddTo(a,k1,b,k2) -> Instruction of SCMPDS equals
  [9,{},<*a,b,k1,k2*>];
  correctness
  proof
    reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def 16;
    9 in { 9,10,11,12,13 } by ENUMSET1:def 3;
    then [9,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th8;
    hence thesis;
  end;
  func SubFrom(a,k1,b,k2) -> Instruction of SCMPDS equals
  [10,{},<*a,b,k1,k2*>];
  correctness
  proof
    reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def 16;
    10 in { 9,10,11,12,13 } by ENUMSET1:def 3;
    then [10,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th8;
    hence thesis;
  end;
  func MultBy(a,k1,b,k2) -> Instruction of SCMPDS equals
  [11,{},<*a,b,k1,k2*>];
  correctness
  proof
    reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def 16;
    11 in { 9,10,11,12,13 } by ENUMSET1:def 3;
    then [11,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th8;
    hence thesis;
  end;
  func Divide(a,k1,b,k2) -> Instruction of SCMPDS equals
  [12,{},<*a,b,k1,k2*>];
  correctness
  proof
    reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def 16;
    12 in { 9,10,11,12,13 } by ENUMSET1:def 3;
    then [12,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th8;
    hence thesis;
  end;
  func (a,k1) := (b,k2) -> Instruction of SCMPDS equals
  [13,{},<*a,b,k1,k2*>];
  correctness
  proof
    reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def 16;
    13 in { 9,10,11,12,13 } by ENUMSET1:def 3;
    then [13,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th8;
    hence thesis;
  end;
end;

theorem
  InsCode (goto k1) = 14;

theorem
  InsCode (return a) = 1;

theorem
  InsCode (a := k1) = 2;

theorem
  InsCode (saveIC(a,k1)) = 3;

theorem
  InsCode ((a,k1)<>0_goto k2) = 4;

theorem
  InsCode ((a,k1)<=0_goto k2) = 5;

theorem
  InsCode ((a,k1)>=0_goto k2) = 6;

theorem
  InsCode ((a,k1) := k2) = 7;

theorem
  InsCode (AddTo(a,k1,k2)) = 8;

theorem
  InsCode (AddTo(a,k1,b,k2)) = 9;

theorem
  InsCode (SubFrom(a,k1,b,k2)) = 10;

theorem
  InsCode (MultBy(a,k1,b,k2)) = 11;

theorem
  InsCode (Divide(a,k1,b,k2)) = 12;

theorem
  InsCode ((a,k1) := (b,k2)) = 13;

Lm2: I in the set of all  [14,{},<*k1*>] where k1 is Element of INT
 implies
InsCode I = 14

proof
  assume I in the set of all  [14,{},<*k1*>]where k1 is Element of INT;
  then ex k1 being Element of INT st I=[14,{},<*k1*>];
  hence thesis;
end;

Lm3: I in the set of all  [1,{},<*d1*>]  implies InsCode I =1
proof
  assume I in the set of all  [1,{},<*d1*>];
  then ex d1 st I=[1,{},<*d1*>];
  hence thesis;
end;

Lm4: I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element of
SCM-Data-Loc, k1 is Element of INT : I1 in { 2, 3} } implies InsCode I =2 or
InsCode I=3

proof
  assume
  I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element
  of SCM-Data-Loc, k1 is Element of INT :I1 in { 2, 3}};

  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1
  being Element of INT such that

A1: I=[I1,{},<*d1,k1*>] and
A2: I1 in { 2, 3};
  I1 = 2 or I1 = 3 by A2,TARSKI:def 2;
  hence thesis by A1;
end;

Lm5: I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15,
d1 is Element of
SCM-Data-Loc, k1,k2 is Element of INT: I1 in { 4,5,6,7,8} } implies InsCode I =
4 or InsCode I=5 or InsCode I =6 or InsCode I=7 or InsCode I =8

proof
  assume
  I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, d1 is
  Element of SCM-Data-Loc, k1,k2 is Element of INT:I1 in { 4,5,6,7,8}};

  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1,
  k2 being Element of INT such that

A1: I=[I1,{},<*d1,k1,k2*>] and
A2: I1 in { 4,5,6,7,8};
  I1 = 4 or I1 = 5 or I1=6 or I1=7 or I1=8 by A2,ENUMSET1:def 3;
  hence thesis by A1;
end;

Lm6: I in { [I1,{},<*d1,d2,k1,k2*>]where I1 is Element of Segm 15, d1,d2 is
Element of SCM-Data-Loc, k1,k2 is Element of INT: I1 in {9,10,11,12,13} }
implies InsCode I =9 or InsCode I=10 or InsCode I =11 or InsCode I=12 or
InsCode I =13

proof
  assume
  I in { [I1,{},<*d1,d2,k1,k2*>]where I1 is Element of Segm 15, d1,d2 is
  Element of SCM-Data-Loc, k1,k2 is Element of INT:I1 in {9,10,11,12,13}};

  then consider
  I1 being Element of Segm 15, d1,d2 being Element of SCM-Data-Loc,
  k1,k2 being Element of INT such that

A1: I=[I1,{},<*d1,d2,k1,k2*>]and
A2: I1 in {9,10,11,12,13};
  I1 = 9 or I1 = 10 or I1=11 or I1=12 or I1=13 by A2,ENUMSET1:def 3;
  hence thesis by A1;
end;

Lm7:
 I in {[0,{},{}]} implies InsCode I = 0
proof
 assume I in {[0,{},{}]};
  then I = [0,{},{}] by TARSKI:def 1;
 hence thesis;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 14 holds ex k1 st
  ins = goto k1
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 14;
  I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4 or I in S5
        by Lm1;
  then consider k1 being Element of INT such that
A2: I=[14,{},<*k1*>] by A1,Lm3,Lm4,Lm5,Lm6,Lm7;
  take k1;
  thus thesis by A2;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 1 holds ex a st
  ins = return a
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 1;
  I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4 or I in S5
   by Lm1;
  then consider d1 such that
A2: I=[1,{},<*d1*>] by A1,Lm2,Lm4,Lm5,Lm6,Lm7;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a;
  thus thesis by A2;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 2 holds ex a,k1
  st ins = a := k1
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 2;
  I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4 or I in S5
   by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1
  being Element of INT such that
A2: I=[I1,{},<*d1,k1*>] and
 I1 in {2,3} by A1,Lm2,Lm3,Lm5,Lm6,Lm7;
  consider d1,k1 such that
A3: I=[2,{},<*d1,k1*>] by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 3 holds ex a,k1
  st ins = saveIC(a,k1)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 3;
  I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4 or I in S5
   by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1
  being Element of INT such that
A2: I=[I1,{},<*d1,k1*>] and
 I1 in {2,3} by A1,Lm2,Lm3,Lm5,Lm6,Lm7;
  consider d1,k1 such that
A3: I=[3,{},<*d1,k1*>]by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1;
  thus thesis by A3;
end;

Lm8: I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S5
 implies InsCode I=0 or InsCode I=14 or InsCode I
=1 or InsCode I=2 or InsCode I=3 or InsCode I=9 or InsCode I=10 or InsCode I=11
or InsCode I=12 or InsCode I=13 by Lm2,Lm3,Lm4,Lm6,Lm7;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 4 holds ex a,k1,
  k2 st ins = (a,k1)<>0_goto k2
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 4;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1,
  k2 being Element of INT such that
A2: I=[I1,{},<*d1,k1,k2*>] and
 I1 in {4,5,6,7,8} by A1,Lm8;
  consider d1,k1,k2 such that
A3: I=[4,{},<*d1,k1,k2*>] by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 5 holds ex a,k1,
  k2 st ins = (a,k1)<=0_goto k2
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 5;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1,
  k2 being Element of INT such that
A2: I=[I1,{},<*d1,k1,k2*>] and
 I1 in {4,5,6,7,8} by A1,Lm8;
  consider d1,k1,k2 such that
A3: I=[5,{},<*d1,k1,k2*>] by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 6 holds ex a,k1,
  k2 st ins = (a,k1)>=0_goto k2
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 6;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1,
  k2 being Element of INT such that
A2: I=[I1,{},<*d1,k1,k2*>] and
 I1 in {4,5,6,7,8} by A1,Lm8;
  consider d1,k1,k2 such that
A3: I=[6,{},<*d1,k1,k2*>] by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 7 holds ex a,k1,
  k2 st ins = (a,k1) := k2
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 7;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1,
  k2 being Element of INT such that
A2: I=[I1,{},<*d1,k1,k2*>] and
 I1 in {4,5,6,7,8} by A1,Lm8;
  consider d1,k1,k2 such that
A3: I=[7,{},<*d1,k1,k2*>] by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 8 holds ex a,k1,
  k2 st ins = AddTo(a,k1,k2)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 8;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc, k1,
  k2 being Element of INT such that
A2: I=[I1,{},<*d1,k1,k2*>] and
 I1 in {4,5,6,7,8} by A1,Lm8;
  consider d1,k1,k2 such that
A3: I=[8,{},<*d1,k1,k2*>] by A1,A2;
  reconsider a=d1 as Int_position by AMI_2:def 16;
  take a,k1,k2;
  thus thesis by A3;
end;

Lm9: I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4
 implies InsCode I=0 or InsCode I=14 or InsCode I
=1 or InsCode I=2 or InsCode I=3 or InsCode I=4 or InsCode I=5 or InsCode I=6
or InsCode I=7 or InsCode I=8

proof
  assume
A1: I in {[0,{},{}]} or I in S1 or I in S2 or I in S3 or I in S4;
  per cases by A1;
  suppose
    I in {[0,{},{}]};
    hence thesis by Lm7;
  end;
  suppose
    I in S1;
    hence thesis by Lm2;
  end;
  suppose
    I in S2;
    hence thesis by Lm3;
  end;
  suppose
    I in S3;
    hence thesis by Lm4;
  end;
  suppose
    I in S4;
    hence thesis by Lm5;
  end;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 9 holds ex a,b,k1
  ,k2 st ins = AddTo(a,k1,b,k2)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 9;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1,d2 being Element of SCM-Data-Loc,
  k1,k2 being Element of INT such that
A2: I=[I1,{},<*d1,d2,k1,k2*>]and
 I1 in {9,10,11,12,13} by A1,Lm9;
  consider d1,d2,k1,k2 such that
A3: I=[9,{},<*d1,d2,k1,k2*>] by A1,A2;
  reconsider a=d1,b=d2 as Int_position by AMI_2:def 16;
  take a,b,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 10 holds ex a,b,
  k1,k2 st ins = SubFrom(a,k1,b,k2)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 10;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1,d2 being Element of SCM-Data-Loc,
  k1,k2 being Element of INT such that
A2: I=[I1,{},<*d1,d2,k1,k2*>]and
 I1 in {9,10,11,12,13} by A1,Lm9;
  consider d1,d2,k1,k2 such that
A3: I=[10,{},<*d1,d2,k1,k2*>] by A1,A2;
  reconsider a=d1,b=d2 as Int_position by AMI_2:def 16;
  take a,b,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 11 holds ex a,b,
  k1,k2 st ins = MultBy(a,k1,b,k2)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 11;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1,d2 being Element of SCM-Data-Loc,
  k1,k2 being Element of INT such that
A2: I=[I1,{},<*d1,d2,k1,k2*>]and
 I1 in {9,10,11,12,13} by A1,Lm9;
  consider d1,d2,k1,k2 such that
A3: I=[11,{},<*d1,d2,k1,k2*>] by A1,A2;
  reconsider a=d1,b=d2 as Int_position by AMI_2:def 16;
  take a,b,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 12 holds ex a,b,
  k1,k2 st ins = Divide(a,k1,b,k2)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 12;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1,d2 being Element of SCM-Data-Loc,
  k1,k2 being Element of INT such that
A2: I=[I1,{},<*d1,d2,k1,k2*>]and
 I1 in {9,10,11,12,13} by A1,Lm9;
  consider d1,d2,k1,k2 such that
A3: I=[12,{},<*d1,d2,k1,k2*>] by A1,A2;
  reconsider a=d1,b=d2 as Int_position by AMI_2:def 16;
  take a,b,k1,k2;
  thus thesis by A3;
end;

theorem
  for ins being Instruction of SCMPDS st InsCode ins = 13 holds ex a,b,
  k1,k2 st ins = (a,k1) := (b,k2)
proof
  let I be Instruction of SCMPDS such that
A1: InsCode I = 13;
  I in {[0,{},{}]} or
  I in S1 or I in S2 or I in S3 or I in S4 or I in S5 by Lm1;
  then consider
  I1 being Element of Segm 15, d1,d2 being Element of SCM-Data-Loc,
  k1,k2 being Element of INT such that
A2: I=[I1,{},<*d1,d2,k1,k2*>]and
 I1 in {9,10,11,12,13} by A1,Lm9;
  consider d1,d2,k1,k2 such that
A3: I=[13,{},<*d1,d2,k1,k2*>] by A1,A2;
  reconsider a=d1,b=d2 as Int_position by AMI_2:def 16;
  take a,b,k1,k2;
  thus thesis by A3;
end;

theorem
  for s being State of SCMPDS, d being Int_position holds d in dom s
proof
  let s be State of SCMPDS, d be Int_position;
  dom s = the carrier of SCMPDS by PARTFUN1:def 2;
  hence thesis;
end;

theorem Th38:
  for s being State of SCMPDS holds SCM-Data-Loc c= dom s
proof
  let s be State of SCMPDS;
  dom s = the carrier of SCMPDS by PARTFUN1:def 2;
  hence thesis;
end;

Lm10: Data-Locations SCMPDS = SCM-Data-Loc
proof
  SCM-Data-Loc misses {NAT} by AMI_2:20,ZFMISC_1:50;
  then
A1: SCM-Data-Loc misses {NAT};

  thus Data-Locations SCMPDS = {NAT} \/ SCM-Data-Loc \ ({NAT})
  by AMI_2:22,SUBSET_1:def 8

    .= SCM-Data-Loc \/ ({NAT}) \ ({NAT})
    .= SCM-Data-Loc \ ({NAT}) by XBOOLE_1:40
    .= SCM-Data-Loc by A1,XBOOLE_1:83;
end;

theorem
  for s being State of SCMPDS holds dom DataPart s = SCM-Data-Loc
proof
  let s be State of SCMPDS;
  SCM-Data-Loc c= dom s by Th38;
  hence thesis by Lm10,RELAT_1:62;
end;

theorem
  for dl being Int_position holds dl <> IC SCMPDS
proof
  let dl be Int_position;
  Values dl = INT by Th2;
  hence thesis by MEMSTR_0:def 6,NUMBERS:7;
end;

theorem
  for s1,s2 being State of SCMPDS st IC s1 = IC s2
   & (for a being Int_position holds s1.a = s2.a)
   holds s1 = s2
proof
  let s1,s2 be State of SCMPDS such that
A1: IC(s1) = IC(s2) and
A2: for a being Int_position holds s1.a = s2.a;
A3: dom s1 = the carrier of SCMPDS by PARTFUN1:def 2;
A4: dom s2 = the carrier of SCMPDS by PARTFUN1:def 2;
A5: now
    let x be object;
    assume x in SCM-Memory;
    then
A6: x in {IC SCMPDS} \/ SCM-Data-Loc by Th1;
    per cases by A6,XBOOLE_0:def 3;
    suppose
      x in {IC SCMPDS};
      then x = IC SCMPDS by TARSKI:def 1;
      hence s1.x = s2.x by A1;
    end;
    suppose
      x in SCM-Data-Loc;
      then x is Int_position by AMI_2:def 16;
      hence s1.x = s2.x by A2;
    end;
  end;
  SCM-Memory = dom s1 by A3;
  hence thesis by A4,A5,FUNCT_1:2;
end;

begin :: Execution semantics of the SCMPDS instructions

theorem Th42:
  Exec( a:=k1, s).IC SCMPDS = IC s + 1 & Exec( a:=k1, s).a = k1 &
  for b st b <> a holds Exec( a:=k1, s).b = s.b
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider mk = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = a:=k1 as Element of SCMPDS-Instr;
  set S1 = SCM-Chg(S, I P21address, I P22const);
  reconsider i = 2 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*mk,k1*>];
  then
A2: I P21address = mk by SCMPDS_I:5;
A3: I P22const = k1 by A1,SCMPDS_I:5;
A4: InsCode(I) = 2;
A5: Exec(a:=k1, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A4,SCMPDS_1:def 22;
  hence Exec(a:=k1, s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
  thus Exec(a:=k1, s).a = S1.mk by A5,AMI_2:12
    .= k1 by A2,A3,AMI_2:15;
  let b;
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: b <> a;
  thus Exec(a:=k1, s).b = S1.mn by A5,AMI_2:12
    .= s.b by A2,A6,AMI_2:16;
end;

theorem Th43:
  Exec((a,k1):=k2, s).IC SCMPDS = IC s + 1 & Exec((a,k1):=k2, s).
DataLoc(s.a,k1) = k2 & for b st b <> DataLoc(s.a,k1) holds Exec((a,k1):=k2, s).
  b = s.b
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider mk = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = (a,k1):=k2 as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P31address,I P32const), S1 = SCM-Chg(S, A2, I
  P33const);
  reconsider i = 7 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*mk,k1,k2*>];
  then
A2: I P33const = k2 by SCMPDS_I:6;
A3: InsCode(I) = 7;
A4: Exec((a,k1):=k2, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A3,SCMPDS_1:def 22;
  hence Exec((a,k1):=k2, s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P31address = mk & I P32const = k1 by A1,SCMPDS_I:6;
  hence Exec((a,k1):=k2, s).DataLoc(s.a,k1) = S1.A2 by A4,AMI_2:12
    .= k2 by A2,AMI_2:15;
  let b;
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: b <> DataLoc(s.a,k1);
  thus Exec((a,k1):=k2, s).b = S1.mn by A4,AMI_2:12
    .= s.b by A5,A6,AMI_2:16;
end;

theorem Th44:
  Exec((a,k1):=(b,k2), s).IC SCMPDS = IC s + 1 & Exec((a,k1):=(b,
  k2), s).DataLoc(s.a,k1) = s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1)
  holds Exec((a,k1):=(b,k2),s).c = s.c
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider da = a,db=b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = (a,k1):=(b,k2) as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P41address,I P43const), A4=Address_Add(S,I P42address
  ,I P44const), S1 = SCM-Chg(S, A2, S.A4);
  reconsider i = 13 as Element of Segm 15 by NAT_1:44;
A1: I = [ i,{}, <*da,db,k1,k2*>];
  then
A2: I P42address = db & I P44const = k2 by SCMPDS_I:7;
A3: InsCode(I) = 13;
A4: Exec((a,k1):=(b,k2), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A3,SCMPDS_1:def 22;
  hence Exec((a,k1):=(b,k2), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P41address = da & I P43const = k1 by A1,SCMPDS_I:7;
  hence Exec((a,k1):=(b,k2), s).DataLoc(s.a,k1) = S1.A2 by A4,AMI_2:12
    .= s.DataLoc(s.b,k2) by A2,AMI_2:15;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: c <> DataLoc(s.a,k1);
  thus Exec((a,k1):=(b,k2), s).c = S1.mn by A4,AMI_2:12
    .= s.c by A5,A6,AMI_2:16;
end;

theorem Th45:
  Exec(AddTo(a,k1,k2), s).IC SCMPDS = IC s + 1 & Exec(AddTo(a,k1,
  k2), s).DataLoc(s.a,k1)=s.DataLoc(s.a,k1)+k2 & for b st b <>DataLoc(s.a,k1)
  holds Exec(AddTo(a,k1,k2), s).b = s.b
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider mk = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = AddTo(a,k1,k2) as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P31address,I P32const), S1 = SCM-Chg(S, A2, S.A2+I
  P33const);
  reconsider i = 8 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*mk,k1,k2*>];
  then
A2: I P33const = k2 by SCMPDS_I:6;
A3: InsCode(I) = 8;
A4: Exec(AddTo(a,k1,k2), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A3,SCMPDS_1:def 22;
  hence Exec(AddTo(a,k1,k2), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P31address = mk & I P32const = k1 by A1,SCMPDS_I:6;
  hence Exec(AddTo(a,k1,k2), s).DataLoc(s.a,k1) = S1.A2 by A4,AMI_2:12
    .= s.DataLoc(s.a,k1)+k2 by A5,A2,AMI_2:15;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: c <> DataLoc(s.a,k1);
  thus Exec(AddTo(a,k1,k2), s).c = S1.mn by A4,AMI_2:12
    .= s.c by A5,A6,AMI_2:16;
end;

theorem Th46:
  Exec(AddTo(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & Exec(AddTo(a,
k1,b,k2), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) + s.DataLoc(s.b,k2) & for c st
  c <> DataLoc(s.a,k1) holds Exec(AddTo(a,k1,b,k2),s).c = s.c
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider da = a,db=b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = AddTo(a,k1,b,k2) as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P41address,I P43const), A4=Address_Add(S,I P42address
  ,I P44const), S1 = SCM-Chg(S, A2, S.A2+S.A4);
  reconsider i = 9 as Element of Segm 15 by NAT_1:44;
A1: I = [ i,{}, <*da,db,k1,k2*>];
  then
A2: I P42address = db & I P44const = k2 by SCMPDS_I:7;
A3: InsCode(I) = 9;
A4: Exec(AddTo(a,k1,b,k2), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A3,SCMPDS_1:def 22;
  hence Exec(AddTo(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P41address = da & I P43const = k1 by A1,SCMPDS_I:7;
  hence Exec(AddTo(a,k1,b,k2), s).DataLoc(s.a,k1) = S1.A2 by A4,AMI_2:12
    .= s.DataLoc(s.a,k1) + s.DataLoc(s.b,k2) by A5,A2,AMI_2:15;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: c <> DataLoc(s.a,k1);
  thus Exec(AddTo(a,k1,b,k2), s).c = S1.mn by A4,AMI_2:12
    .= s.c by A5,A6,AMI_2:16;
end;

theorem Th47:
  Exec(SubFrom(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & Exec(SubFrom
(a,k1,b,k2), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) - s.DataLoc(s.b,k2) & for c
  st c <> DataLoc(s.a,k1) holds Exec(SubFrom(a,k1,b,k2),s).c = s.c
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider da = a,db=b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = SubFrom(a,k1,b,k2) as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P41address,I P43const), A4=Address_Add(S,I P42address
  ,I P44const), S1 = SCM-Chg(S, A2, S.A2-S.A4);
  reconsider i = 10 as Element of Segm 15 by NAT_1:44;
A1: I = [ i,{}, <*da,db,k1,k2*>];
  then
A2: I P42address = db & I P44const = k2 by SCMPDS_I:7;
A3: InsCode(I) = 10;
A4: Exec(SubFrom(a,k1,b,k2), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A3,SCMPDS_1:def 22;
  hence Exec(SubFrom(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P41address = da & I P43const = k1 by A1,SCMPDS_I:7;
  hence Exec(SubFrom(a,k1,b,k2), s).DataLoc(s.a,k1) = S1.A2 by A4,AMI_2:12
    .= s.DataLoc(s.a,k1) - s.DataLoc(s.b,k2) by A5,A2,AMI_2:15;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: c <> DataLoc(s.a,k1);
  thus Exec(SubFrom(a,k1,b,k2), s).c = S1.mn by A4,AMI_2:12
    .= s.c by A5,A6,AMI_2:16;
end;

theorem Th48:
  Exec(MultBy(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & Exec(MultBy(a
  ,k1,b,k2), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) * s.DataLoc(s.b,k2) & for c
  st c <> DataLoc(s.a,k1) holds Exec(MultBy(a,k1,b,k2),s).c = s.c
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider da = a,db=b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = MultBy(a,k1,b,k2) as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P41address,I P43const), A4=Address_Add(S,I P42address
  ,I P44const), S1 = SCM-Chg(S, A2, S.A2*S.A4);
  reconsider i = 11 as Element of Segm 15 by NAT_1:44;
A1: I = [ i,{}, <*da,db,k1,k2*>];
  then
A2: I P42address = db & I P44const = k2 by SCMPDS_I:7;
A3: InsCode(I) = 11;
A4: Exec(MultBy(a,k1,b,k2), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= (SCM-Chg(S1, IC S + 1)) by A3,SCMPDS_1:def 22;
  hence Exec(MultBy(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P41address = da & I P43const = k1 by A1,SCMPDS_I:7;
  hence Exec(MultBy(a,k1,b,k2), s).DataLoc(s.a,k1) = S1.A2 by A4,AMI_2:12
    .= s.DataLoc(s.a,k1) * s.DataLoc(s.b,k2) by A5,A2,AMI_2:15;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A6: c <> DataLoc(s.a,k1);
  thus Exec(MultBy(a,k1,b,k2), s).c = S1.mn by A4,AMI_2:12
    .= s.c by A5,A6,AMI_2:16;
end;

theorem Th49:
  Exec(Divide(a,k1,b,k2), s).IC SCMPDS = IC s + 1 & (DataLoc(s.a,
k1) <> DataLoc(s.b,k2) implies Exec(Divide(a,k1,b,k2), s).DataLoc(s.a,k1) = s.
DataLoc(s.a,k1) div s.DataLoc(s.b,k2)) & Exec(Divide(a,k1,b,k2), s).DataLoc(s.b
,k2) = s.DataLoc(s.a,k1) mod s.DataLoc(s.b,k2) & for c st c <> DataLoc(s.a,k1)
  & c <> DataLoc(s.b,k2) holds Exec(Divide(a,k1,b,k2),s).c = s.c
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider da = a,db=b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = Divide(a,k1,b,k2) as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P41address,I P43const), A4=Address_Add(S,I P42address
,I P44const), S1 = SCM-Chg(S, A2,S.A2 div S.A4), S2 = SCM-Chg(S1,A4,S.A2 mod S.
  A4);
  reconsider i = 12 as Element of Segm 15 by NAT_1:44;
  set Da=DataLoc(s.a,k1), Db=DataLoc(s.b,k2);
A1: I = [ i,{}, <*da,db,k1,k2*>];
  then
A2: I P41address = da & I P43const = k1 by SCMPDS_I:7;
A3: InsCode(I) = 12;
A4: Exec(Divide(a,k1,b,k2), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= SCM-Chg(S2, IC S + 1) by A3,SCMPDS_1:def 22;
  hence Exec(Divide(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
A5: I P42address = db & I P44const = k2 by A1,SCMPDS_I:7;
  hereby
    reconsider mn = Da as Element of SCM-Data-Loc by AMI_2:def 16;
    assume
A6: Da <> DataLoc(s.b,k2);
    thus Exec(Divide(a,k1,b,k2), s).Da = S2.mn by A4,AMI_2:12
      .= S1.A2 by A2,A5,A6,AMI_2:16
      .= s.Da div s.Db by A2,A5,AMI_2:15;
  end;
  thus Exec(Divide(a,k1,b,k2), s).DataLoc(s.b,k2) = S2.A4 by A4,A5,AMI_2:12
    .= s.Da mod s.Db by A2,A5,AMI_2:15;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
  assume that
A7: c <> Da and
A8: c <> Db;
  thus Exec(Divide(a,k1,b,k2), s).c = S2.mn by A4,AMI_2:12
    .= S1.mn by A5,A8,AMI_2:16
    .= s.c by A2,A7,AMI_2:16;
end;

theorem
  Exec(Divide(a,k1,a,k1), s).IC SCMPDS = IC s + 1 & Exec(Divide(a,k1,a,
k1), s).DataLoc(s.a,k1) = s.DataLoc(s.a,k1) mod s.DataLoc(s.a,k1) & for c st c
  <> DataLoc(s.a,k1) holds Exec(Divide(a,k1,a,k1),s).c = s.c by Th49;

definition
  let s be State of SCMPDS,c be Integer;
  func ICplusConst(s,c) -> Element of NAT means
  :Def17:
  ex m
  be Element of NAT st m = IC s & it = |.m+c.|;
  existence
  proof
    reconsider m1=IC s as Element of NAT;
    consider k being Element of NAT such that
A1: m1 = k;
    reconsider m=|.k+c.| as Nat;
    reconsider l = m as Element of NAT;
    take l;
    thus thesis by A1;
  end;
  correctness;
end;

theorem Th51:
  Exec(goto k1, s).IC SCMPDS = ICplusConst(s,k1) & for a holds
  Exec(goto k1, s).a = s.a
proof
  reconsider i = 14 as Element of Segm 15 by NAT_1:44;
  reconsider I = goto k1 as Element of SCMPDS-Instr;
  reconsider S = s as SCM-State by CARD_3:107;
 I = [ i,{}, <*k1*>];
  then
A1: I const_INT = k1 by SCMPDS_I:4;
A2: InsCode(I) = 14;
A3: Exec(goto k1, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .=SCM-Chg(S,jump_address(S,I const_INT)) by A2,SCMPDS_1:def 22;
  ex n be Element of NAT st n=IC s & ICplusConst(s,k1)=|.n+k1.| by Def17;
  hence Exec(goto k1, s).IC SCMPDS =ICplusConst(s,k1) by A3,A1,Th1,AMI_2:11;
  let a;
  reconsider mn = a as Element of SCM-Data-Loc by AMI_2:def 16;
  thus Exec(goto k1, s).a = S.mn by A3,AMI_2:12
    .= s.a;
end;

theorem Th52:
  ( s.DataLoc(s.a,k1) <> 0 implies Exec((a,k1)<>0_goto k2, s).IC
  SCMPDS = ICplusConst(s,k2)) & ( s.DataLoc(s.a,k1) = 0 implies Exec((a,k1)
  <>0_goto k2, s).IC SCMPDS = IC s + 1 ) & Exec((a,k1)<>0_goto k2, s).b = s.b
proof
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider S = s as SCM-State by CARD_3:107;
A1: ex n be Element of NAT st n=IC s & ICplusConst(s,k2)=|.n+k2.| by Def17;
  reconsider da = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = (a,k1)<>0_goto k2 as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P31address,I P32const), JP=jump_address(S,I P33const)
  , IF=IFEQ(S.A2, 0, IC S + 1,JP), Da=DataLoc(s.a,k1);
  reconsider i = 4 as Element of Segm 15 by NAT_1:44;
A2: I = [ i,{}, <*da,k1,k2*>];
  then
A3: I P31address = da & I P32const = k1 by SCMPDS_I:6;
A4: InsCode(I) = 4;
A5: Exec((a,k1)<>0_goto k2, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .=SCM-Chg(S,IF) by A4,SCMPDS_1:def 22;
A6: I P33const = k2 by A2,SCMPDS_I:6;
  thus s.Da <> 0 implies Exec((a,k1)<>0_goto k2,s).IC SCMPDS = ICplusConst(s,
  k2)
  proof
    assume
A7: s.Da <> 0;
    thus Exec((a,k1)<>0_goto k2, s).IC SCMPDS = IF by A5,Th1,AMI_2:11
      .=ICplusConst(s,k2) by A3,A6,A1,A7,Th1,FUNCOP_1:def 8;
  end;
  thus s.Da = 0 implies Exec((a,k1)<>0_goto k2,s).IC SCMPDS = IC s + 1
  proof
    assume
A8: s.Da = 0;
    thus Exec((a,k1)<>0_goto k2, s).IC SCMPDS = IF by A5,Th1,AMI_2:11
      .= IC S + 1 by A3,A8,FUNCOP_1:def 8
      .= IC s + 1 by AMI_2:22,SUBSET_1:def 8;
  end;
  thus Exec((a,k1)<>0_goto k2, s).b = S.mn by A5,AMI_2:12
    .= s.b;
end;

theorem Th53:
  ( s.DataLoc(s.a,k1) <= 0 implies Exec((a,k1)<=0_goto k2, s).IC
  SCMPDS = ICplusConst(s,k2)) & ( s.DataLoc(s.a,k1) > 0 implies Exec((a,k1)
  <=0_goto k2, s).IC SCMPDS = IC s + 1 ) & Exec((a,k1)<=0_goto k2, s).b = s.b
proof
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider S = s as SCM-State by CARD_3:107;
A1: ex n be Element of NAT st n=IC s & ICplusConst(s,k2)=|.n+k2.| by Def17;
  reconsider da = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = (a,k1)<=0_goto k2 as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P31address,I P32const),
    JP=jump_address(S,I P33const), Da=DataLoc(s.a,k1);
  reconsider IF=IFGT(S.A2, 0, IC S + 1,JP) as Element of NAT
      by ORDINAL1:def 12;
  reconsider i = 5 as Element of Segm 15 by NAT_1:44;
A2: I = [ i,{}, <*da,k1,k2*>];
  then
A3: I P31address = da & I P32const = k1 by SCMPDS_I:6;
A4: InsCode(I) = 5;
A5: Exec((a,k1)<=0_goto k2, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .=SCM-Chg(S,IF) by A4,SCMPDS_1:def 22;
A6: I P33const = k2 by A2,SCMPDS_I:6;
  thus s.Da <= 0 implies Exec((a,k1)<=0_goto k2,s).IC SCMPDS = ICplusConst(s,
  k2)
  proof
    assume
A7: s.Da <= 0;
    thus Exec((a,k1)<=0_goto k2, s).IC SCMPDS = IF by A5,Th1,AMI_2:11
      .=ICplusConst(s,k2) by A3,A6,A1,A7,Th1,XXREAL_0:def 11;
  end;
  thus s.Da > 0 implies Exec((a,k1)<=0_goto k2,s).IC SCMPDS = IC s + 1
  proof
    assume
A8: s.Da > 0;
    thus Exec((a,k1)<=0_goto k2, s).IC SCMPDS = IF by A5,Th1,AMI_2:11
      .= IC S + 1 by A3,A8,XXREAL_0:def 11
      .= IC s + 1 by AMI_2:22,SUBSET_1:def 8;
  end;
  thus Exec((a,k1)<=0_goto k2, s).b = S.mn by A5,AMI_2:12
    .= s.b;
end;

theorem Th54:
  ( s.DataLoc(s.a,k1) >= 0 implies Exec((a,k1)>=0_goto k2, s).IC
  SCMPDS = ICplusConst(s,k2)) & ( s.DataLoc(s.a,k1) < 0 implies Exec((a,k1)
  >=0_goto k2, s).IC SCMPDS = IC s + 1 ) & Exec((a,k1)>=0_goto k2, s).b = s.b
proof
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider S = s as SCM-State by CARD_3:107;
A1: ex n be Element of NAT st n=IC s & ICplusConst(s,k2)=|.n+k2.| by Def17;
  reconsider da = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = (a,k1)>=0_goto k2 as Element of SCMPDS-Instr;
  set A2=Address_Add(S,I P31address,I P32const), JP=jump_address(S,I P33const)
  , IF=IFGT(0, S.A2, IC S + 1,JP), Da=DataLoc(s.a,k1);
  reconsider i = 6 as Element of Segm 15 by NAT_1:44;
A2: I = [ i,{}, <*da,k1,k2*>];
  then
A3: I P31address = da & I P32const = k1 by SCMPDS_I:6;
A4: InsCode(I) = 6;
A5: Exec((a,k1)>=0_goto k2, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .=SCM-Chg(S,IF) by A4,SCMPDS_1:def 22;
A6: I P33const = k2 by A2,SCMPDS_I:6;
  thus s.Da >= 0 implies Exec((a,k1)>=0_goto k2,s).IC SCMPDS = ICplusConst(s,
  k2)
  proof
    assume
A7: s.Da >= 0;
    thus Exec((a,k1)>=0_goto k2, s).IC SCMPDS = IF by A5,Th1,AMI_2:11
      .=ICplusConst(s,k2) by A3,A6,A1,A7,Th1,XXREAL_0:def 11;
  end;
  thus s.Da < 0 implies Exec((a,k1)>=0_goto k2,s).IC SCMPDS = IC s + 1
  proof
    assume
A8: s.Da < 0;
    thus Exec((a,k1)>=0_goto k2, s).IC SCMPDS = IF by A5,Th1,AMI_2:11
      .= IC S + 1 by A3,A8,XXREAL_0:def 11
      .= IC s + 1 by AMI_2:22,SUBSET_1:def 8;
  end;
  thus Exec((a,k1)>=0_goto k2, s).b = S.mn by A5,AMI_2:12
    .= s.b;
end;

theorem Th55:
  Exec(return a, s).IC SCMPDS = (|.s.DataLoc(s.a,RetIC).|)+2 &
Exec(return a, s).a = s.DataLoc(s.a,RetSP) & for b st a <> b holds Exec(return
  a, s).b = s.b
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider da = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = return a as Element of SCMPDS-Instr;
  set A1 =Address_Add(S,I address_1,RetSP), S1 =SCM-Chg(S,I address_1,S.A1),
  A2=Address_Add(S,I address_1,RetIC), lc=PopInstrLoc(S,A2);
  reconsider i = 1 as Element of Segm 15 by NAT_1:44;
 I = [ i,{}, <*da*>];
  then
A1: I address_1 = da by SCMPDS_I:3;
A2: InsCode(I) = 1;
A3: Exec(return a, s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= SCM-Chg(S1,lc) by A2,SCMPDS_1:def 22;
  hence Exec(return a, s).IC SCMPDS =(|.s.DataLoc(s.a,RetIC).|)+2 by A1,Th1,
AMI_2:11;
  thus Exec(return a, s).a = S1.da by A3,AMI_2:12
    .= s.DataLoc(s.a,RetSP) by A1,AMI_2:15;
  let b;
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A4: b <> a;
  thus Exec(return a, s).b = S1.mn by A3,AMI_2:12
    .= s.b by A1,A4,AMI_2:16;
end;

theorem Th56:
  Exec(saveIC(a,k1),s).IC SCMPDS = IC s + 1 & Exec(saveIC(a,k1),
s).DataLoc(s.a,k1) = IC s & for b st DataLoc(s.a,k1) <> b holds Exec(saveIC(a,
  k1), s).b = s.b
proof
  reconsider S = s as SCM-State by CARD_3:107;
  reconsider m = IC S as Element of NAT;
  reconsider da = a as Element of SCM-Data-Loc by AMI_2:def 16;
  reconsider I = saveIC(a,k1) as Element of SCMPDS-Instr;
  set A1=Address_Add(S,I P21address,I P22const), S1=SCM-Chg(S, A1,m);
  reconsider i = 3 as Element of Segm 15 by NAT_1:44;
  set DL=DataLoc(s.a,k1);
 I = [ i,{}, <*da,k1*>];
  then
A1: I P21address = da & I P22const = k1 by SCMPDS_I:5;
A2: InsCode(I) = 3;
A3: Exec(saveIC(a,k1), s) = SCM-Exec-Res(I,S) by SCMPDS_1:def 23
    .= SCM-Chg(S1,IC S + 1) by A2,SCMPDS_1:def 22;
  hence Exec(saveIC(a,k1), s).IC SCMPDS = IC s + 1 by Th1,AMI_2:11;
  thus Exec(saveIC(a,k1), s).DL =S1.A1 by A3,A1,AMI_2:12
    .=IC s by Th1,AMI_2:15;
  let b;
  reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
  assume
A4: DL <> b;
  thus Exec(saveIC(a,k1),s).b = S1.mn by A3,AMI_2:12
    .= s.b by A1,A4,AMI_2:16;
end;

::$CT

theorem Th57:
  for k be Integer holds ex s be State of SCMPDS st for d being
  Int_position holds s.d = k
proof
  set f = the_Values_of SCMPDS;
  set S =the  SCM-State;
  let k be Integer;
  S is total (SCM-Memory)-defined Function by AMI_2:29;
   then
A1: dom S = the carrier of SCMPDS by PARTFUN1:def 2;
A2: dom f = SCM-Memory by PARTFUN1:def 2;
  k in INT by INT_1:def 2;
  then reconsider g = SCM-Data-Loc --> k as Function of SCM-Data-Loc,INT
               by FUNCOP_1:45;
  set t = S +* g;
A3: for x being object st x in dom f holds t.x in f.x
  proof
    let x be object such that
A4: x in dom f;
    per cases;
    suppose
A5:   x in dom g;
      then
A6:   x in SCM-Data-Loc;
      then
A7:   f.x = INT by AMI_2:8;
      t.x = g.x by A5,FUNCT_4:13
        .= k by A6,FUNCOP_1:7;
      hence thesis by A7,INT_1:def 2;
    end;
    suppose
      not x in dom g;
      then t.x = S.x by FUNCT_4:11;
      hence thesis by A4,CARD_3:9;
    end;
  end;
  dom t = dom S \/ dom g by FUNCT_4:def 1
    .= SCM-Memory \/ dom g by A1
    .= SCM-Memory \/ SCM-Data-Loc
    .= SCM-Memory by XBOOLE_1:12;
  then reconsider s=t as State of SCMPDS by A2,A3,FUNCT_1:def 14,PARTFUN1:def 2
,RELAT_1:def 18;
  take s;
  let d be Int_position;
  reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;
  D in dom g;
  hence s.d =g.D by FUNCT_4:13
    .=k;
end;

theorem Th58:
  for k be Integer,loc be Element of NAT holds ex
  s be State of SCMPDS st s.NAT=loc & for d being Int_position holds s.d = k
proof
  set f = the_Values_of SCMPDS;
  let k be Integer,loc be Element of NAT;
A1: {NAT} c= SCM-Memory by AMI_2:22,ZFMISC_1:31;
A2: dom f = SCM-Memory by PARTFUN1:def 2;
  consider s1 be State of SCMPDS such that
A3: for d being Int_position holds s1.d = k by Th57;
  reconsider S = s1 as SCM-State by CARD_3:107;
  set t = S +* (NAT.--> loc);
A4: dom S = the carrier of SCMPDS by PARTFUN1:def 2;
  NAT in dom (NAT.--> loc) by TARSKI:def 1;
  then
A6: t.NAT = (NAT.--> loc).NAT by FUNCT_4:13
    .= loc by FUNCOP_1:72;
  then
A7: t.NAT in NAT;
A8: for x being object st x in dom f holds t.x in f.x
  proof
    let x be object such that
A9: x in dom f;
    per cases;
    suppose
      x = NAT;
      hence thesis by A7,AMI_2:6;
    end;
    suppose
      x <> NAT;
      then not x in dom (NAT.--> loc) by TARSKI:def 1;
      then t.x = S.x by FUNCT_4:11;
      hence thesis by A9,CARD_3:9;
    end;
  end;
  dom t = dom S \/ dom (NAT.--> loc) by FUNCT_4:def 1
    .= SCM-Memory \/ dom (NAT.--> loc) by A4
    .= SCM-Memory \/ {NAT}
    .= SCM-Memory by A1,XBOOLE_1:12;
  then reconsider s=t as State of SCMPDS by A2,A8,FUNCT_1:def 14,PARTFUN1:def 2
,RELAT_1:def 18;
  take s;
  thus s.NAT=loc by A6;
  hereby
    let d be Int_position;
    d in SCM-Data-Loc by AMI_2:def 16;
    then
A10: ex j be Nat st d=[1,j] by AMI_2:23;
     not d in dom (NAT.--> loc) by A10,TARSKI:def 1;
    hence s.d=s1.d by FUNCT_4:11
      .=k by A3;
  end;
end;

Lm11:
 InsCode I = 0 implies Exec(I,s) = s
proof
 assume InsCode I = 0;
   then
A1:   InsCode I <> 1 & InsCode I <> 2 & InsCode I <> 3 & InsCode I <> 4 &
     InsCode I <> 5 & InsCode I <> 6 & InsCode I <> 7 & InsCode I <> 8 &
     InsCode I <> 9 & InsCode I <> 10 & InsCode I <> 11 & InsCode I <> 12 &
     InsCode I <> 13 & InsCode I <> 14;
   reconsider ss = s as SCM-State by CARD_3:107;
   reconsider ii = I as Element of SCMPDS-Instr;
 thus Exec(I,s) = ((the Execution of SCMPDS).I).s
        .= SCMPDS-Exec.I.s
        .= SCM-Exec-Res (ii,ss) by SCMPDS_1:def 23
        .= s by A1,SCMPDS_1:def 22;
end;

theorem Th59:
  for I being Instruction of SCMPDS st I = [0,{},{}]
  holds I is halting
proof
  let I be Instruction of SCMPDS;
  assume I = [0,{},{}];
   then
A1: InsCode I = 0;
  let s be State of SCMPDS;
  thus Exec(I,s) = s by A1,Lm11;
end;

theorem Th60:
  for I being Instruction of SCMPDS st ex s st Exec(I,s).IC SCMPDS
  = IC s + 1 holds I is non halting
proof
  let I be Instruction of SCMPDS;
  given s such that
A1: Exec(I, s).IC SCMPDS = IC s + 1;
  assume I is halting;
  then Exec(I,s).IC SCMPDS = s.NAT by Th1;
  hence contradiction by A1,Th1;
  IC s = s.NAT by AMI_2:22,SUBSET_1:def 8;
  then reconsider w = s.NAT as Element of NAT;
end;

theorem
  a:=k1 is non halting
proof
  set s =the  State of SCMPDS;
  Exec(a:=k1, s).IC SCMPDS = IC s + 1 by Th42;
  hence thesis by Th60;
end;

theorem
  (a,k1):=k2 is non halting
proof
  set s =the  State of SCMPDS;
  Exec((a,k1):=k2, s).IC SCMPDS = IC s + 1 by Th43;
  hence thesis by Th60;
end;

theorem
  (a,k1):=(b,k2) is non halting
proof
  set s =the  State of SCMPDS;
  Exec((a,k1):=(b,k2), s).IC SCMPDS = IC s + 1 by Th44;
  hence thesis by Th60;
end;

theorem
  AddTo(a,k1,k2) is non halting
proof
  set s =the  State of SCMPDS;
  Exec(AddTo(a,k1,k2), s).IC SCMPDS = IC s + 1 by Th45;
  hence thesis by Th60;
end;

theorem
  AddTo(a,k1,b,k2) is non halting
proof
  set s =the  State of SCMPDS;
  Exec(AddTo(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th46;
  hence thesis by Th60;
end;

theorem
  SubFrom(a,k1,b,k2) is non halting
proof
  set s =the  State of SCMPDS;
  Exec(SubFrom(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th47;
  hence thesis by Th60;
end;

theorem
  MultBy(a,k1,b,k2) is non halting
proof
  set s =the  State of SCMPDS;
  Exec(MultBy(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th48;
  hence thesis by Th60;
end;

theorem
  Divide(a,k1,b,k2) is non halting
proof
  set s =the  State of SCMPDS;
  Exec(Divide(a,k1,b,k2), s).IC SCMPDS = IC s + 1 by Th49;
  hence thesis by Th60;
end;

theorem
  k1 <> 0 implies goto k1 is non halting
proof
  assume
A1: k1<>0;
  set n=|.k1.|;
  reconsider loc=n+1 as Element of NAT;
  consider s be State of SCMPDS such that
A2: s.NAT=loc and
  for d being Int_position holds s.d = 0 by Th58;
  -n<=k1 by ABSVALUE:4;
  then 0-n<=k1;
  then
A3: (n+k1)*1>=0 by XREAL_1:20;
  ex m be Element of NAT st m=IC s & ICplusConst(s,k1)=|.m+k1.| by Def17;
  then
A4: Exec(goto k1, s).IC SCMPDS = |.n+k1+1.| by A2,Th1,Th51
    .= |.n+k1.|+|.1.| by A3,ABSVALUE:11
    .=|.(n+k1).|+1 by ABSVALUE:def 1
    .=(n+k1)+1 by A3,ABSVALUE:def 1
    .=n+1+k1;
  assume goto k1 is halting;
  then Exec(goto k1,s).IC SCMPDS = n+1 by A2,Th1;
  hence contradiction by A1,A4;
end;

theorem
  (a,k1)<>0_goto k2 is non halting
proof
  consider s being State of SCMPDS such that
A1: for d being Int_position holds s.d = 0 by Th57;
  s.DataLoc(s.a,k1) = 0 by A1;
  then Exec((a,k1)<>0_goto k2, s).IC SCMPDS = IC s + 1 by Th52;
  hence thesis by Th60;
end;

theorem
  (a,k1)<=0_goto k2 is non halting
proof
  consider s being State of SCMPDS such that
A1: for d being Int_position holds s.d = 1 by Th57;
  s.DataLoc(s.a,k1) = 1 by A1;
  then Exec((a,k1)<=0_goto k2, s).IC SCMPDS = IC s + 1 by Th53;
  hence thesis by Th60;
end;

theorem
  (a,k1)>=0_goto k2 is non halting
proof
  consider s being State of SCMPDS such that
A1: for d being Int_position holds s.d = -1 by Th57;
  s.DataLoc(s.a,k1) = -1 by A1;
  then Exec((a,k1)>=0_goto k2, s).IC SCMPDS = IC s + 1 by Th54;
  hence thesis by Th60;
end;

theorem
  return a is non halting
proof
  reconsider loc=1 as Element of NAT;
A1: In(NAT,SCM-Memory) = NAT by AMI_2:22,SUBSET_1:def 8;
  consider s be State of SCMPDS such that
A2: s.NAT=loc and
A3: for d being Int_position holds s.d = 0 by Th58;
  Exec(return a, s).IC SCMPDS = (|.s.DataLoc(s.a,RetIC).|)+2 by Th55
    .=(|.0.|)+2 by A3
    .=0+2 by ABSVALUE:def 1
    .=IC s + 1 by A2,A1;
  hence thesis by Th60;
end;

theorem
  saveIC(a,k1) is non halting
proof
  set s =the  State of SCMPDS;
  Exec(saveIC(a,k1), s).IC SCMPDS = IC s + 1 by Th56;
  hence thesis by Th60;
end;

theorem
  for I being set holds I is Instruction of SCMPDS implies
   I = [0,{},{}] or
   (ex k1 st I
= goto k1) or (ex a st I = return a) or (ex a,k1 st I = saveIC(a,k1)) or (ex a,
k1 st I = a:=k1) or (ex a,k1,k2 st I = (a,k1):=k2) or (ex a,k1,k2 st I = (a,k1)
<>0_goto k2) or (ex a,k1,k2 st I = (a,k1)<=0_goto k2) or (ex a,k1,k2 st I = (a,
k1)>=0_goto k2) or (ex a,b,k1,k2 st I = AddTo(a,k1,k2)) or (ex a,b,k1,k2 st I =
AddTo(a,k1,b,k2)) or (ex a,b,k1,k2 st I = SubFrom(a,k1,b,k2)) or (ex a,b,k1,k2
st I = MultBy(a,k1,b,k2)) or (ex a,b,k1,k2 st I = Divide(a,k1,b,k2)) or ex a,b,
  k1,k2 st I = (a,k1):=(b,k2)
proof
  let I be set;
    assume I is Instruction of SCMPDS;
    then reconsider I as Instruction of SCMPDS;
    per cases by Lm1;
    suppose
      I in {[0,{},{}]};
      then I = [0,{},{}] by TARSKI:def 1;
      hence thesis;
    end;
    suppose
      I in S1;
      then consider k1 being Element of INT such that
A1:   I = [14,{},<*k1*>];
      I = goto k1 by A1;
      hence thesis;
    end;
    suppose
      I in S2;
      then consider d1 such that
A2:   I = [1,{},<*d1*>];
      reconsider a=d1 as Int_position by AMI_2:def 16;
      I = return a by A2;
      hence thesis;
    end;
    suppose
      I in S3;
      then consider
      I2 being Element of Segm 15, d2 being Element of SCM-Data-Loc,
      k2 being Element of INT such that
A3:   I = [I2,{},<*d2,k2*>] & I2 in {2,3};
      reconsider a=d2 as Int_position by AMI_2:def 16;
      I = saveIC(a,k2) or I = a:=k2 by A3,TARSKI:def 2;
      hence thesis;
    end;
    suppose
      I in S4;
      then consider
      I3 being Element of Segm 15, d3 being Element of SCM-Data-Loc,
      k1,k2 being Element of INT such that
A4:   I=[I3,{},<*d3,k1,k2*>] & I3 in {4,5,6,7,8};
      reconsider a=d3 as Int_position by AMI_2:def 16;
      I = (a,k1)<>0_goto k2 or I=(a,k1)<=0_goto k2 or I= (a,k1) >=0_goto
      k2 or I= (a,k1) := k2 or I=AddTo(a,k1,k2) by A4,ENUMSET1:def 3;
      hence thesis;
    end;
    suppose
      I in S5;
      then consider I3 being Element of Segm 15, d4,d5 being Element of
      SCM-Data-Loc, k1,k2 being Element of INT such that
A5:   I=[I3,{},<*d4,d5,k1,k2*>] & I3 in {9,10,11,12,13};
      reconsider a=d4,b=d5 as Int_position by AMI_2:def 16;
      I=AddTo(a,k1,b,k2) or I=SubFrom(a,k1,b,k2) or I=MultBy(a,k1,b,k2)
      or I=Divide(a,k1,b,k2) or I=(a,k1) := (b,k2) by A5,ENUMSET1:def 3;
      hence thesis;
    end;
end;

:: Poniewaz zostal dodany prawdziwy halt,
:: tego lematu nie mozna udowodnic.
::Lm11: for W being Instruction of SCMPDS st W is halting holds W = goto 0
::proof
::  set I = goto 0;
::  let W be Instruction of SCMPDS such that
::A1: W is halting;
::  assume
::A2: I <> W;
::  per cases by Th91;
::  suppose
::    ex k1 st W=goto k1;
::    hence thesis by A1,A2,Th85;
::  end;
::  suppose
::    ex a st W = return a;
::    hence thesis by A1,Th89;
::  end;
::  suppose
::    ex a,k1 st W = saveIC(a,k1);
::    hence thesis by A1,Th90;
::  end;
::  suppose
::    ex a,k1 st W = a:=k1;
::    hence thesis by A1,Th77;
::  end;
::  suppose
::    ex a,k1,k2 st W=(a,k1):=k2;
::    hence thesis by A1,Th78;
::  end;
::  suppose
::    ex a,k1,k2 st W = (a,k1)<>0_goto k2;
::    hence thesis by A1,Th86;
::  end;
::  suppose
::    ex a,k1,k2 st W = (a,k1)<=0_goto k2;
::    hence thesis by A1,Th87;
::  end;
::  suppose
::    ex a,k1,k2 st W = (a,k1)>=0_goto k2;
::    hence thesis by A1,Th88;
::  end;
::  suppose
::    ex a,b,k1,k2 st W = AddTo(a,k1,k2);
::    hence thesis by A1,Th80;
::  end;
::  suppose
::    ex a,b,k1,k2 st W = AddTo(a,k1,b,k2);
::    hence thesis by A1,Th81;
::  end;
::  suppose
::    ex a,b,k1,k2 st W = SubFrom(a,k1,b,k2);
::    hence thesis by A1,Th82;
::  end;
::  suppose
::    ex a,b,k1,k2 st W = MultBy(a,k1,b,k2);
::    hence thesis by A1,Th83;
::  end;
::  suppose
::    ex a,b,k1,k2 st W = Divide(a,k1,b,k2);
::    hence thesis by A1,Th84;
::  end;
::  suppose
::    ex a,b,k1,k2 st W = (a,k1):=(b,k2);
::    hence thesis by A1,Th79;
::  end;
::end;

registration
  cluster SCMPDS -> halting;
  coherence
  by Th59;
end;

::Dopoki sa przeskoki, to jednoznacznosc instrukcji, ktora jest halting
:: i tak sie nie uda udowodnic.
::theorem Th92:
::  for I being Instruction of SCMPDS st I is halting holds I = halt
::  SCMPDS
::proof
::  let I be Instruction of SCMPDS;
::  assume I is halting;
::  then I = goto 0 by Lm11;
::  hence thesis by Lm11;
::end;

theorem
  halt SCMPDS = [0,{},{}];

::$CT

theorem
  for i being Element of NAT holds IC SCMPDS <> dl.i
proof
  let i be Element of NAT;
    assume IC SCMPDS = dl.i;
    then NAT = [1,i] by Th1,AMI_3:def 11;
    hence contradiction;
end;

::$CT

theorem
  Data-Locations SCMPDS = SCM-Data-Loc by Lm10;

::$CT

theorem
 InsCode I = 0 implies Exec(I,s) = s by Lm11;