The Mizar article:

Some Remarks on the Simple Concrete Model of Computer

by
Andrzej Trybulec, and
Yatsuka Nakamura

Received October 8, 1993

Copyright (c) 1993 Association of Mizar Users

MML identifier: AMI_3
[ MML identifier index ]


environ

 vocabulary AMI_1, INT_1, AMI_2, GR_CY_1, RELAT_1, FUNCT_1, CAT_1, FINSEQ_1,
      FUNCT_2, CARD_3, ARYTM_1, NAT_1, CQC_LANG, BOOLE, MCART_1, FUNCT_4,
      PARTFUN1, FUNCOP_1, FINSET_1, ORDINAL2, AMI_3, ARYTM;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0, FUNCT_1, FUNCT_2, INT_1, NAT_1, MCART_1, CQC_LANG,
      CARD_3, GR_CY_1, RELAT_1, FUNCT_4, PARTFUN1, FINSET_1, FINSEQ_1,
      STRUCT_0, AMI_1, CAT_3, AMI_2;
 constructors DOMAIN_1, REAL_1, NAT_1, CAT_2, FINSEQ_4, AMI_1, AMI_2, CAT_3,
      MEMBERED, XBOOLE_0;
 clusters INT_1, AMI_1, FUNCT_1, RELSET_1, AMI_2, CQC_LANG, NAT_1, FINSET_1,
      XBOOLE_0, FRAENKEL, MEMBERED, ZFMISC_1, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions AMI_1, TARSKI, INT_1, XBOOLE_0;
 theorems NAT_1, PARTFUN1, FUNCT_1, SUBSET_1, GRFUNC_1, TARSKI, ZFMISC_1,
      ENUMSET1, AMI_2, CQC_LANG, FUNCT_4, AMI_1, FUNCOP_1, CARD_3, FUNCT_2,
      MCART_1, FINSEQ_3, TREES_1, INT_1, RELAT_1, RELSET_1, GR_CY_1, STRUCT_0,
      ORDINAL2, XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes NAT_1;

begin :: A small concrete machine


 reserve i,j,k for Nat;

definition
 func SCM -> strict AMI-Struct over { INT } equals
:Def1:
   AMI-Struct(#NAT,0,SCM-Instr-Loc,Segm 9,SCM-Instr,SCM-OK,SCM-Exec#);
 coherence;
end;

definition
 cluster SCM -> non empty non void;
 coherence by Def1,AMI_1:def 3,STRUCT_0:def 1;
end;

theorem Th1:
 SCM is data-oriented
 proof
  set A = SCM;
  let x be set;
  assume A1: x in (the Object-Kind of A)"{ the Instructions of A };
  then reconsider x as Nat by Def1,FUNCT_2:46;
    SCM-OK.x in { SCM-Instr } by A1,Def1,FUNCT_2:46;
  then SCM-OK.x = SCM-Instr by TARSKI:def 1;
  then consider k such that
A2:      x = 2*k+2*1 by AMI_2:9;
    x = 2*(k + 1) & k + 1 > 0 by A2,NAT_1:19,XCMPLX_1:8;
  hence thesis by Def1,AMI_2:def 3;
 end;

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

definition
 cluster SCM -> IC-Ins-separated data-oriented definite;
 coherence
  proof
   SCM is IC-Ins-separated
 proof
A1: IC SCM = 0 by Def1,AMI_1:def 5;
      ObjectKind IC SCM
     = SCM-OK.IC SCM by Def1,AMI_1:def 6
    .= the Instruction-Locations of SCM by A1,Def1,AMI_2:def 5;
  hence thesis by AMI_1:def 11;
 end;
  hence thesis by Th1,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 by Def1;
   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 by Def1;
    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
:Def3: [ 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:24;
     then [ 1, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis by Def1;
  end;
 func AddTo(a,b) -> Instruction of SCM equals
:Def4: [ 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:24;
     then [ 2, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis by Def1;
  end;
 func SubFrom(a,b) -> Instruction of SCM equals
:Def5: [ 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:24;
     then [ 3, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis by Def1;
  end;
 func MultBy(a,b) -> Instruction of SCM equals
:Def6: [ 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:24;
     then [ 4, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis by Def1;
  end;
 func Divide(a,b) -> Instruction of SCM equals
:Def7: [ 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:24;
     then [ 5, <*mk, ml*>] in SCM-Instr by AMI_2:5;
   hence thesis by Def1;
  end;
end;

definition let loc;
 func goto loc -> Instruction of SCM equals
:Def8: [ 6, <*loc*>];
 correctness by Def1, AMI_2:3;
 let a;
 func a=0_goto loc -> Instruction of SCM equals
:Def9: [ 7, <*loc,a*>];
 correctness
  proof
    reconsider loc as Element of SCM-Instr-Loc by Def1;
    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 by Def1;
  end;
 func a>0_goto loc -> Instruction of SCM equals
:Def10: [ 8, <*loc,a*>];
 correctness
  proof
    reconsider loc as Element of SCM-Instr-Loc by Def1;
    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 by Def1;
  end;
end;

reserve s for State of SCM;

canceled;

theorem Th4:
 IC SCM = 0 by Def1,AMI_1:def 5;

theorem Th5:
 for S being SCM-State st S = s holds IC s = IC S
 proof let S be SCM-State; assume S = s;
  hence IC s = S.0 by Th4,AMI_1:def 15 .= IC S by AMI_2:def 6;
 end;

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 by Def1;
      Next loc is Instruction-Location of SCM by Def1;
   hence thesis;
  end;
 correctness;
end;

theorem Th6:
 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 be Element of SCM-Instr-Loc;
     ex mj being Element of SCM-Instr-Loc st mj = loc & Next loc= Next mj
    by Def11;
  hence thesis;
 end;

theorem Th7:
for i being Element of SCM-Instr st i = I
for S being SCM-State st S = s holds
 Exec(I,s) = SCM-Exec-Res(i,S)
 proof let i be Element of SCM-Instr such that
A1: i = I;
  let S be SCM-State; assume
   S = s;
  hence Exec(I,s) =
(SCM-Exec.i qua Element of Funcs(product SCM-OK, product SCM-OK)).S
           by A1,Def1,AMI_1:def 7
        .= SCM-Exec-Res(i,S) by AMI_2:def 17;
 end;

begin :: Users guide

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 by Def1;
  reconsider S = s as SCM-State by Def1;
  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*>] by Def3;
A2:  IC s = IC S by Th5;
A3: Exec(a:=b, s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S))
 by A1,AMI_2:def 16;
A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
  thus Exec(a:=b, s).IC SCM = Next IC S by A3,Th4,AMI_2:16
    .= Next IC s by A2,Th6;
  thus Exec(a:=b, s).a = S1.mk by A3,AMI_2:17
   .= s.b by A4,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A5:   c <> a;
  thus Exec(a:=b, s).c = S1.mn by A3,AMI_2:17
    .= s.c by A4,A5,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 by Def1;
  reconsider S = s as SCM-State by Def1;
  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*>] by Def4;
A2:  IC s = IC S by Th5;
A3: Exec(AddTo(a,b), s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S))
 by A1,AMI_2:def 16;
A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
  thus Exec(AddTo(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16
    .= Next IC s by A2,Th6;
  thus Exec(AddTo(a,b), s).a = S1.mk by A3,AMI_2:17
   .= s.a + s.b by A4,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A5:   c <> a;
  thus Exec(AddTo(a,b), s).c = S1.mn by A3,AMI_2:17
    .= s.c by A4,A5,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 by Def1;
  reconsider S = s as SCM-State by Def1;
  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*>] by Def5;
A2:  IC s = IC S by Th5;
A3: Exec(SubFrom(a,b), s) = SCM-Exec-Res(I,S) by Th7
 .= (SCM-Chg(S1, Next IC S))
 by A1,AMI_2:def 16;
A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
  thus Exec(SubFrom(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16
    .= Next IC s by A2,Th6;
  thus Exec(SubFrom(a,b), s).a = S1.mk by A3,AMI_2:17
   .= s.a - s.b by A4,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A5:   c <> a;
  thus Exec(SubFrom(a,b), s).c = S1.mn by A3,AMI_2:17
    .= s.c by A4,A5,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 by Def1;
  reconsider S = s as SCM-State by Def1;
  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*>] by Def6;
A2:  IC s = IC S by Th5;
A3: Exec(MultBy(a,b), s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S1, Next IC S))
 by A1,AMI_2:def 16;
A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
  thus Exec(MultBy(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16
    .= Next IC s by A2,Th6;
  thus Exec(MultBy(a,b), s).a = S1.mk by A3,AMI_2:17
   .= s.a * s.b by A4,AMI_2:20;
  let c;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
  A5: c <> a;
  thus Exec(MultBy(a,b), s).c = S1.mn by A3,AMI_2:17
    .= s.c by A4,A5,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 by Def1;
  reconsider S = s as SCM-State by Def1;
  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*>] by Def7;
A2:  IC s = IC S by Th5;
A3: Exec(Divide(a,b), s) = SCM-Exec-Res(I,S) by Th7
 .= (SCM-Chg(S1', Next IC S))
 by A1,AMI_2:def 16;
A4: I address_1 = mk & I address_2 = ml by A1,AMI_2:23;
  thus Exec(Divide(a,b), s).IC SCM = Next IC S by A3,Th4,AMI_2:16
    .= Next IC s by A2,Th6;
  hereby
    assume
A5:  a <> b;
    thus Exec(Divide(a,b), s).a = S1'.mk by A3,AMI_2:17
    .= S1.mk by A4,A5,AMI_2:21
    .= s.a div s.b by A4,AMI_2:20;
  end;
  thus Exec(Divide(a,b), s).b = S1'.ml by A3,AMI_2:17
   .= s.a mod s.b by A4,AMI_2:20;
  let c;
  reconsider mn = c as Element of SCM-Data-Loc by Def2;
  assume
A6:   c <> a & c <> b;
  thus Exec(Divide(a,b), s).c = S1'.mn by A3,AMI_2:17
    .= S1.mn by A4,A6,AMI_2:21 .= s.c by A4,A6,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 by Def1;
  reconsider I = goto loc as Element of SCM-Instr by Def1;
  reconsider S = s as SCM-State by Def1;
  reconsider i = 6 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mj*>] by Def8;
A2: Exec(goto loc, s) = SCM-Exec-Res(I,S) by Th7 .= (SCM-Chg(S,I jump_address))
 by A1,AMI_2:def 16;
   I jump_address = mj by A1,AMI_2:24;
  hence Exec(goto loc, s).IC SCM = loc by A2,Th4,AMI_2:16;
   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 by Def1;
  reconsider a' = a as Element of SCM-Data-Loc by Def2;
  reconsider I = a=0_goto loc as Element of SCM-Instr by Def1;
  reconsider S = s as SCM-State by Def1;
  reconsider i = 7 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mj,a'*>] by Def9;
A2:  IC s = IC S by Th5;
A3: Exec(a=0_goto loc, s) = SCM-Exec-Res(I,S) by Th7
  .= 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 A4:   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 A3,Th4,AMI_2:16
      .= I cjump_address by A4,CQC_LANG:def 1
      .= 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 A5:   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 A3,Th4,AMI_2:16
      .= Next IC S by A5,CQC_LANG:def 1
      .= Next IC s by A2,Th6;
   end;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  thus Exec(a=0_goto loc, s).c = S.mn by A3,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 by Def1;
  reconsider a' = a as Element of SCM-Data-Loc by Def2;
  reconsider I = a>0_goto loc as Element of SCM-Instr by Def1;
  reconsider S = s as SCM-State by Def1;
  reconsider i = 8 as Element of Segm 9 by GR_CY_1:10;
A1:  I = [ i, <*mj,a'*>] by Def10;
A2:  IC s = IC S by Th5;
A3: Exec(a>0_goto loc, s) = SCM-Exec-Res(I,S) by Th7
   .= 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 A4:   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 A3,Th4,AMI_2:16
      .= I cjump_address by A4,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 A5:   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 A3,Th4,AMI_2:16
      .= Next IC S by A5,AMI_2:def 14
      .= Next IC s by A2,Th6;
   end;
   reconsider mn = c as Element of SCM-Data-Loc by Def2;
  thus Exec(a>0_goto loc, s).c = S.mn by A3,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;
    reconsider t = s as SCM-State by Def1;
A3: IC t = IC s by Th5;
A4: IC t = t.0 by AMI_2:def 6;
A5: Exec(I,s).IC SCM = s.IC SCM by A2,AMI_1:def 8
       .= t.0 by A3,A4,AMI_1:def 15;
    reconsider w = t.0 as Instruction-Location of SCM by A4,Def1;
    consider mj being Element of SCM-Instr-Loc such that
A6:   mj = w & Next w = Next mj by Def11;
A7: Exec(I,s).IC SCM = Next w by A1,A4,Th5;
      Next w = mj + 2 by A6,AMI_2:def 15;
    hence contradiction by A5,A6,A7,XCMPLX_1:3;
  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 by A1,AMI_2:2;
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 by Def1;
    thus Exec(I,s) = SCM-Exec-Res(L,t) by Th7
       .= 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 by Def1;
    reconsider a3 = loc as Element of SCM-Instr-Loc by Def1;
A2: goto loc = [ 6, <*loc*>] by Def8;
    consider s being SCM-State;
    set t = s +* (0.--> Next a3);
    set f = the Object-Kind of SCM;
A3: dom(0 .--> Next a3) = {0} by CQC_LANG:5;
    then 0 in dom (0.--> Next a3) by TARSKI:def 1;
then A4: t.0 = (0.--> Next a3).0 by FUNCT_4:14
       .= Next a3 by CQC_LANG:6;
then A5: t.0 = a3 + 2 by AMI_2:def 15;
A6: {0} c= NAT by ZFMISC_1:37;
A7: dom s = dom SCM-OK by CARD_3:18;
A8: dom t = dom s \/ dom (0.--> Next a3) by FUNCT_4:def 1
         .= NAT \/ dom (0.--> Next a3) by A7,FUNCT_2:def 1
         .= NAT \/ {0} by CQC_LANG:5
         .= NAT by A6,XBOOLE_1:12;
A9: dom f = NAT by Def1,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
A10:     x in dom f;
      per cases;
      suppose
A11:     x = 0;
      then f.x = SCM-Instr-Loc by Def1,AMI_2:7;
      hence t.x in f.x by A4,A11;
      suppose x <> 0;
      then not x in dom (0.--> Next a3) by A3,TARSKI:def 1;
then t.x = s.x by FUNCT_4:12;
      hence t.x in f.x by A10,Def1,CARD_3:18;
    end;
    then reconsider t as State of SCM by A8,A9,CARD_3:18;
    reconsider w = t as SCM-State by Def1;
      dom(0 .--> loc) = {0} by CQC_LANG:5;
    then 0 in dom (0 .--> loc) by TARSKI:def 1;
then A12: (w +* (0 .--> loc)).0 = (0 .--> loc).0 by FUNCT_4:14
       .= loc by CQC_LANG:6;
A13: 6 is Element of Segm 9 by GR_CY_1:10;
      w +* (0 .--> loc)
      = SCM-Chg(w,a3) by AMI_2:def 7
     .= SCM-Chg(w,V jump_address) by A2,A13,AMI_2:24
     .= SCM-Exec-Res(V,w) by A2,AMI_2:def 16
     .= Exec(goto loc,t) by Th7
     .= t by A1,AMI_1:def 8;
    hence contradiction by A5,A12,XCMPLX_1:3;
  end;

Lm9:
 a=0_goto loc is non halting
  proof
    reconsider V = a=0_goto loc as Element of SCM-Instr by Def1;
    reconsider a3 = loc as Element of SCM-Instr-Loc by Def1;
A1: a=0_goto loc = [ 7, <*loc,a*>] by Def9;
    consider s being SCM-State;
    set t = s +* (0.--> Next a3);
    set f = the Object-Kind of SCM;
A2: dom(0 .--> Next a3) = {0} by CQC_LANG:5;
    then 0 in dom (0.--> Next a3) by TARSKI:def 1;
then A3: t.0 = (0.--> Next a3).0 by FUNCT_4:14
       .= Next a3 by CQC_LANG:6;
then A4: t.0 = a3 + 2 by AMI_2:def 15;
A5: {0} c= NAT by ZFMISC_1:37;
A6: dom s = dom SCM-OK by CARD_3:18;
A7: dom t = dom s \/ dom (0.--> Next a3) by FUNCT_4:def 1
         .= NAT \/ dom (0.--> Next a3) by A6,FUNCT_2:def 1
         .= NAT \/ {0} by CQC_LANG:5
         .= NAT by A5,XBOOLE_1:12;
A8: dom f = NAT by Def1,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
A9:     x in dom f;
      per cases;
      suppose
A10:     x = 0;
      then f.x = SCM-Instr-Loc by Def1,AMI_2:7;
      hence t.x in f.x by A3,A10;
      suppose x <> 0;
      then not x in dom (0.--> Next a3) by A2,TARSKI:def 1;
then t.x = s.x by FUNCT_4:12;
      hence t.x in f.x by A9,Def1,CARD_3:18;
    end;
    then reconsider t as State of SCM by A7,A8,CARD_3:18;
    reconsider w = t as SCM-State by Def1;
      dom(0 .--> loc) = {0} by CQC_LANG:5;
    then 0 in dom (0 .--> loc) by TARSKI:def 1;
then A11: (w +* (0 .--> loc)).0 = (0 .--> loc).0 by FUNCT_4:14
       .= loc by CQC_LANG:6;
A12: 7 is Element of Segm 9 by GR_CY_1:10;
A13: a is Element of SCM-Data-Loc by Def2;
    assume
A14:   a=0_goto loc is halting;
    per cases;
    suppose
A15:   w.(V cond_address) <> 0;
A16: IC t = IC w by Th5;
A17: IC w = w.0 by AMI_2:def 6;
A18: Exec(a=0_goto loc,t).IC SCM = t.IC SCM by A14,AMI_1:def 8
       .= w.0 by A16,A17,AMI_1:def 15;
    reconsider e = w.0 as Instruction-Location of SCM by A17,Def1;
      t.a <> 0 by A1,A12,A13,A15,AMI_2:25;
then A19: Exec(a=0_goto loc,t).IC SCM = Next e by A16,A17,Th14;
    consider mj being Element of SCM-Instr-Loc such that
A20:   mj = e & Next e = Next mj by Def11;
      Next e = mj + 2 by A20,AMI_2:def 15;
    hence contradiction by A18,A19,A20,XCMPLX_1:3;
    suppose w.(V cond_address) = 0;
then A21: IFEQ(w.(V cond_address),0,V cjump_address,Next IC w) = V
cjump_address
      by CQC_LANG:def 1;
      w +* (0 .--> loc)
      = SCM-Chg(w,a3) by AMI_2:def 7
     .= SCM-Chg(w,IFEQ(w.(V cond_address),0,V cjump_address,Next IC w)) by A1,
A12,A13,A21,AMI_2:25
     .= SCM-Exec-Res(V,w) by A1,A13,AMI_2:def 16
     .= Exec(a=0_goto loc,t) by Th7
     .= t by A14,AMI_1:def 8;
    hence contradiction by A4,A11,XCMPLX_1:3;
  end;

Lm10:
 a>0_goto loc is non halting
  proof
    reconsider V = a>0_goto loc as Element of SCM-Instr by Def1;
    reconsider a3 = loc as Element of SCM-Instr-Loc by Def1;
A1: a>0_goto loc = [ 8, <*loc,a*>] by Def10;
    consider s being SCM-State;
    set t = s +* (0.--> Next a3);
    set f = the Object-Kind of SCM;
A2: dom(0 .--> Next a3) = {0} by CQC_LANG:5;
    then 0 in dom (0.--> Next a3) by TARSKI:def 1;
then A3: t.0 = (0.--> Next a3).0 by FUNCT_4:14
       .= Next a3 by CQC_LANG:6;
then A4: t.0 = a3 + 2 by AMI_2:def 15;
A5: {0} c= NAT by ZFMISC_1:37;
A6: dom s = dom SCM-OK by CARD_3:18;
A7: dom t = dom s \/ dom (0.--> Next a3) by FUNCT_4:def 1
         .= NAT \/ dom (0.--> Next a3) by A6,FUNCT_2:def 1
         .= NAT \/ {0} by CQC_LANG:5
         .= NAT by A5,XBOOLE_1:12;
A8: dom f = NAT by Def1,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
A9:     x in dom f;
      per cases;
      suppose
A10:     x = 0;
      then f.x = SCM-Instr-Loc by Def1,AMI_2:7;
      hence t.x in f.x by A3,A10;
      suppose x <> 0;
      then not x in dom (0.--> Next a3) by A2,TARSKI:def 1;
then t.x = s.x by FUNCT_4:12;
      hence t.x in f.x by A9,Def1,CARD_3:18;
    end;
    then reconsider t as State of SCM by A7,A8,CARD_3:18;
    reconsider w = t as SCM-State by Def1;
      dom(0 .--> loc) = {0} by CQC_LANG:5;
    then 0 in dom (0 .--> loc) by TARSKI:def 1;
then A11: (w +* (0 .--> loc)).0 = (0 .--> loc).0 by FUNCT_4:14
       .= loc by CQC_LANG:6;
A12: 8 is Element of Segm 9 by GR_CY_1:10;
A13: a is Element of SCM-Data-Loc by Def2;
    assume
A14:   a>0_goto loc is halting;
    per cases;
    suppose
A15:   w.(V cond_address) <= 0;
A16: IC t = IC w by Th5;
A17: IC w = w.0 by AMI_2:def 6;
A18: Exec(a>0_goto loc,t).IC SCM = t.IC SCM by A14,AMI_1:def 8
       .= w.0 by A16,A17,AMI_1:def 15;
    reconsider e = w.0 as Instruction-Location of SCM by A17,Def1;
      t.a <= 0 by A1,A12,A13,A15,AMI_2:25;
then A19: Exec(a>0_goto loc,t).IC SCM = Next e by A16,A17,Th15;
    consider mj being Element of SCM-Instr-Loc such that
A20:   mj = e & Next e = Next mj by Def11;
      Next e = mj + 2 by A20,AMI_2:def 15;
    hence contradiction by A18,A19,A20,XCMPLX_1:3;
    suppose w.(V cond_address) > 0;
then A21: IFGT(w.(V cond_address),0,V cjump_address,Next IC w) = V
cjump_address
      by AMI_2:def 14;
      w +* (0 .--> loc)
      = SCM-Chg(w,a3) by AMI_2:def 7
     .= SCM-Chg(w,IFGT(w.(V cond_address),0,V cjump_address,Next IC w)) by A1,
A12,A13,A21,AMI_2:25
     .= SCM-Exec-Res(V,w) by A1,A13,AMI_2:def 16
     .= Exec(a>0_goto loc,t) by Th7
     .= t by A14,AMI_1:def 8;
    hence contradiction by A4,A11,XCMPLX_1:3;
  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 Def1,AMI_2:def 4,
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 AMI_2:def 1,TARSKI:def 1;
      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 Def1;
        I = goto loc by A2,Def8;
      hence thesis;
      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 Def1;
      reconsider a = b1 as Data-Location by Def1,Def2;
        K = 7 or K = 8 by A3,TARSKI:def 2;
      then I = a=0_goto loc or I = a>0_goto loc by A3,Def9,Def10;
      hence thesis;
      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 Def1,Def2;
        T = 1 or T = 2 or T = 3 or T = 4 or T = 5 by A4,ENUMSET1:23;
      then 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,Def3,Def4,Def5,Def6,Def7;
      hence thesis;
    end;
    thus thesis by Def1,AMI_2:2;
  end;

definition
 cluster SCM -> halting;
coherence
  proof
    reconsider I = [0,{}] as Instruction of SCM by Def1,AMI_2:2;
    take I;
    thus I is halting by Lm2;
    let W be Instruction of SCM such that
A1:   W is halting;
    assume
A2:   I <> W;
    per cases by Lm11;
    suppose W = [0,{}];
    hence thesis by A2;
    suppose ex a,b st W = a:=b;
    hence thesis by A1,Lm3;
    suppose ex a,b st W = AddTo(a,b);
    hence thesis by A1,Lm4;
    suppose ex a,b st W = SubFrom(a,b);
    hence thesis by A1,Lm5;
    suppose ex a,b st W = MultBy(a,b);
    hence thesis by A1,Lm6;
    suppose ex a,b st W = Divide(a,b);
    hence thesis by A1,Lm7;
    suppose ex loc st W = goto loc;
    hence thesis by A1,Lm8;
    suppose ex a,loc st W = a=0_goto loc;
    hence thesis by A1,Lm9;
    suppose ex a,loc st W = a>0_goto loc;
    hence thesis by A1,Lm10;
  end;
end;

Lm12:
 for I being Instruction of SCM st I is halting holds I = halt SCM
  proof
    let I be Instruction of SCM such that
A1:   I is halting;
    consider K being Instruction of SCM such that
        K is halting and
A2:   for J being Instruction of SCM st J is halting holds K = J
       by AMI_1:def 9;
    thus I = K by A1,A2
          .= halt SCM by A2;
  end;

Lm13:
 halt SCM = [0,{}]
  proof
    reconsider I = [0,{}] as Instruction of SCM by Def1,AMI_2:2;
      I is halting by Lm2;
    hence thesis by Lm12;
  end;

begin :: Preliminaries

canceled 2;

theorem Th18:
 for m,j being Integer holds m*j, 0 are_congruent_mod m
 proof let m,j be Integer;
  take j;
  thus m*j = m*j - 0;
 end;

scheme INDI{ k,n() -> Nat, P[set] }:
     P[n()]
provided
 A1: P[0] and
 A2: k() > 0 and
 A3: for i,j st P[k()*i] & j <> 0 & j <= k() holds
     P[k()*i+j]
 proof
   defpred R[Nat] means P[k()*$1];
A4: R[0] by A1;
A5: now let i; assume
A6:  R[i];
       k()*(i+1) = k()*i + k()*1 by XCMPLX_1:8
       .= k()*i + k();
    hence R[i+1] by A2,A3,A6;
   end;
  A7: for i holds R[i] from Ind(A4,A5);
then A8: P[k()*(n() div k())];
  per cases;
  suppose n() mod k() = 0;
   then n() = k() * (n() div k()) + 0 by A2,NAT_1:47;
   hence thesis by A7;
  suppose
A9: n() mod k() <> 0;
A10: n() = k() * (n() div k()) + (n() mod k()) by A2,NAT_1:47;
     n() mod k() <= k() by A2,NAT_1:46;
  hence thesis by A3,A8,A9,A10;
 end;

theorem Th19:
 for X,Y being non empty set,
  f,g being PartFunc of X,Y st
   for x being Element of X, y being Element of Y holds
    [x,y] in f iff [x,y] in g
 holds f = g
 proof
  let X,Y be non empty set, f,g be PartFunc of X,Y such that
A1: for x being Element of X, y being Element of Y holds
    [x,y] in f iff [x,y] in g;
   reconsider df = dom f, dg = dom g as Subset of X by RELSET_1:12;
     now let x be Element of X;
     hereby assume x in df;
       then [x,f.x] in f & f.x in Y by FUNCT_1:8,PARTFUN1:27;
       then [x,f.x] in g by A1;
      hence x in dg by FUNCT_1:8;
     end;
    assume x in dg;
     then [x,g.x] in g & g.x in Y by FUNCT_1:8,PARTFUN1:27;
     then [x,g.x] in f by A1;
    hence x in df by FUNCT_1:8;
   end;
then A2: df = dg by SUBSET_1:8;
     now let x be Element of X;
    assume x in dom f;
     then [x,f.x] in f & f.x in Y by FUNCT_1:8,PARTFUN1:27;
     then [x,f.x] in g by A1;
    hence f.x = g.x by FUNCT_1:8;
   end;
  hence f = g by A2,PARTFUN1:34;
 end;

theorem Th20:
 for f,g being Function, A,B being set st
  f|A = g|A & f|B = g|B holds f|(A \/ B) = g|(A \/ B)
 proof let f,g be Function, A,B be set;
  assume f|A = g|A & f|B = g|B;
  hence f|(A \/ B) = g|A \/ g|B by RELAT_1:107
      .= g|(A \/ B) by RELAT_1:107;
 end;

theorem
   for X being set, f,g being Function st dom g c= X & g c= f
  holds g c= f|X
 proof let X be set, f,g be Function;
  assume dom g c= X & g c= f;
   then g|dom g c= f|X by RELAT_1:106;
  hence g c= f|X by RELAT_1:97;
 end;

theorem Th22:
 for f being Function, x being set st x in dom f
 holds f|{x} = {[x,f.x]}
 proof let f be Function, x be set such that
A1: x in dom f;
A2: x in {x} by TARSKI:def 1;
     dom(f|{x} qua Function) = dom f /\
 {x} by RELAT_1:90 .= {x} by A1,ZFMISC_1:52;
  hence f|{x} = {[x,(f|{x}).x]} by GRFUNC_1:18
      .= {[x,f.x]} by A2,FUNCT_1:72;
 end;

theorem Th23:
 for f being Function, X being set st X misses dom f
  holds f|X = {}
 proof let f be Function, X be set such that
A1: X /\ dom f = {};
  thus f|X = (f|dom f)|X by RELAT_1:97
          .= f|{} by A1,RELAT_1:100
          .= {} by RELAT_1:110;
 end;

theorem Th24:
 for f,g being Function, x being set st dom f = dom g & f.x = g.x
 holds f|{x} = g|{x}
 proof
  let f,g be Function, x be set such that
A1: dom f = dom g and
A2: f.x = g.x;
   per cases;
   suppose
A3:  x in dom f;
   hence f|{x} = {[x,g.x]} by A2,Th22 .= g|{x} by A1,A3,Th22;
   suppose not x in dom f;
then A4: {x} misses dom f by ZFMISC_1:56;
   hence f|{x} = {} by Th23 .= g|{x} by A1,A4,Th23;
 end;

theorem Th25:
 for f,g being Function, x,y being set st dom f = dom g
  & f.x = g.x & f.y = g.y
 holds f|{x,y} = g|{x,y}
 proof let f,g be Function, x,y be set such that
A1: dom f = dom g and
A2: f.x = g.x and
A3: f.y = g.y;
A4: f|{x} = g|{x} by A1,A2,Th24;
A5: f|{y} = g|{y} by A1,A3,Th24;
     {x,y} = {x} \/ {y} by ENUMSET1:41;
  hence f|{x,y} = g|{x,y} by A4,A5,Th20;
 end;

theorem
   for f,g being Function, x,y,z being set st dom f = dom g
  & f.x = g.x & f.y = g.y & f.z = g.z
 holds f|{x,y,z} = g|{x,y,z}
 proof let f,g be Function, x,y,z be set such that
A1: dom f = dom g and
A2: f.x = g.x & f.y = g.y and
A3: f.z = g.z;
A4: f|{x,y} = g|{x,y} by A1,A2,Th25;
A5: f|{z} = g|{z} by A1,A3,Th24;
     {x,y,z} = {x,y} \/ {z} by ENUMSET1:43;
  hence f|{x,y,z} = g|{x,y,z} by A4,A5,Th20;
 end;

theorem Th27:
 for a,b being set, f being Function st a in dom f & f.a = b
  holds a .--> b c= f
 proof let a,b be set, f be Function;
  assume a in dom f & f.a = b;
   then [a,b] in f by FUNCT_1:8;
   then {[a,b]} c= f by ZFMISC_1:37;
  hence a .--> b c= f by AMI_1:19;
 end;

canceled;

theorem
   for a,b,c,d being set, f being Function st
     a in dom f & c in dom f & f.a = b & f.c = d
  holds (a,c) --> (b,d) c= f
 proof let a,b,c,d be set, f be Function;
  assume
A1: a in dom f & c in dom f & f.a = b & f.c = d;
  per cases;
  suppose
A2:  a <> c;
     [a,b] in f & [c,d] in f by A1,FUNCT_1:8;
   then { [a,b], [c,d]} c= f by ZFMISC_1:38;
  hence (a,c) --> (b,d) c= f by A2,FUNCT_4:71;
  suppose a = c;
   then (a,c) --> (b,d) = c .--> d by AMI_1:20;
  hence (a,c) --> (b,d) c= f by A1,Th27;
 end;

begin :: Some Remarks on AMI-Struct

reserve N for set;

canceled;

theorem Th31:
 for S being AMI-Struct over N,
     p being FinPartState of S
  holds p in FinPartSt S
 proof let S be AMI-Struct over N;
  let p be FinPartState of S;
A1:  FinPartSt S =
    { q where q is Element of sproduct the Object-Kind of S: q is finite }
     by AMI_1:def 23;
     p is finite by AMI_1:def 24;
  hence p in FinPartSt S by A1;
 end;

definition let N be set; let S be AMI-Struct over N;
 cluster FinPartSt S -> non empty;
 coherence by Th31;
end;

theorem Th32:
 for S being AMI-Struct over N,
     p being Element of FinPartSt S
  holds p is FinPartState of S
 proof let S be AMI-Struct over N;
  let p be Element of FinPartSt S;
A1:  FinPartSt S =
    { q where q is Element of sproduct the Object-Kind of S: q is finite }
     by AMI_1:def 23;
     p in FinPartSt S;
   then ex q being Element of sproduct the Object-Kind of S
     st q = p & q is finite by A1;
  hence p is FinPartState of S by AMI_1:def 24;
 end;

theorem Th33:
 for S being AMI-Struct over N,
     F1,F2 being PartFunc of FinPartSt S, FinPartSt S
  st for p,q being FinPartState of S holds
   [p,q] in F1 iff [p,q] in F2
  holds F1 = F2
 proof
  let S be AMI-Struct over N,
      F1,F2 be PartFunc of FinPartSt S, FinPartSt S such that
A1: for p,q being FinPartState of S holds [p,q] in F1 iff [p,q] in F2;
     now let p,q be Element of FinPartSt S;
     reconsider p' = p, q' = q as FinPartState of S by Th32;
       [p',q'] in F1 iff [p',q'] in F2 by A1;
    hence [p,q] in F1 iff [p,q] in F2;
   end;
  hence F1 = F2 by Th19;
 end;

scheme EqFPSFunc{ N() -> non empty with_non-empty_elements set,
    S() -> AMI-Struct over N(), P[set,set],
    IT1,IT2()->PartFunc of FinPartSt S(), FinPartSt S()}:
 IT1() = IT2()
 provided
A1: for p,q being FinPartState of S() holds [p,q] in IT1() iff P[p,q] and
A2: for p,q being FinPartState of S() holds [p,q] in IT2() iff P[p,q]
 proof
     now let p,q be FinPartState of S();
       [p,q] in IT1() iff P[p,q] by A1;
    hence [p,q] in IT1() iff [p,q] in IT2() by A2;
   end;
  hence thesis by Th33;
 end;

definition let N be with_non-empty_elements set;
   let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
   let l be Instruction-Location of S;
 func Start-At l -> FinPartState of S equals
:Def12: IC S .--> l;
 correctness
  proof ObjectKind IC S = the Instruction-Locations of S by AMI_1:def 11;
   hence thesis by AMI_1:59;
  end;
end;

reserve N for with_non-empty_elements set;

theorem
   for S being IC-Ins-separated definite (non empty non void AMI-Struct over N)
 for l being Instruction-Location of S
  holds dom(Start-At l) = {IC S}
proof
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let l be Instruction-Location of S;
    Start-At l = IC S .--> l by Def12
    .= {IC S} --> l by CQC_LANG:def 2;
 hence thesis by FUNCOP_1:19;
end;

definition let N be set; let S be AMI-Struct over N;
 let IT be FinPartState of S;
 attr IT is programmed means
:Def13: dom IT c= the Instruction-Locations of S;
end;

definition let N be set; let S be AMI-Struct over N;
 cluster programmed FinPartState of S;
 existence
  proof
      {} in sproduct the Object-Kind of S & {} is finite by AMI_1:26;
    then reconsider Z = {} as FinPartState of S by AMI_1:def 24;
   take Z;
    thus dom Z c= the Instruction-Locations of S by RELAT_1:60,XBOOLE_1:2;
  end;
end;

theorem
  for N being set for S being AMI-Struct over N
 for p1,p2 being programmed FinPartState of S
  holds p1 +* p2 is programmed
proof let N be set, S be AMI-Struct over N;
 let p1,p2 be programmed FinPartState of S;
A1: dom p1 c= the Instruction-Locations of S &
   dom p2 c= the Instruction-Locations of S by Def13;
    dom(p1 +* p2) = dom p1 \/ dom p2 by FUNCT_4:def 1;
 hence dom(p1 +* p2) c= the Instruction-Locations of S by A1,XBOOLE_1:8;
end;

theorem Th36:
 for S being non void AMI-Struct over N, s being State of S holds
  dom s = the carrier of S
 proof let S be non void AMI-Struct over N, s be State of S;
  thus dom s = dom the Object-Kind of S by CARD_3:18
      .= the carrier of S by FUNCT_2:def 1;
 end;

theorem Th37:
 for S being AMI-Struct over N, p being FinPartState of S holds
  dom p c= the carrier of S
 proof let S be AMI-Struct over N, p be FinPartState of S;
     sproduct the Object-Kind of S <> {};
   then dom p c= dom the Object-Kind of S by AMI_1:25;
  hence dom p c= the carrier of S by FUNCT_2:def 1;
 end;

theorem
  for S being steady-programmed IC-Ins-separated definite
   (non empty non void AMI-Struct over N)
 for p being programmed FinPartState of S
 for s being State of S st p c= s
 for k holds p c= (Computation s).k
proof
 let S be steady-programmed IC-Ins-separated definite
   (non empty non void AMI-Struct over N);
 let p be programmed FinPartState of S, s be State of S such that
A1: p c= s;
 let k;
    dom s = the carrier of S by Th36 .= dom((Computation s).k) by Th36;
  then A2: dom p c= dom((Computation s).k) by A1,GRFUNC_1:8;
A3: dom p c= the Instruction-Locations of S by Def13;
    now let x be set;
   assume
A4:  x in dom p;
    then s.x = ((Computation s).k).x by A3,AMI_1:54;
   hence p.x = ((Computation s).k).x by A1,A4,GRFUNC_1:8;
  end;
 hence p c= (Computation s).k by A2,GRFUNC_1:8;
end;

definition let N;
 let S be IC-Ins-separated (non empty non void AMI-Struct over N);
 let s be State of S, l be Instruction-Location of S;
 pred s starts_at l means
    IC s = l;
end;

definition let N;
 let S be IC-Ins-separated halting (non empty non void AMI-Struct over N);
 let s be State of S, l be Instruction-Location of S;
 pred s halts_at l means
:Def15:  s.l = halt S;
end;

theorem Th39:
 for S being non void AMI-Struct over N, p being FinPartState of S
  ex s being State of S st p c= s
 proof let S be non void AMI-Struct over N, p be FinPartState of S;
   consider h being State of S;
     sproduct the Object-Kind of S <> {};
   then reconsider s = h +* p as State of S by AMI_1:29;
  take s;
  thus p c= s by FUNCT_4:26;
 end;

definition let N;
  let S be definite IC-Ins-separated (non empty non void AMI-Struct over N);
 let p be FinPartState of S such that
A1: IC S in dom p;
 func IC p -> Instruction-Location of S equals
:Def16:  p.IC S;
 coherence
  proof
    consider s being State of S such that
A2:   p c= s by Th39;
      IC s is Instruction-Location of S;
    then s.IC S is Instruction-Location of S by AMI_1:def 15;
   hence thesis by A1,A2,GRFUNC_1:8;
  end;
end;

definition let N;
 let S be definite IC-Ins-separated (non empty non void AMI-Struct over N);
 let p be FinPartState of S, l be Instruction-Location of S;
 pred p starts_at l means
    IC S in dom p & IC p = l;
end;

definition let N;
 let S be definite IC-Ins-separated halting
  (non empty non void AMI-Struct over N);
 let p be FinPartState of S, l be Instruction-Location of S;
 pred p halts_at l means
    l in dom p & p.l = halt S;
end;

theorem Th40:
 for S being IC-Ins-separated
 definite steady-programmed halting (non empty non void AMI-Struct over N),
  s being State of S holds
  s is halting iff ex k st s halts_at IC (Computation s).k
 proof
  let S be IC-Ins-separated
 definite steady-programmed halting (non empty non void AMI-Struct over N);
  let s be State of S;
  hereby assume s is halting;
    then consider k such that
A1:   CurInstr((Computation s).k) = halt S by AMI_1:def 20;
   take k;
      s.IC (Computation s).k
      = (Computation s).k.IC ((Computation s).k) by AMI_1:54
     .= halt S by A1,AMI_1:def 17;
   hence s halts_at IC (Computation s).k by Def15;
  end;
  given k such that
A2: s halts_at IC (Computation s).k;
  take k;
  thus CurInstr((Computation s).k)
     = (Computation s).k.IC ((Computation s).k) by AMI_1:def 17
    .= s.IC (Computation s).k by AMI_1:54
    .= halt S by A2,Def15;
 end;

theorem
   for S being IC-Ins-separated
 definite steady-programmed halting (non empty non void AMI-Struct over N),
  s being State of S, p being FinPartState of S,
  l being Instruction-Location of S st p c= s & p halts_at l
   holds s halts_at l
proof
 let S be IC-Ins-separated
 definite steady-programmed halting (non empty non void AMI-Struct over N);
 let s be State of S, p be FinPartState of S,
     l be Instruction-Location of S such that
A1: p c= s;
 assume l in dom p & p.l = halt S;
 hence s.l = halt S by A1,GRFUNC_1:8;
end;

theorem Th42:
 for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N),
     s being State of S, k st s is halting
  holds Result s = (Computation s).k iff s halts_at IC (Computation s).k
 proof
  let S be halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N);
  let s be State of S, k such that
A1: s is halting;
  hereby assume Result s = (Computation s).k;
   then ex i st (Computation s).k = (Computation s).i &
       CurInstr((Computation s).k) = halt S by A1,AMI_1:def 22;
    then (Computation s).k.IC (Computation s).k = halt S by AMI_1:def 17;
    then s.IC (Computation s).k = halt S by AMI_1:54;
   hence s halts_at IC (Computation s).k by Def15;
  end;
  assume s.IC (Computation s).k = halt S;
   then (Computation s).k.IC (Computation s).k = halt S by AMI_1:54;
   then CurInstr((Computation s).k) = halt S by AMI_1:def 17;
  hence Result s = (Computation s).k by A1,AMI_1:def 22;
 end;

theorem
   for S being steady-programmed IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     s being State of S, p being programmed FinPartState of S, k
  holds p c= s iff p c= (Computation s).k
 proof
  let S be steady-programmed IC-Ins-separated
       definite (non empty non void AMI-Struct over N);
  let s be State of S, p be programmed FinPartState of S, k;
    dom s = the carrier of S & dom((Computation s).k) = the carrier of S by
Th36
;
   then A1: dom p c= dom s & dom p c= dom((Computation s).k) by Th37;
A2: dom p c= the Instruction-Locations of S by Def13;
     now
    hereby assume
A3:  for x being set st x in dom p holds p.x = s.x;
     let x be set;
     assume
A4:   x in dom p;
     hence (Computation s).k.x = s.x by A2,AMI_1:54
       .= p.x by A3,A4;
    end;
    assume
A5:  for x being set st x in dom p holds p.x = (Computation s).k.x;
    let x be set;
    assume
A6:   x in dom p;
    hence s.x = (Computation s).k.x by A2,AMI_1:54
     .= p.x by A5,A6;
   end;
  hence p c= s iff p c= (Computation s).k by A1,GRFUNC_1:8;
 end;

theorem Th44:
 for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N),
     s being State of S, k st s halts_at IC (Computation s).k
  holds Result s = (Computation s).k
 proof
  let S be halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N),
      s be State of S, k;
  assume
A1: s halts_at IC (Computation s).k;
   then s is halting by Th40;
  hence Result s = (Computation s).k by A1,Th42;
 end;

theorem Th45:
 i <= j implies
  for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N)
  for s being State of S st s halts_at IC (Computation s).i
   holds s halts_at IC (Computation s).j
 proof assume
A1: i <= j;
  let S be halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N);
  let s be State of S;
  assume
A2: s.IC (Computation s).i = halt S;
      CurInstr((Computation s).i) = (Computation s).i.IC (Computation s).i
          by AMI_1:def 17
      .= halt S by A2,AMI_1:54;
  hence s.IC (Computation s).j = halt S by A1,A2,AMI_1:52;
 end;

theorem :: AMI_1:46
   i <= j implies
  for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N)
  for s being State of S st s halts_at IC (Computation s).i
   holds (Computation s).j = (Computation s).i
 proof assume
A1: i <= j;
  let S be halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N),
      s be State of S;
  assume
A2:  s halts_at IC (Computation s).i;
   then s halts_at IC (Computation s).j by A1,Th45;
  hence (Computation s).j = Result s by Th44
             .= (Computation s).i by A2,Th44;
 end;

theorem :: AMI_2:46
   for S being steady-programmed IC-Ins-separated
 halting definite (non empty non void AMI-Struct over N)
 for s being State of S st ex k st s halts_at IC (Computation s).k
 for i holds Result s = Result (Computation s).i
proof
 let S be steady-programmed IC-Ins-separated
 halting definite (non empty non void AMI-Struct over N),
     s be State of S;
 given k such that
A1: s halts_at IC (Computation s).k;
 let i;
    s.IC (Computation s).k = halt S by A1,Def15;
 hence Result s = Result (Computation s).i by AMI_1:57;
end;

theorem
   for S being steady-programmed IC-Ins-separated
 definite halting (non empty non void AMI-Struct over N)
 for s being State of S,l being Instruction-Location of S,k holds
  s halts_at l iff (Computation s).k halts_at l
 proof
  let S be steady-programmed IC-Ins-separated
 definite halting (non empty non void AMI-Struct over N),
      s be State of S, l be Instruction-Location of S,k;
  hereby assume s halts_at l;
    then s.l = halt S by Def15;
    then (Computation s).k.l = halt S by AMI_1:54;
   hence (Computation s).k halts_at l by Def15;
  end;
  assume (Computation s).k.l = halt S;
  hence s.l = halt S by AMI_1:54;
 end;

theorem
   for S being definite IC-Ins-separated (non empty non void AMI-Struct over N)
,
     p being FinPartState of S, l being Instruction-Location of S
  st p starts_at l
 for s being State of S st p c= s holds s starts_at l
 proof
  let S be definite IC-Ins-separated (non empty non void AMI-Struct over N),
      p be FinPartState of S, l be Instruction-Location of S such that
A1: IC S in dom p & IC p = l;
  let s be State of S such that
A2: p c= s;
  thus IC s = s.IC S by AMI_1:def 15
   .= p.IC S by A1,A2,GRFUNC_1:8
   .= l by A1,Def16;
 end;

theorem
   for S being IC-Ins-separated definite (non empty non void AMI-Struct over N)
,
     l being Instruction-Location of S
  holds (Start-At l).IC S = l
 proof
  let S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
      l be Instruction-Location of S;
  thus (Start-At l).IC S = (IC S .--> l).IC S by Def12
          .= l by CQC_LANG:6;
 end;

definition let N;
 let S be definite IC-Ins-separated (non empty non void AMI-Struct over N);
 let l be Instruction-Location of S, I be Element of the Instructions of S;
 redefine func l .--> I -> programmed FinPartState of S;
  coherence
   proof ObjectKind l = the Instructions of S by AMI_1:def 14;
     then reconsider L = l .--> I as FinPartState of S by AMI_1:59;
        dom L = {l} by CQC_LANG:5;
     then dom L c= the Instruction-Locations of S by ZFMISC_1:37;
    hence thesis by Def13;
   end;
end;

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 by Def1;
      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 AMI_2:def 4,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 by Def1;
   reconsider l' = l as Element of SCM-Instr-Loc by Def1;
A2: Exec(i,s) = SCM-Exec.c.S by Def1,AMI_1:def 7
    .= SCM-Exec-Res(c,S) by AMI_2:def 17;
     now per cases by A1,XBOOLE_0:def 2;
    case c in { [SCM-Halt,{}] };
   then c = [SCM-Halt,{}] by TARSKI:def 1;
then A3: c`2 = {} by MCART_1:7;
A4: now let l be 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 A3,FINSEQ_3:38;
   end;
A5: now let l be Nat; let mk be Element of SCM-Instr-Loc;
    assume c = [ l, <*mk*>];
     then c`2 = <*mk*> by MCART_1:7;
    hence contradiction by A3,TREES_1:4;
   end;
  now let l be 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 A3,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 A4,A5;
     hence SCM-Exec-Res(c,S).l' = S.l' by AMI_2:def 16;
    case c in { [Y,<*a2*>] : Y = 6 };
     then consider Y,a2 such that
A6:    c = [Y,<*a2*>] & Y = 6;
     thus SCM-Exec-Res(c,S).l' = SCM-Chg(S,c jump_address).l' by A6,AMI_2:def
16
        .= S.l' by AMI_2:18;
    case c in { [K,<*a1,b1*>] : K in { 7,8 } };
     then consider K,a1,b1 such that
A7:    c = [K,<*a1,b1*>] & K in { 7,8 };
        now per cases by A7,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 A7,AMI_2:def 16
          .= S.l' by AMI_2:18;
       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 A7,AMI_2:def 16
          .= S.l' by AMI_2:18;
      end;
     hence SCM-Exec-Res(c,S).l' = S.l';
    case c in { [T,<*b2,c1*>] : T in { 1,2,3,4,5} };
      then consider T,b2,c1 such that
A8:     c = [T,<*b2,c1*>] & T in { 1,2,3,4,5};
        now per cases by A8,ENUMSET1:23;
       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 A8,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;
       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 A8,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;
       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 A8,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;
       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 A8,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;
       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 A8,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;
     hence SCM-Exec-Res(c,S).l' = S.l';
   end;
  hence s.l = Exec(i,s).l by A2;
 end;

theorem
  SCM is realistic by Def1,AMI_1:def 21,AMI_2:6;

definition
 cluster SCM -> steady-programmed realistic;
 coherence
  proof
       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;
   hence thesis by Def1,AMI_1:def 21,AMI_2:6;
  end;
end;

definition let k be natural number;
 func dl.k -> Data-Location equals
:Def19:  2*k +1;
 coherence
  proof
    reconsider k as Nat by ORDINAL2:def 21;
    reconsider d = 2*k+1 as Object of SCM by Def1;
      2*k +1 in SCM-Data-Loc by AMI_2:def 2;
    then d is Data-Location by Def2;
   hence thesis;
  end;
 func il.k -> Instruction-Location of SCM equals
:Def20:  2*k +2;
 coherence
  proof
    reconsider k as Nat by ORDINAL2:def 21;
      SCM-Instr-Loc = { 2*i : i > 0 } & k+1 > 0 by AMI_2:def 3,NAT_1:19;
    then 2*(k +1) in SCM-Instr-Loc;
    then 2*k +2*1 in SCM-Instr-Loc by XCMPLX_1:8;
   hence thesis by Def1;
  end;
end;

reserve i,j,k for natural number;

theorem
   i <> j implies dl.i <> dl.j
 proof
A1: dl.j = 2*j +1 & dl.i = 2*i + 1 by Def19;
  assume i <> j;
  then 2*i <> 2*j by XCMPLX_1:5;
  hence dl.i <> dl.j by A1,XCMPLX_1:2;
 end;

theorem
   i <> j implies il.i <> il.j
 proof
A1: il.j = 2*j +2 & il.i = 2*i + 2 by Def20;
  assume i <> j;
  then 2*i <> 2*j by XCMPLX_1:5;
  hence il.i <> il.j by A1,XCMPLX_1:2;
 end;

theorem
   Next il.k = il.(k+1)
 proof
   reconsider loc = il.k as Element of SCM-Instr-Loc by Def1;
  thus Next il.k = Next loc by Th6
     .= loc +2 by AMI_2:def 15
     .= 2*k+2*1 +2 by Def20
     .= 2*(k+1)+2 by XCMPLX_1:8
     .= il.(k+1) by Def20;
 end;

theorem Th55:
 for l being Data-Location holds ObjectKind l = INT
  proof let l be Data-Location;
A1:  l in SCM-Data-Loc by Def2;
   thus ObjectKind l = (the Object-Kind of SCM).l by AMI_1:def 6
     .= INT by A1,Def1,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
A1: il.j = 2*j +2 & dl.i = 2*i + 1 by Def19,Def20;
     now assume 2*j + 2, 2*i + 1 are_congruent_mod 2;
     then 2*j, 1 + 2*i are_congruent_mod 2 by INT_1:42;
     then 1 + 2*i, 2*j are_congruent_mod 2 by INT_1:35;
     then 1, 2*j - 2*i are_congruent_mod 2 by INT_1:40;
     then A2:    1, 2*(j - i) are_congruent_mod 2 by XCMPLX_1:40;
        2*(j - i), 0 are_congruent_mod 2 by Th18;
     then 1, 0 are_congruent_mod 2 by A2,INT_1:36;
     then consider k being Integer such that
A3:    2*k = 1 - 0 by INT_1:def 3;
    thus contradiction by A3,INT_1:22;
   end;
  hence dl.i <> il.j by A1,INT_1:32;
 end;

theorem
   IC SCM <> dl.i & IC SCM <> il.i
 proof
  hereby assume IC SCM = dl.i;
    then 0 = 2*i + 1 by Def19,Th4;
   hence contradiction;
  end;
  assume IC SCM = il.i;
    then 0 = 2*i + (1 + 1) by Def20,Th4
      .= 2*i + 1 + 1 by XCMPLX_1:1;
  hence contradiction;
 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;

theorem
   [0,{}] is Instruction of SCM by Def1,AMI_2:2;

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;

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

Back to top