:: Some Remarks on Simple Concrete Model of Computer
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

environ

 vocabularies AMI_1, INT_1, AMI_2, GR_CY_1, RELAT_1, FUNCT_1, CAT_1, FINSEQ_1,
      CARD_3, ARYTM_1, NAT_1, CQC_LANG, BOOLE, MCART_1, FUNCT_4, PARTFUN1,
      FUNCOP_1, FINSET_1, ORDINAL2, AMI_3, ARYTM, TARSKI, FUNCT_7;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS,
      XCMPLX_0, FUNCT_1, INT_1, NAT_1, NAT_D, ZFMISC_1, MCART_1, FUNCOP_1,
      CARD_1, CARD_3, RELAT_1, FUNCT_4, FUNCT_7,
      PARTFUN1, FINSET_1, FINSEQ_1, STRUCT_0,
      AMI_1, AMI_2, XXREAL_0;
 constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, NAT_D, FINSEQ_4, CAT_2, AMI_1,
      AMI_2;
 registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1, FUNCOP_1,
      ARYTM_3, FINSET_1, FRAENKEL, NUMBERS, XREAL_0, NAT_1, INT_1, CARD_3,
      AMI_1, AMI_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions AMI_1, INT_1, FUNCOP_1, AMI_2, CARD_1, RELSET_1;
 theorems NAT_1, PARTFUN1, FUNCT_1, SUBSET_1, GRFUNC_1, TARSKI, ZFMISC_1,
      ENUMSET1, AMI_2, FUNCOP_1, FUNCT_4, AMI_1, CARD_3, FUNCT_2, MCART_1,
      FINSEQ_3, TREES_1, INT_1, RELAT_1, RELSET_1, GR_CY_1, STRUCT_0, ORDINAL1,
      XBOOLE_0, XBOOLE_1, NAT_D, FUNCT_7,ARYTM_3;
 schemes NAT_1;

begin :: A small concrete machine

 reserve i,j,k for Element of NAT;

definition
 func SCM -> strict AMI-Struct over { INT } equals

    AMI-Struct(#SCM-Memory,In(NAT,SCM-Memory),SCM-Instr-Loc,
                 SCM-Instr,SCM-OK,SCM-Exec#);
 coherence;
end;

registration
 cluster SCM -> standard-ins non empty non void;
 coherence
  proof
   thus the Instructions of SCM
    c= [: NAT, ((union {INT}) \/ the carrier of SCM)* :];

   thus thesis by AMI_1:def 3,STRUCT_0:def 1;
  end;
end;

canceled;

theorem Th2:
 SCM is definite
proof let l be Instruction-Location of SCM;
  reconsider L = l as Element of SCM-Instr-Loc;
 thus ObjectKind l = the Instructions of SCM by AMI_2:11;
end;

registration
 cluster SCM -> IC-Ins-separated definite;
 coherence
  proof
     SCM is IC-Ins-separated
 proof
  IC SCM = In(NAT,SCM-Memory) .= NAT by FUNCT_7:def 1,AMI_2:30;
  then ObjectKind IC SCM = SCM-OK.NAT
     .= the Instruction-Locations of SCM by AMI_2:def 5,AMI_2:30;
  hence thesis by AMI_1:def 11;
 end;
  hence thesis by Th2;
  end;
end;

definition
 mode Data-Location -> Object of SCM means
:Def2: it in SCM-Data-Loc;
 existence
  proof consider x being Element of SCM-Data-Loc;
    reconsider x as Object of SCM;
   take x;
   thus thesis;
  end;
end;

definition let s be State of SCM, d be Data-Location;
 redefine func s.d -> Integer;
 coherence
  proof
    reconsider S = s as SCM-State;
    reconsider D = d as Element of SCM-Data-Loc by Def2;
        S.D = s.d;
   hence thesis;
  end;
end;

reserve a,b,c for Data-Location,
        loc for Instruction-Location of SCM,
        I for Instruction of SCM;

definition let a,b;
 func a := b -> Instruction of SCM equals
  [ 1, <*a, b*>];
 correctness
  proof
    reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
         1 in { 1,2,3,4,5} by ENUMSET1:def 3;
     then [ 1, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis;
  end;
 func AddTo(a,b) -> Instruction of SCM equals
  [ 2, <*a, b*>];
 correctness
  proof
    reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
         2 in { 1,2,3,4,5} by ENUMSET1:def 3;
     then [ 2, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis;
  end;
 func SubFrom(a,b) -> Instruction of SCM equals
  [ 3, <*a, b*>];
 correctness
  proof
    reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
         3 in { 1,2,3,4,5} by ENUMSET1:def 3;
     then [ 3, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis;
  end;
 func MultBy(a,b) -> Instruction of SCM equals
  [ 4, <*a, b*>];
 correctness
  proof
    reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
         4 in { 1,2,3,4,5} by ENUMSET1:def 3;
     then [ 4, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis;
  end;
 func Divide(a,b) -> Instruction of SCM equals
  [ 5, <*a, b*>];
 correctness
  proof
    reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
         5 in { 1,2,3,4,5} by ENUMSET1:def 3;
     then [ 5, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis;
  end;
end;

definition let loc;
 func goto loc -> Instruction of SCM equals
  [ 6, <*loc*>];
 correctness by AMI_2:3;
 let a;
 func a=0_goto loc -> Instruction of SCM equals
  [ 7, <*loc,a*>];
 correctness
  proof
    reconsider loc as Element of SCM-Instr-Loc;
    reconsider a as Element of SCM-Data-Loc by Def2;
         7 in { 7,8 } by TARSKI:def 2;
     then [ 7, <*loc,a*>] in SCM-Instr by AMI_2:4;
   hence thesis;
  end;
 func a>0_goto loc -> Instruction of SCM equals
  [ 8, <*loc,a*>];
 correctness
  proof
    reconsider loc as Element of SCM-Instr-Loc;
    reconsider a as Element of SCM-Data-Loc by Def2;
         8 in { 7,8 } by TARSKI:def 2;
     then [ 8, <*loc,a*>] in SCM-Instr by AMI_2:4;
   hence thesis;
  end;
end;

reserve s for State of SCM;

canceled;

theorem Tx:
  IC SCM = NAT by FUNCT_7:def 1,AMI_2:30;

definition let loc be Instruction-Location of SCM;
 func Next loc -> Instruction-Location of SCM means
:Def11: ex mj being Element of SCM-Instr-Loc st mj = loc & it = Next mj;
 existence
  proof reconsider loc as Element of SCM-Instr-Loc;
     Next loc is Instruction-Location of SCM by AMI_1:def 4;
   hence thesis;
  end;
 correctness;
end;

canceled;

theorem
  for loc being Instruction-Location of SCM,
     mj being Element of SCM-Instr-Loc st mj = loc
 holds Next mj = Next loc
  proof let loc be Instruction-Location of SCM,
     mj being Element of SCM-Instr-Loc such that
A1:  mj = loc;
     ex m being Element of SCM-Instr-Loc st m = loc & Next loc = Next m
           by Def11;
   hence thesis by A1;
  end;

begin :: Users guide

canceled;

theorem Th8:
 Exec(a:=b, s).IC SCM = Next IC s &
 Exec(a:=b, s).a = s.b &
 for c st c <> a holds Exec(a:=b, s).c = s.c
 proof
  reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
  reconsider I = a:=b as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  set S1 = SCM-Chg(S, I address_1,S.(I address_2));
  reconsider i = 1 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mk, ml*>];
A2: Exec(a:=b, s) = SCM-Exec-Res(I,S) by AMI_2:def 17
                 .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16;
A3: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
 ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
  hence Exec(a:=b, s).IC SCM = Next IC s by A2,AMI_2:16,Tx;
  thus Exec(a:=b, s).a = S1.mk by A2,AMI_2:17
   .= s.b by A3,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A4:   c <> a;
  thus Exec(a:=b, s).c = S1.mn by A2,AMI_2:17
    .= s.c by A3,A4,AMI_2:21;
 end;

theorem Th9:
 Exec(AddTo(a,b), s).IC SCM = Next IC s &
 Exec(AddTo(a,b), s).a = s.a + s.b &
 for c st c <> a holds Exec(AddTo(a,b), s).c = s.c
 proof
  reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
  reconsider I = AddTo(a,b) as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  set S1 = SCM-Chg(S, I address_1,S.(I address_1)+S.(I address_2));
  reconsider i = 2 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mk, ml*>];
A2: Exec(AddTo(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 17
                       .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16;
A3: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
 ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
  hence Exec(AddTo(a,b), s).IC SCM = Next IC s by A2,AMI_2:16,Tx;
  thus Exec(AddTo(a,b), s).a = S1.mk by A2,AMI_2:17
   .= s.a + s.b by A3,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A4:   c <> a;
  thus Exec(AddTo(a,b), s).c = S1.mn by A2,AMI_2:17
    .= s.c by A3,A4,AMI_2:21;
 end;

theorem Th10:
 Exec(SubFrom(a,b), s).IC SCM = Next IC s &
 Exec(SubFrom(a,b), s).a = s.a - s.b &
 for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c
 proof
  reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
  reconsider I = SubFrom(a,b) as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  set S1 = SCM-Chg(S, I address_1,S.(I address_1)-S.(I address_2));
  reconsider i = 3 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mk, ml*>];
A2: Exec(SubFrom(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 17
 .= (SCM-Chg(S1, Next IC S))
 by A1,AMI_2:def 16;
A3: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
 ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
  hence Exec(SubFrom(a,b), s).IC SCM = Next IC s by A2,AMI_2:16,Tx;
  thus Exec(SubFrom(a,b), s).a = S1.mk by A2,AMI_2:17
   .= s.a - s.b by A3,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A4:   c <> a;
  thus Exec(SubFrom(a,b), s).c = S1.mn by A2,AMI_2:17
    .= s.c by A3,A4,AMI_2:21;
 end;

theorem Th11:
 Exec(MultBy(a,b), s).IC SCM = Next IC s &
 Exec(MultBy(a,b), s).a = s.a * s.b &
 for c st c <> a holds Exec(MultBy(a,b), s).c = s.c
 proof
  reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
  reconsider I = MultBy(a,b) as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  set S1 = SCM-Chg(S, I address_1,S.(I address_1)*S.(I address_2));
  reconsider i = 4 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mk, ml*>];
A2: Exec(MultBy(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 17
                        .= (SCM-Chg(S1, Next IC S)) by A1,AMI_2:def 16;
A3: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
 ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
  hence Exec(MultBy(a,b), s).IC SCM = Next IC s by A2,AMI_2:16,Tx;
  thus Exec(MultBy(a,b), s).a = S1.mk by A2,AMI_2:17
   .= s.a * s.b by A3,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
  A4: c <> a;
  thus Exec(MultBy(a,b), s).c = S1.mn by A2,AMI_2:17
    .= s.c by A3,A4,AMI_2:21;
 end;

theorem Th12:
 Exec(Divide(a,b), s).IC SCM = Next IC s &
 (a <> b implies Exec(Divide(a,b), s).a = s.a div s.b) &
 Exec(Divide(a,b), s).b = s.a mod s.b &
 for c st c <> a & c <> b holds Exec(Divide(a,b), s).c = s.c
 proof
  reconsider mk = a, ml = b as Element of SCM-Data-Loc by Def2;
  reconsider I = Divide(a,b) as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  set S1 = SCM-Chg(S, I address_1,S.(I address_1) div S.(I address_2));
  set S1' = SCM-Chg(S1, I address_2,S.(I address_1) mod S.(I address_2));
  reconsider i = 5 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mk, ml*>];
A2: Exec(Divide(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 17
 .= (SCM-Chg(S1', Next IC S))
 by A1,AMI_2:def 16;
A3: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
 ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
  hence Exec(Divide(a,b), s).IC SCM = Next IC s by A2,AMI_2:16,Tx;
  hereby
    assume
A4:  a <> b;
    thus Exec(Divide(a,b), s).a = S1'.mk by A2,AMI_2:17
    .= S1.mk by A3,A4,AMI_2:21
    .= s.a div s.b by A3,AMI_2:20;
  end;
  thus Exec(Divide(a,b), s).b = S1'.ml by A2,AMI_2:17
   .= s.a mod s.b by A3,AMI_2:20;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A5:   c <> a & c <> b;
  thus Exec(Divide(a,b), s).c = S1'.mn by A2,AMI_2:17
    .= S1.mn by A3,A5,AMI_2:21 .= s.c by A3,A5,AMI_2:21;
 end;

theorem
     Exec(goto loc, s).IC SCM = loc &
 Exec(goto loc, s).c = s.c
 proof
  reconsider mj = loc as Element of SCM-Instr-Loc;
  reconsider I = goto loc as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  reconsider i = 6 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mj*>];
A2: Exec(goto loc, s) = SCM-Exec-Res(I,S) by AMI_2:def 17
                     .= (SCM-Chg(S,I jump_address)) by AMI_2:def 16;
     I jump_address = mj by A1,AMI_2:24;
  hence Exec(goto loc, s).IC SCM = loc by A2,AMI_2:16,Tx;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  thus Exec(goto loc, s).c = S.mn by A2,AMI_2:17 .= s.c;
 end;

theorem Th14:
 (s.a = 0 implies Exec(a =0_goto loc, s).IC SCM = loc) &
 (s.a <> 0 implies Exec(a=0_goto loc, s).IC SCM = Next IC s) &
 Exec(a=0_goto loc, s).c = s.c
 proof
  reconsider mj = loc as Element of SCM-Instr-Loc;
  reconsider a' = a as Element of SCM-Data-Loc by Def2;
  reconsider I = a=0_goto loc as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  reconsider i = 7 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mj,a'*>];
A2: Exec(a=0_goto loc, s) = SCM-Exec-Res(I,S) by AMI_2:def 17
  .= SCM-Chg(S,IFEQ(S.(I cond_address),0,I cjump_address,Next IC S))
    by A1,AMI_2:def 16;
  thus s.a = 0 implies Exec(a=0_goto loc, s).IC SCM = loc
   proof assume s.a = 0;
then A3:   S.(I cond_address)=0 by A1,AMI_2:25;
    thus Exec(a=0_goto loc, s).IC SCM =
IFEQ(S.(I cond_address),0,I cjump_address,Next IC S) by A2,AMI_2:16,Tx
      .= I cjump_address by A3,FUNCOP_1:def 8
      .= loc by A1,AMI_2:25;
   end;
  thus s.a <> 0 implies Exec(a=0_goto loc, s).IC SCM = Next IC s
   proof assume s.a <> 0;
then A4:   S.(I cond_address) <> 0 by A1,AMI_2:25;
A5: ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
    thus Exec(a=0_goto loc, s).IC SCM =
IFEQ(S.(I cond_address),0,I cjump_address,Next IC S) by A2,AMI_2:16,Tx
      .= Next IC s by A4,FUNCOP_1:def 8,A5,Tx;
   end;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  thus Exec(a=0_goto loc, s).c = S.mn by A2,AMI_2:17 .= s.c;
 end;

theorem Th15:
 (s.a > 0 implies Exec(a >0_goto loc, s).IC SCM = loc) &
 (s.a <= 0 implies Exec(a>0_goto loc, s).IC SCM = Next IC s) &
 Exec(a>0_goto loc, s).c = s.c
 proof
  reconsider mj = loc as Element of SCM-Instr-Loc;
  reconsider a' = a as Element of SCM-Data-Loc by Def2;
  reconsider I = a>0_goto loc as Element of SCM-Instr;
  reconsider S = s as SCM-State;
  reconsider i = 8 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mj,a'*>];
A2: Exec(a>0_goto loc, s) = SCM-Exec-Res(I,S) by AMI_2:def 17
   .= SCM-Chg(S,IFGT(S.(I cond_address),0,I cjump_address,Next IC S))
    by A1,AMI_2:def 16;
  thus s.a > 0 implies Exec(a>0_goto loc, s).IC SCM = loc
   proof assume s.a > 0;
then A3:   S.(I cond_address) > 0 by A1,AMI_2:25;
    thus Exec(a>0_goto loc, s).IC SCM =
IFGT(S.(I cond_address),0,I cjump_address,Next IC S) by A2,AMI_2:16,Tx
      .= I cjump_address by A3,AMI_2:def 14
      .= loc by A1,AMI_2:25;
   end;
  thus s.a <= 0 implies Exec(a>0_goto loc, s).IC SCM = Next IC s
   proof assume s.a <= 0;
then A4:   S.(I cond_address) <= 0 by A1,AMI_2:25;
A5: ex mj being Element of SCM-Instr-Loc st mj = IC s & Next IC s = Next mj
           by Def11;
    thus Exec(a>0_goto loc, s).IC SCM =
IFGT(S.(I cond_address),0,I cjump_address,Next IC S) by A2,AMI_2:16,Tx
      .= Next IC s by A4,AMI_2:def 14,A5,Tx;
   end;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  thus Exec(a>0_goto loc, s).c = S.mn by A2,AMI_2:17 .= s.c;
 end;

reserve Y,K,T for Element of Segm 9,
        a1,a2,a3 for Element of SCM-Instr-Loc,
        b1,b2,c1,c2,c3 for Element of SCM-Data-Loc;

Lm1:
 for I being Instruction of SCM st
  ex s st Exec(I,s).IC SCM = Next IC s
 holds I is non halting
  proof
    let I be Instruction of SCM;
    given s such that
A1:   Exec(I, s).IC SCM = Next IC s;
    assume
A2:   I is halting;
A3: IC s = s.NAT by Tx;
A4: Exec(I,s).IC SCM = s.NAT by A2,AMI_1:def 8,Tx;
    reconsider w = s.NAT as Instruction-Location of SCM by A3;
    consider mj being Element of SCM-Instr-Loc such that
A5:   mj = w & Next w = Next mj by Def11; :: nie mozna zastapic na 'ex'
    thus contradiction by A3,A4,A5,A1;
  end;

Lm2:
 for I being Instruction of SCM st I = [0,{}] holds I is halting
  proof
    let I be Instruction of SCM such that
A1:   I = [0,{}];
    let s be State of SCM;
    reconsider L = I as Element of SCM-Instr;
A2: I`2 = {} by A1,MCART_1:7;
A3: now let i; let mk, ml be Element of SCM-Data-Loc;
    assume I = [ i, <*mk, ml*>];
     then I`2 = <*mk, ml*> by MCART_1:7;
    hence contradiction by A2,FINSEQ_3:38;
   end;
A4: now let i; let mk be Element of SCM-Instr-Loc;
    assume I = [ i, <*mk*>];
     then I`2 = <*mk*> by MCART_1:7;
    hence contradiction by A2,TREES_1:4;
   end;
     now let i;
    let mk be Element of SCM-Instr-Loc, ml be Element of SCM-Data-Loc;
    assume I = [ i, <*mk, ml*>];
     then I`2 = <*mk, ml*> by MCART_1:7;
    hence contradiction by A2,FINSEQ_3:38;
   end;
then A5:
   not (ex mk, ml being Element of SCM-Data-Loc st I = [ 1, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st I = [ 2, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st I = [ 3, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st I = [ 4, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st I = [ 5, <*mk, ml*>]) &
   not (ex mk being Element of SCM-Instr-Loc st I = [ 6, <*mk*>]) &
   not (ex mk being Element of SCM-Instr-Loc,
           ml being Element of SCM-Data-Loc st I = [ 7, <*mk,ml*>]) &
   not (ex mk being Element of SCM-Instr-Loc,
           ml being Element of SCM-Data-Loc st I = [ 8, <*mk,ml*>]) by A3,A4;
    reconsider t = s as SCM-State;
    thus Exec(I,s) = SCM-Exec-Res(L,t) by AMI_2:def 17
       .= s by A5,AMI_2:def 16;
  end;

Lm3:
 a := b is non halting
  proof
    consider s;
        Exec(a:=b,s).IC SCM = Next IC s by Th8;
    hence thesis by Lm1;
  end;

Lm4:
 AddTo(a,b) is non halting
  proof
    consider s;
        Exec(AddTo(a,b),s).IC SCM = Next IC s by Th9;
    hence thesis by Lm1;
  end;

Lm5:
 SubFrom(a,b) is non halting
  proof
    consider s;
        Exec(SubFrom(a,b),s).IC SCM = Next IC s by Th10;
    hence thesis by Lm1;
  end;

Lm6:
 MultBy(a,b) is non halting
  proof
    consider s;
        Exec(MultBy(a,b),s).IC SCM = Next IC s by Th11;
    hence thesis by Lm1;
  end;

Lm7:
 Divide(a,b) is non halting
  proof
    consider s;
        Exec(Divide(a,b),s).IC SCM = Next IC s by Th12;
    hence thesis by Lm1;
  end;

Lm8:
 goto loc is non halting
  proof
    assume
A1:   goto loc is halting;
    reconsider V = goto loc as Element of SCM-Instr;
    reconsider a3 = loc as Element of SCM-Instr-Loc;
    consider s being SCM-State;
    set t = s +* (NAT.--> Next a3);
    set f = the Object-Kind of SCM;
A2: dom(NAT .--> Next a3) = {NAT} by FUNCOP_1:19;
    then NAT in dom (NAT.--> Next a3) by TARSKI:def 1;
then A3: t.NAT = (NAT.--> Next a3).NAT by FUNCT_4:14
       .= Next a3 by FUNCOP_1:87;
A4: {NAT} c= SCM-Memory by ZFMISC_1:37,AMI_2:30;
A5: dom s = dom SCM-OK by CARD_3:18;
A6: dom t = dom s \/ dom (NAT.--> Next a3) by FUNCT_4:def 1
         .= SCM-Memory \/ dom (NAT.--> Next a3) by A5,FUNCT_2:def 1
         .= SCM-Memory \/ {NAT} by FUNCOP_1:19
         .= SCM-Memory by A4,XBOOLE_1:12;
A7: dom f = SCM-Memory by FUNCT_2:def 1;
        for x being set st x in dom f holds t.x in f.x
    proof
      let x be set such that
A8:     x in dom f;
      per cases;
      suppose
A9:     x = NAT;
      then f.x = SCM-Instr-Loc by AMI_2:7,AMI_2:30;
      hence t.x in f.x by A3,A9;
      end;
      suppose x <> NAT;
       then not x in dom (NAT.--> Next a3) by A2,TARSKI:def 1;
       then t.x = s.x by FUNCT_4:12;
      hence t.x in f.x by A8,CARD_3:18;
    end;
    end;
    then reconsider t as State of SCM by A6,A7,CARD_3:18;
    reconsider w = t as SCM-State;
        dom(NAT .--> loc) = {NAT} by FUNCOP_1:19;
    then NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A10: (w +* (NAT .--> loc)).NAT = (NAT .--> loc).NAT by FUNCT_4:14
       .= loc by FUNCOP_1:87;
 6 is Element of Segm 9 by GR_CY_1:10;
       then w +* (NAT .--> loc)
      = SCM-Chg(w,V jump_address) by AMI_2:24
     .= SCM-Exec-Res(V,w) by AMI_2:def 16
     .= Exec(goto loc,t) by AMI_2:def 17
     .= t by A1,AMI_1:def 8;
    hence contradiction by A3,A10;
  end;

Lm9:
 a=0_goto loc is non halting
  proof
    reconsider V = a=0_goto loc as Element of SCM-Instr;
    reconsider a3 = loc as Element of SCM-Instr-Loc;
    consider s being SCM-State;
    set t = s +* (NAT.--> Next a3);
    set f = the Object-Kind of SCM;
A1: dom(NAT .--> Next a3) = {NAT} by FUNCOP_1:19;
    then NAT in dom (NAT.--> Next a3) by TARSKI:def 1;
then A2: t.NAT = (NAT.--> Next a3).NAT by FUNCT_4:14
       .= Next a3 by FUNCOP_1:87;
A3: {NAT} c= SCM-Memory by ZFMISC_1:37,AMI_2:30;
A4: dom s = dom SCM-OK by CARD_3:18;
A5: dom t = dom s \/ dom (NAT.--> Next a3) by FUNCT_4:def 1
         .= SCM-Memory \/ dom (NAT.--> Next a3) by A4,FUNCT_2:def 1
         .= SCM-Memory \/ {NAT} by FUNCOP_1:19
         .= SCM-Memory by A3,XBOOLE_1:12;
A6: dom f = SCM-Memory by FUNCT_2:def 1;
        for x being set st x in dom f holds t.x in f.x
    proof
      let x be set such that
A7:     x in dom f;
      per cases;
      suppose
A8:     x = NAT;
      then f.x = SCM-Instr-Loc by AMI_2:7,AMI_2:30;
      hence t.x in f.x by A2,A8;
      end;
      suppose x <> NAT;
      then not x in dom (NAT.--> Next a3) by A1,TARSKI:def 1;
then t.x = s.x by FUNCT_4:12;
      hence t.x in f.x by A7,CARD_3:18;
    end;
    end;
    then reconsider t as State of SCM by A5,A6,CARD_3:18;
    reconsider w = t as SCM-State;
        dom(NAT .--> loc) = {NAT} by FUNCOP_1:19;
    then NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A9: (w +* (NAT .--> loc)).NAT = (NAT .--> loc).NAT by FUNCT_4:14
       .= loc by FUNCOP_1:87;
A10: 7 is Element of Segm 9 by GR_CY_1:10;
A11: a is Element of SCM-Data-Loc by Def2;
    assume
A12:   a=0_goto loc is halting;
    per cases;
    suppose
A13:   w.(V cond_address) <> 0;
A14: IC t = IC w by Tx;
A15: IC w = w.NAT;
A16: Exec(a=0_goto loc,t).IC SCM = w.NAT by A12,AMI_1:def 8,Tx;
    reconsider e = w.NAT as Instruction-Location of SCM by A15, AMI_1:def 4;
    t.a <> 0 by A10,A11,A13,AMI_2:25;
    then
A17: Exec(a=0_goto loc,t).IC SCM = Next e by A14,Th14;
    consider mj being Element of SCM-Instr-Loc such that
A18:   mj = e & Next e = Next mj by Def11;
    thus contradiction by A16,A17,A18;
    end;
    suppose w.(V cond_address) = 0;
     then IFEQ(w.(V cond_address),0,V cjump_address,Next IC w) = V
        cjump_address
      by FUNCOP_1:def 8;
       then w +* (NAT .--> loc)
      = SCM-Chg(w,IFEQ(w.(V cond_address),0,V cjump_address,Next IC w)) by A10,
A11,AMI_2:25
     .= SCM-Exec-Res(V,w) by A11,AMI_2:def 16
     .= Exec(a=0_goto loc,t) by AMI_2:def 17
     .= t by A12,AMI_1:def 8;
    hence contradiction by A2,A9;
  end;
  end;

Lm10:
 a>0_goto loc is non halting
  proof
    reconsider V = a>0_goto loc as Element of SCM-Instr;
    reconsider a3 = loc as Element of SCM-Instr-Loc;
    consider s being SCM-State;
    set t = s +* (NAT.--> Next a3);
    set f = the Object-Kind of SCM;
A1: dom(NAT .--> Next a3) = {NAT} by FUNCOP_1:19;
    then NAT in dom (NAT.--> Next a3) by TARSKI:def 1;
then A2: t.NAT = (NAT.--> Next a3).NAT by FUNCT_4:14
       .= Next a3 by FUNCOP_1:87;
A3: {NAT} c= SCM-Memory by ZFMISC_1:37,AMI_2:30;
A4: dom s = dom SCM-OK by CARD_3:18;
A5: dom t = dom s \/ dom (NAT.--> Next a3) by FUNCT_4:def 1
         .= SCM-Memory \/ dom (NAT.--> Next a3) by A4,FUNCT_2:def 1
         .= SCM-Memory \/ {NAT} by FUNCOP_1:19
         .= SCM-Memory by A3,XBOOLE_1:12;
A6: dom f = SCM-Memory by FUNCT_2:def 1;
        for x being set st x in dom f holds t.x in f.x
    proof
      let x be set such that
A7:     x in dom f;
      per cases;
      suppose
A8:     x = NAT;
      then f.x = SCM-Instr-Loc by AMI_2:7,AMI_2:30;
      hence t.x in f.x by A2,A8;
      end;
      suppose x <> NAT;
      then not x in dom (NAT.--> Next a3) by A1,TARSKI:def 1;
      then t.x = s.x by FUNCT_4:12;
      hence t.x in f.x by A7,CARD_3:18;
    end;
    end;
    then reconsider t as State of SCM by A5,A6,CARD_3:18;
    reconsider w = t as SCM-State;
        dom(NAT .--> loc) = {NAT} by FUNCOP_1:19;
    then NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A9: (w +* (NAT .--> loc)).NAT = (NAT .--> loc).NAT by FUNCT_4:14
       .= loc by FUNCOP_1:87;
A10: 8 is Element of Segm 9 by GR_CY_1:10;
A11: a is Element of SCM-Data-Loc by Def2;
    assume
A12:   a>0_goto loc is halting;
    per cases;
    suppose
A13:   w.(V cond_address) <= 0;
A14: IC t = IC w by Tx;
A15: IC w = w.NAT;
A16: Exec(a>0_goto loc,t).IC SCM = w.NAT by A12,AMI_1:def 8,Tx;
    reconsider e = w.NAT as Instruction-Location of SCM by A15, AMI_1:def 4;
        t.a <= 0 by A10,A11,A13,AMI_2:25;
then A17: Exec(a>0_goto loc,t).IC SCM = Next e by A14,Th15;
    consider mj being Element of SCM-Instr-Loc such that
A18:   mj = e & Next e = Next mj by Def11;
    thus contradiction by A16,A17,A18;
    end;
    suppose w.(V cond_address) > 0;
then IFGT(w.(V cond_address),0,V cjump_address,Next IC w) = V
cjump_address
      by AMI_2:def 14;
       then w +* (NAT .--> loc)
      = SCM-Chg(w,IFGT(w.(V cond_address),0,V cjump_address,Next IC w)) by A10,
A11,AMI_2:25
     .= SCM-Exec-Res(V,w) by A11,AMI_2:def 16
     .= Exec(a>0_goto loc,t) by AMI_2:def 17
     .= t by A12,AMI_1:def 8;
    hence contradiction by A2,A9;
  end;
  end;

Lm11:
 for I being set holds I is Instruction of SCM iff
  I = [0,{}] or
  (ex a,b st I = a:=b) or
  (ex a,b st I = AddTo(a,b)) or
  (ex a,b st I = SubFrom(a,b)) or
  (ex a,b st I = MultBy(a,b)) or
  (ex a,b st I = Divide(a,b)) or
  (ex loc st I = goto loc) or
  (ex a,loc st I = a=0_goto loc) or
  ex a,loc st I = a>0_goto loc
  proof
    let I be set;
    thus I is Instruction of SCM implies
     I = [0,{}] or
     (ex a,b st I = a:=b) or
     (ex a,b st I = AddTo(a,b)) or
     (ex a,b st I = SubFrom(a,b)) or
     (ex a,b st I = MultBy(a,b)) or
     (ex a,b st I = Divide(a,b)) or
     (ex loc st I = goto loc) or
     (ex a,loc st I = a=0_goto loc) or
     ex a,loc st I = a>0_goto loc
    proof
      assume I is Instruction of SCM;
      then I in { [SCM-Halt,{}] } \/
          { [Y,<*a3*>] : Y = 6 } \/
          { [K,<*a1,b1*>] : K in { 7,8 } } or
           I in { [T,<*c2,c3*>] : T in { 1,2,3,4,5 } } by XBOOLE_0:def 2;
then A1:   I in { [SCM-Halt,{}] } \/
        { [Y,<*a3*>] : Y = 6 } or
         I in { [K,<*a1,b1*>] : K in { 7,8 } } or
          I in { [T,<*c2,c3*>] : T in { 1,2,3,4,5 } } by XBOOLE_0:def 2;
      per cases by A1,XBOOLE_0:def 2;
      suppose I in { [SCM-Halt,{}] };
      hence thesis by TARSKI:def 1;
      end;
      suppose I in { [Y,<*a3*>] : Y = 6 };
      then consider Y, a3 such that
A2:     I = [Y,<*a3*>] & Y = 6;
      reconsider loc = a3 as Instruction-Location of SCM by AMI_1:def 4;
          I = goto loc by A2;
      hence thesis;
      end;
      suppose I in { [K,<*a1,b1*>] : K in { 7,8 } };
      then consider K, a1, b1 such that
A3:     I = [K,<*a1,b1*>] & K in { 7,8 };
      reconsider loc = a1 as Instruction-Location of SCM by AMI_1:def 4;
      reconsider a = b1 as Data-Location by Def2;
       I = a=0_goto loc or I = a>0_goto loc by A3,TARSKI:def 2;
      hence thesis;
      end;
      suppose I in { [T,<*c2,c3*>] : T in { 1,2,3,4,5 } };
      then consider T, c2, c3 such that
A4:     I = [T,<*c2,c3*>] & T in { 1,2,3,4,5 };
      reconsider a = c2, b = c3 as Data-Location by Def2;
       I = a:=b or I = AddTo(a,b) or I = SubFrom(a,b) or I = MultBy(a,b) or
       I = Divide(a,b) by A4,ENUMSET1:def 3;
      hence thesis;
    end;
    end;
    thus thesis by AMI_2:2;
  end;

Lm12:
 for W being Instruction of SCM st W is halting holds W = [0,{}]
  proof let W be Instruction of SCM such that
A1: W is halting;
    set I = [0,{}];
    assume
A2:   I <> W;
    per cases by Lm11;
    suppose W = [0,{}];
    hence thesis by A2;
    end;
    suppose ex a,b st W = a:=b;
    hence thesis by A1,Lm3;
    end;
    suppose ex a,b st W = AddTo(a,b);
    hence thesis by A1,Lm4;
    end;
    suppose ex a,b st W = SubFrom(a,b);
    hence thesis by A1,Lm5;
    end;
    suppose ex a,b st W = MultBy(a,b);
    hence thesis by A1,Lm6;
    end;
    suppose ex a,b st W = Divide(a,b);
    hence thesis by A1,Lm7;
    end;
    suppose ex loc st W = goto loc;
    hence thesis by A1,Lm8;
    end;
    suppose ex a,loc st W = a=0_goto loc;
    hence thesis by A1,Lm9;
    end;
    suppose ex a,loc st W = a>0_goto loc;
    hence thesis by A1,Lm10;
    end;
  end;

registration
 cluster SCM -> halting;
coherence
  proof
    reconsider I = [0,{}] as Instruction of SCM by AMI_2:2;
    take I;
    thus I is halting by Lm2;
  end;
end;

Lm13:
 halt SCM = [0,{}] by Lm12;

begin :: Small concrete model

Lm14:
 for s being State of SCM, i being Instruction of SCM,
      l being Instruction-Location of SCM
   holds Exec(i,s).l = s.l
 proof let s be State of SCM, i be Instruction of SCM,
    l be Instruction-Location of SCM;
   reconsider c = i as Element of SCM-Instr;
        c in { [SCM-Halt,{}] } \/
       { [Y,<*a2*>] : Y = 6 } \/
       { [K,<*a1,b1*>] : K in { 7,8 } } or
    c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} } by XBOOLE_0:def 2;
   then A1:    c in { [SCM-Halt,{}] } \/
       { [Y,<*a2*>] : Y = 6 } or
    c in { [K,<*a1,b1*>] : K in { 7,8 } } or
    c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} } by XBOOLE_0:def 2;
   reconsider S = s as Element of product SCM-OK;
   reconsider l' = l as Element of SCM-Instr-Loc;
       now per cases by A1,XBOOLE_0:def 2;
    case c in { [SCM-Halt,{}] };
   then c = [SCM-Halt,{}] by TARSKI:def 1;
then A2: c`2 = {} by MCART_1:7;
A3: now let l be Element of NAT; let mk, ml be Element of SCM-Data-Loc;
    assume c = [ l, <*mk, ml*>];
     then c`2 = <*mk, ml*> by MCART_1:7;
    hence contradiction by A2,FINSEQ_3:38;
   end;
A4: now let l be Element of NAT; let mk be Element of SCM-Instr-Loc;
    assume c = [ l, <*mk*>];
     then c`2 = <*mk*> by MCART_1:7;
    hence contradiction by A2,TREES_1:4;
   end;
    now let l be Element of NAT;
    let mk be Element of SCM-Instr-Loc, ml be Element of SCM-Data-Loc;
    assume c = [ l, <*mk, ml*>];
     then c`2 = <*mk, ml*> by MCART_1:7;
    hence contradiction by A2,FINSEQ_3:38;
   end;
   then not (ex mk, ml being Element of SCM-Data-Loc st c = [ 1, <*mk, ml*>])
&
   not (ex mk, ml being Element of SCM-Data-Loc st c = [ 2, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st c = [ 3, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st c = [ 4, <*mk, ml*>]) &
   not (ex mk, ml being Element of SCM-Data-Loc st c = [ 5, <*mk, ml*>]) &
   not (ex mk being Element of SCM-Instr-Loc st c = [ 6, <*mk*>]) &
   not (ex mk being Element of SCM-Instr-Loc,
           ml being Element of SCM-Data-Loc st c = [ 7, <*mk,ml*>]) &
   not (ex mk being Element of SCM-Instr-Loc,
    ml being Element of SCM-Data-Loc st c = [ 8, <*mk,ml*>]) by A3,A4;
     hence SCM-Exec-Res(c,S).l' = S.l' by AMI_2:def 16;
    end;
    case c in { [Y,<*a2*>] : Y = 6 };
     then consider Y,a2 such that
A5:    c = [Y,<*a2*>] & Y = 6;
     thus SCM-Exec-Res(c,S).l' = SCM-Chg(S,c jump_address).l' by A5,
AMI_2:def 16
        .= S.l' by AMI_2:18;
    end;
    case c in { [K,<*a1,b1*>] : K in { 7,8 } };
     then consider K,a1,b1 such that
A6:    c = [K,<*a1,b1*>] & K in { 7,8 };
          now per cases by A6,TARSKI:def 2;
       case K=7;
        hence SCM-Exec-Res(c,S).l'
           = SCM-Chg(S,IFEQ(S.(c cond_address),0,c cjump_address,Next IC S)).l'
              by A6,AMI_2:def 16
          .= S.l' by AMI_2:18;
       end;
       case K=8;
        hence SCM-Exec-Res(c,S).l'
           = SCM-Chg(S,IFGT(S.(c cond_address),0,c cjump_address,Next IC S)).l'
              by A6,AMI_2:def 16
          .= S.l' by AMI_2:18;
      end;
      end;
     hence SCM-Exec-Res(c,S).l' = S.l';
    end;
    case c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} };
      then consider T,b2,c1 such that
A7:     c = [T,<*b2,c1*>] & T in { 1,2,3,4,5};
          now per cases by A7,ENUMSET1:def 3;
       case T = 1;
        hence SCM-Exec-Res(c,S).l'
          = SCM-Chg(SCM-Chg(S, c address_1,S.(c address_2)), Next IC S).l'
              by A7,AMI_2:def 16
         .= SCM-Chg(S, c address_1,S.(c address_2)).l' by AMI_2:18
         .= S.l' by AMI_2:22;
       end;
       case T = 2;
        hence SCM-Exec-Res(c,S).l'
           = SCM-Chg(SCM-Chg(S,c address_1,
            S.(c address_1)+S.(c address_2)),Next IC S).l' by A7,AMI_2:def 16
          .= SCM-Chg(S,c address_1,S.(c address_1)+S.(c address_2)).l'
               by AMI_2:18
          .= S.l' by AMI_2:22;
       end;
       case T = 3;
        hence SCM-Exec-Res(c,S).l'
           = SCM-Chg(SCM-Chg(S,c address_1,
            S.(c address_1)-S.(c address_2)),Next IC S).l' by A7,AMI_2:def 16
          .= SCM-Chg(S,c address_1,S.(c address_1)-S.(c address_2)).l'
              by AMI_2:18
          .= S.l' by AMI_2:22;
       end;
       case T = 4;
        hence SCM-Exec-Res(c,S).l'
           = SCM-Chg(SCM-Chg(S,c address_1,
            S.(c address_1)*S.(c address_2)),Next IC S).l' by A7,AMI_2:def 16
          .= SCM-Chg(S,c address_1,S.(c address_1)*S.(c address_2)).l'
              by AMI_2:18
          .= S.l' by AMI_2:22;
       end;
       case T = 5;
        hence SCM-Exec-Res(c,S).l'
           = SCM-Chg(SCM-Chg(
           SCM-Chg(S,c address_1,S.(c address_1) div S.(c address_2)),
           c address_2,S.(c address_1) mod S.(c address_2)),Next IC S).l'
              by A7,AMI_2:def 16
          .= SCM-Chg(
           SCM-Chg(S,c address_1,S.(c address_1) div S.(c address_2)),
           c address_2,S.(c address_1) mod S.(c address_2)).l' by AMI_2:18
          .= SCM-Chg(S,c address_1,S.(c address_1) div S.(c address_2)).l'
              by AMI_2:22
          .= S.l' by AMI_2:22;
      end;
      end;
     hence SCM-Exec-Res(c,S).l' = S.l';
   end;
   end;
  hence s.l = Exec(i,s).l by AMI_2:def 17;
 end;

canceled 35;

theorem Th51:
  SCM is realistic
  proof
   assume the Instruction-Counter of SCM in
            the Instruction-Locations of SCM;
    then ex k st NAT = 2*k by Tx;
    then NAT in NAT;
   hence contradiction;
  end;

registration
 cluster SCM -> steady-programmed realistic;
 coherence
  proof
   thus SCM is steady-programmed
     proof let s be State of SCM, i be Instruction of SCM,
      l be Instruction-Location of SCM;
      thus Exec(i,s).l = s.l by Lm14;
     end;
   thus thesis by Th51;
  end;
end;

definition let k be natural number;
 canceled 7;
 func dl.k -> Data-Location equals
   [1,k];
 coherence
  proof
    reconsider k as Element of NAT by ORDINAL1:def 13;
    1 in {1} by TARSKI:def 1;
    then [1,k] in SCM-Data-Loc by ZFMISC_1:106;
   hence thesis by Def2;
  end;
 func il.k -> Instruction-Location of SCM equals
   k;
 coherence
  proof
    reconsider k as Element of NAT by ORDINAL1:def 13;
    k in SCM-Instr-Loc;
   hence thesis by AMI_1:def 4;
  end;
end;

reserve i,j,k for natural number;

theorem
   i <> j implies dl.i <> dl.j by ZFMISC_1:33;

theorem
   i <> j implies il.i <> il.j;

theorem
     Next il.k = il.(k+1)
 proof
   reconsider loc = il.k as Element of SCM-Instr-Loc;
 ex mj being Element of SCM-Instr-Loc st mj = il.k & Next il.k = Next mj
           by Def11;
  hence Next il.k = il.(k+1);
 end;

theorem Th55:
 for l being Data-Location holds ObjectKind l = INT
  proof let l be Data-Location;
  l in SCM-Data-Loc by Def2;
   hence ObjectKind l = INT by AMI_2:10;
  end;

definition
 let la be Data-Location;
 let a be Integer;
 redefine func la .--> a -> FinPartState of SCM;
  coherence
   proof
        a is Element of INT & ObjectKind la = INT by Th55,INT_1:def 2;
    hence thesis by AMI_1:59;
   end;
end;

definition
 let la,lb be Data-Location;
 let a, b be Integer;
 redefine func (la,lb) --> (a,b) -> FinPartState of SCM;
  coherence
   proof
     a is Element of INT & b is Element of INT &
    ObjectKind la = INT & ObjectKind lb = INT by Th55,INT_1:def 2;
    hence thesis by AMI_1:58;
   end;
end;

theorem
     dl.i <> il.j
 proof
  assume dl.i = il.j;
   then
X:  [1,i] = j;
   j in NAT by ORDINAL1:def 13;
  hence contradiction by X,ARYTM_3:38;
 end;

theorem
 IC SCM <> dl.i & IC SCM <> il.i
 proof
  thus IC SCM <> dl.i by ARYTM_3:36,Tx;
  assume IC SCM = il.i;
   then IC SCM in SCM-Instr-Loc;
   then ex k being Element of NAT st IC SCM = k;
   then IC SCM in NAT;
   hence contradiction by Tx;
 end;

begin  :: Halt Instruction

theorem
     for I being Instruction of SCM st
  ex s st Exec(I,s).IC SCM = Next IC s
 holds I is non halting by Lm1;

theorem
     for I being Instruction of SCM st I = [0,{}] holds I is halting by Lm2;

theorem
     a := b is non halting by Lm3;

theorem
     AddTo(a,b) is non halting by Lm4;

theorem
     SubFrom(a,b) is non halting by Lm5;

theorem
     MultBy(a,b) is non halting by Lm6;

theorem
     Divide(a,b) is non halting by Lm7;

theorem
     goto loc is non halting by Lm8;

theorem
     a=0_goto loc is non halting by Lm9;

theorem
     a>0_goto loc is non halting by Lm10;

canceled;

theorem
     for I being set holds I is Instruction of SCM iff
  I = [0,{}] or
  (ex a,b st I = a:=b) or
  (ex a,b st I = AddTo(a,b)) or
  (ex a,b st I = SubFrom(a,b)) or
  (ex a,b st I = MultBy(a,b)) or
  (ex a,b st I = Divide(a,b)) or
  (ex loc st I = goto loc) or
  (ex a,loc st I = a=0_goto loc) or
  ex a,loc st I = a>0_goto loc by Lm11;

theorem
     for I being Instruction of SCM st I is halting holds I = halt SCM
                    by Lm12,Lm13;

theorem
     halt SCM = [0,{}] by Lm12;