:: On the Composition of Macro Instructions of Standard Computers
::  by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000 Association of Mizar Users

environ

 vocabularies AMI_3, ORDINAL2, ARYTM, AMI_1, RELAT_1, BOOLE, FUNCT_1, FUNCT_4,
      FINSET_1, TARSKI, CARD_1, ARYTM_1, FRAENKEL, SETFAM_1, CARD_3, PRALG_2,
      FINSEQ_2, FINSEQ_1, CAT_1, FUNCOP_1, GOBOARD5, WAYBEL_0, AMISTD_1,
      MCART_1, AMI_5, UNIALG_1, REALSET1, CARD_5, FRECHET, PRE_TOPC, RELOC,
      FUNCT_7, ORDINAL1, SQUARE_1, SCMFSA6A, AMISTD_2, MEMBERED;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ZFMISC_1, MCART_1, SETFAM_1,
      MEMBERED, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2, FRAENKEL, REALSET1,
      FUNCT_4, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1,
      FINSEQ_2, FUNCOP_1, BINARITH, FUNCT_7, STRUCT_0, AMI_1, PRE_CIRC,
      AMISTD_1;
 constructors WELLORD2, XXREAL_0, NAT_1, REALSET1, BINARITH, PRE_CIRC, PRALG_2,
      AMISTD_1, INT_1;
 registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1,
      FRAENKEL, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, CARD_3,
      REALSET1, PRE_CIRC, FUNCT_7, STRUCT_0, AMI_1, AMISTD_1, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions TARSKI, RELAT_1, FUNCT_1, WELLORD2, FRAENKEL, REAL_1, FUNCT_7,
      AMI_1, YELLOW_8, AMISTD_1, XBOOLE_0, FUNCOP_1, CARD_3;
 theorems AMI_1, BINARITH, CARD_1, CARD_2, AMISTD_1, FUNCOP_1, FINSEQ_1,
      FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, FUNCT_4, GRFUNC_1, INT_1, MCART_1,
      CATALG_1, NAT_1, PRE_CIRC, REAL_1, REALSET1, RELAT_1, SETFAM_1, TARSKI,
      YELLOW_8, ZFMISC_1, CARD_3, ORDINAL1, XBOOLE_0, XBOOLE_1, FINSET_1,
      XREAL_1, XXREAL_0, DOMAIN_1;
 schemes FUNCT_7, FINSEQ_1, CLASSES1;

begin

reserve k, m for natural number,
  x, X for set,
  N for with_non-empty_elements set,
  IL for non empty set;

registration
  let D be set;
  cluster -> functional FinSequenceSet of D;
  coherence;
end;

registration
  let i be Element of NAT, D be set;
  cluster i-tuples_on D -> with_common_domain;
  coherence
  proof
    set S = i-tuples_on D;
    let f, g be Function such that
A1: f in S & g in S;
    S = { s where s is Element of D*: len s = i } by FINSEQ_2:def 4;
    then (ex s being Element of D* st f = s & len s = i) &
    (ex s being Element of D* st g = s & len s = i) by A1;
    hence dom f = dom g by FINSEQ_3:31;
  end;
end;

registration
  let i be Element of NAT, D be set;
  cluster i-tuples_on D -> product-like;
  coherence
  proof
    set S = i-tuples_on D;
    per cases;
    suppose D = {} & i = 0;
      then S = { <*>D } by FINSEQ_2:112
        .= {{}};
      hence thesis by CARD_3:19;
    end;
    suppose D = {} & i <> 0;
      then
A1:   S = {} by CATALG_1:7;
      take f = 0 .--> {};
      rng f = {{}} by FUNCOP_1:14;
      then {} in rng f by TARSKI:def 1;
      hence thesis by A1,CARD_3:37;
    end;
    suppose D <> {};
      then reconsider D as non empty set;
      set S = i-tuples_on D;
      take product" S;
      S = product product" S
      proof
        thus S c= product product" S by CARD_3:94;
        let x be set;
        assume x in product product" S;
        then consider g being Function such that
A2:     x = g and
A3:     dom g = dom product" S and
A4:     for z being set st z in dom product" S holds g.z in (product" S).z
        by CARD_3:def 5;
A5:     S = { s where s is Element of D*: len s = i } by FINSEQ_2:def 4;
        consider s being Element of S;
        s in S;
        then consider t being Element of D* such that
A6:     s = t and
A7:     len t = i by A5;
A8:     dom g = DOM S by A3,CARD_3:92
          .= dom s by CARD_3:def 12;
        dom s = Seg len t by A6,FINSEQ_1:def 3;
        then
A9:     g is FinSequence by A8,FINSEQ_1:def 2;
        rng g c= D
        proof
          let y be set;
          assume y in rng g;
          then consider a being set such that
A10:      a in dom g and
A11:      g.a = y by FUNCT_1:def 5;
          g.a in (product" S).a by A3,A4,A10;
          then g.a in pi(S,a) by A3,A10,CARD_3:def 13;
          then consider f being Function such that
A12:      f in S and
A13:      g.a = f.a by CARD_3:def 6;
          consider w being Element of D* such that
A14:      f = w and len w = i by A5,A12;
A15:      rng w c= D by FINSEQ_1:def 4;
          dom g = dom w by A8,A12,A14,CARD_3:def 10;
          then w.a in rng w by A10,FUNCT_1:def 5;
          hence y in D by A11,A13,A14,A15;
        end;
        then reconsider g as FinSequence of D by A9,FINSEQ_1:def 4;
A16:    g in D* by FINSEQ_1:def 11;
        len g = i by A6,A7,A8,FINSEQ_3:31;
        hence thesis by A2,A5,A16;
      end;
      hence thesis;
    end;
  end;
end;

Lm1: -1 < k
proof
  -1 < 0 & 0 <= k;
  hence thesis;
end;

Lm2: for a, b, c being Element of NAT st 1 <= a & 2 <= b holds
k < a - 1 or a <= k & k <= a + b - 3 or k = a + b - 2 or
a + b - 2 < k or k = a - 1
proof
  let a, b, c be Element of NAT such that
A1: 1 <= a and
A2: 2 <= b and
A3: a - 1 <= k and
A4: (a > k or k > a + b - 3) and
A5: k <> a + b - 2 and
A6: k <= a + b - 2;
A7: a - 1 is Element of NAT by A1,INT_1:18;
  now per cases by A4;
    case k < a;
      then k < a - 1 + 1;
      hence k <= a - 1 by A7,NAT_1:13;
    end;
    case
A8:   a + b - 3 < k;
      1 + 2 <= a + b by A1,A2,XREAL_1:9;
      then
A9:   a + b - 3 is Element of NAT by INT_1:18;
      k < a + b - 3 + 1 by A5,A6,REAL_1:def 5;
      hence k <= a - 1 by A8,A9,NAT_1:13;
    end;
  end;
  hence a - 1 = k by A3,XXREAL_0:1;
end;

begin  :: Properties of AMI-Struct

canceled 10;

theorem
  for IL,N being set, S being AMI-Struct over IL,N,
  F being FinPartState of S holds F \ X is FinPartState of S by CARD_3:80;

theorem Th12:
  for S being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  F being programmed FinPartState of S
  holds F \ X is programmed FinPartState of S
proof
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  F be programmed FinPartState of S;
  reconsider G = F \ X as FinPartState of S by CARD_3:80;
  per cases;
  suppose G is empty;
    then reconsider H = G as empty FinPartState of S;
    H is programmed;
    hence thesis;
  end;
  suppose G is non empty;
    then reconsider G as non empty FinPartState of S;
    G is programmed
    proof
A1:   dom G c= dom F by GRFUNC_1:8;
      dom F c= IL by AMI_1:def 40;
      hence dom G c= IL by A1,XBOOLE_1:1;
    end;
    hence thesis;
  end;
end;

definition
  let IL be non empty set;
  canceled 2;
  let N be with_non-empty_elements set, S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  i1, i2 be Instruction-Location of S,
  I1, I2 be Element of the Instructions of S;
  redefine func (i1,i2) --> (I1,I2) -> FinPartState of S;
  coherence
  proof
    ObjectKind i1 = the Instructions of S &
    ObjectKind i2 = the Instructions of S by AMI_1:def 14;
    hence thesis by AMI_1:58;
  end;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  let S be halting (stored-program AMI-Struct over IL,N);
  cluster halting Instruction of S;
  existence
  proof
    take halt S;
    thus thesis;
  end;
end;

theorem Th13:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being lower programmed FinPartState of S,
  G being programmed FinPartState of S st dom F = dom G holds G is lower
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower programmed FinPartState of S, G be programmed FinPartState of S;
  assume dom F = dom G;
  hence for l being Instruction-Location of S st l in dom G
  holds for m being Instruction-Location of S st m <= l holds m in dom G
  by AMISTD_1:def 20;
end;

theorem Th14:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being lower programmed FinPartState of S,
  f being Instruction-Location of S st f in dom F holds locnum f < card F
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower programmed FinPartState of S,
  f be Instruction-Location of S such that
A1: f in dom F;
  f = il.(S,locnum f) by AMISTD_1:def 13;
  hence thesis by A1,AMISTD_1:50;
end;

theorem Th15:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being lower programmed FinPartState of S
  holds dom F = { il.(S,k) where k is Element of NAT: k < card F }
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower programmed FinPartState of S;
A1: dom F c= NAT by AMI_1:def 40;
  hereby
    let x be set;
    assume
A2: x in dom F;
    then reconsider f = x as Instruction-Location of S by A1,AMI_1:def 4;
A3: locnum f < card F by A2,Th14;
    reconsider i = locnum f as Element of NAT;
    f = il.(S,i) by AMISTD_1:def 13;
    hence x in { il.(S,k) where k is Element of NAT: k < card F } by A3;
  end;
  let x be set;
  assume x in { il.(S,k) where k is Element of NAT: k < card F };
  then ex k being Element of NAT st x = il.(S,k) & k < card F;
  hence thesis by AMISTD_1:50;
end;

definition
  let IL,N be set;
  let S be AMI-Struct over IL,N;
  let I be Element of the Instructions of S;
  func AddressPart I equals

  I`2;
  coherence;
end;

definition
  let IL,N be set;
  let S be standard-ins AMI-Struct over IL,N;
  let I be Element of the Instructions of S;
  redefine func AddressPart I -> FinSequence of (union N) \/ the carrier of S;
  coherence
  proof
A1: the Instructions of S c= [: NAT, ((union N) \/ the carrier of S)* :]
    by AMI_1:def 32;
    I in the Instructions of S;
    then AddressPart I in ((union N) \/ the carrier of S)* by A1,MCART_1:10;
    hence thesis by FINSEQ_1:def 11;
  end;
end;

theorem Th16:
  for N being set, S being standard-ins AMI-Struct over IL,N,
  I, J being Element of the Instructions of S holds
  InsCode I = InsCode J & AddressPart I = AddressPart J implies I = J
proof
  let N be set, S be standard-ins AMI-Struct over IL,N,
  I, J be Element of the Instructions of S;
A1: the Instructions of S c= [: NAT, ((union N) \/ the carrier of S)* :]
  by AMI_1:def 32;
A2: I in the Instructions of S;
  J in the Instructions of S;
  hence thesis by A1,A2,DOMAIN_1:12;
end;

definition
  let IL,N be set;
  let S be standard-ins AMI-Struct over IL,N;
  attr S is homogeneous means
  :Def4:
  for I, J being Instruction of S st InsCode I = InsCode J holds
  dom AddressPart I = dom AddressPart J;
end;

theorem Th17:
  for I being Instruction of STC N holds AddressPart I = 0
proof
  let I be Instruction of STC N;
  the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
  then I = [0,0] or I = [1,0] by TARSKI:def 2;
  hence AddressPart I = 0 by MCART_1:def 2;
end;

definition
  let IL,N be set;
  let S be standard-ins AMI-Struct over IL,N;
  let T be InsType of S;
  func AddressParts T equals
  { AddressPart I where I is Instruction of S: InsCode I = T };
  coherence;
end;

registration
  let IL,N be set;
  let S be standard-ins AMI-Struct over IL,N;
  let T be InsType of S;
  cluster AddressParts T -> functional;
  coherence
  proof
    let f be set;
    assume f in AddressParts T;
    then ex I being Instruction of S st f = AddressPart I & InsCode I = T;
    hence f is Function;
  end;
end;

definition
  let IL be non empty set;
  let N be with_non-empty_elements set,
  S be IC-Ins-separated definite standard-ins
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of S;
  attr I is with_explicit_jumps means
  :Def6:
  for f being set st f in JUMP I holds
  ex k being set st k in dom AddressPart I & f = (AddressPart I).k &
  (product" AddressParts InsCode I).k = IL;
  attr I is without_implicit_jumps means
  :Def7:
  for f being set st
  ex k being set st k in dom AddressPart I & f = (AddressPart I).k &
  (product" AddressParts InsCode I).k = IL holds f in JUMP I;
end;

definition
  let IL be non empty set;
  let N be with_non-empty_elements set,
  S be standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N);
  attr S is with_explicit_jumps means
  :Def8:
  for I being Instruction of S holds I is with_explicit_jumps;
  attr S is without_implicit_jumps means
  :Def9:
  for I being Instruction of S holds I is without_implicit_jumps;
end;

registration
  let N be with_non-empty_elements set;
  cluster standard -> (IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N));
  coherence;
end;

registration
  let N be with_non-empty_elements set;
  cluster standard standard-ins (IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N));
  existence
  proof
    take STC N;
    thus thesis;
  end;
end;

theorem Th18:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I being Instruction of S
  st for f being Instruction-Location of S holds NIC(I,f)={NextLoc f}
  holds JUMP I is empty
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of S;
  assume
A1: for f being Instruction-Location of S holds NIC(I,f)={NextLoc f};
  set p=1, q=2;
  reconsider p,q as Instruction-Location of S by AMI_1:def 4;
  set X = { NIC(I,f) where f is Instruction-Location of S:
  not contradiction };
  assume not thesis;
  then consider x being set such that
A3: x in meet X by XBOOLE_0:def 1;
  NIC(I,p) = {NextLoc p} & NIC(I,q) = {NextLoc q} by A1;
  then {NextLoc p} in X & {NextLoc q} in X;
  then x in {NextLoc p} & x in {NextLoc q} by A3,SETFAM_1:def 1;
  then x = NextLoc p & x = NextLoc q by TARSKI:def 1;
  hence contradiction by AMISTD_1:36;
end;

registration
  let N be with_non-empty_elements set, I be Instruction of STC N;
  cluster JUMP I -> empty;
  coherence
  proof
    per cases by AMISTD_1:22;
    suppose InsCode I = 0;
      then for f being Instruction-Location of STC N holds NIC(I,f)={f}
      by AMISTD_1:15,20;
      hence thesis by AMISTD_1:14;
    end;
    suppose InsCode I = 1;
      then for f being Instruction-Location of STC N holds NIC(I,f)={NextLoc f
      } by AMISTD_1:39;
      hence thesis by Th18;
    end;
  end;
end;

definition
  let IL,N be set;
  let S be standard-ins AMI-Struct over IL,N;
  canceled;
  attr S is regular means
  :Def11:
  for T being InsType of S holds AddressParts T is product-like;
end;

registration
  let IL,N be set;
  cluster regular -> homogeneous (standard-ins AMI-Struct over IL,N);
  coherence
  proof
    let S be standard-ins AMI-Struct over IL,N such that
A1: for T being InsType of S holds AddressParts T is product-like;
    let I, J be Instruction of S such that
A2: InsCode I = InsCode J;
    AddressParts InsCode I is product-like by A1;
    then consider f being Function such that
A3: AddressParts InsCode I = product f by CARD_3:def 14;
A4: AddressPart I in AddressParts InsCode I &
    AddressPart J in AddressParts InsCode I by A2;
    hence dom AddressPart I = dom f by A3,CARD_3:18
      .= dom AddressPart J by A3,A4,CARD_3:18;
  end;
end;

theorem Th19:
  for T being InsType of STC N holds AddressParts T = {0}
proof
  let T be InsType of STC N;
  set A = { AddressPart I where I is Instruction of STC N: InsCode I = T };
  {0} = A
  proof
    hereby
      let a be set;
      assume a in {0};
      then
A1:   a = 0 by TARSKI:def 1;
A2:   the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
      then
A3:   InsCodes STC N = {0,1} by RELAT_1:24;
      per cases by A3,TARSKI:def 2;
      suppose
A4:     T = 0;
        reconsider I = [0,0] as Instruction of STC N by A2,TARSKI:def 2;
A5:     AddressPart I = 0 by Th17;
        InsCode I = 0 by MCART_1:def 1;
        hence a in A by A1,A4,A5;
      end;
      suppose
A6:     T = 1;
        reconsider I = [1,0] as Instruction of STC N by A2,TARSKI:def 2;
A7:     AddressPart I = 0 by Th17;
        InsCode I = 1 by MCART_1:def 1;
        hence a in A by A1,A6,A7;
      end;
    end;
    let a be set;
    assume a in A;
    then ex I being Instruction of STC N st a = AddressPart I & InsCode I = T;
    then a = 0 by Th17;
    hence a in {0} by TARSKI:def 1;
  end;
  hence thesis;
end;

Lm3: for I being Instruction of Trivial-AMI(IL,N) holds AddressPart I = 0
proof
  let I be Instruction of Trivial-AMI(IL,N);
  the Instructions of Trivial-AMI(IL,N) = {[0,{}]} by AMI_1:def 2;
  then I = [0,0] by TARSKI:def 1;
  hence AddressPart I = 0 by MCART_1:def 2;
end;

Lm4: for T being InsType of Trivial-AMI(IL,N) holds AddressParts T = {0}
proof
  let T be InsType of Trivial-AMI(IL,N);
  set A = { AddressPart I where
  I is Instruction of Trivial-AMI(IL,N): InsCode I = T };
  {0} = A
  proof
    hereby
      let a be set;
      assume a in {0};
      then
A1:   a = 0 by TARSKI:def 1;
A2:   the Instructions of Trivial-AMI(IL,N) = {[0,{}]} by AMI_1:def 2;
      then InsCodes Trivial-AMI(IL,N) = {0} by RELAT_1:23;
      then
A3:   T = 0 by TARSKI:def 1;
      reconsider I = [0,0] as Instruction of Trivial-AMI(IL,N)
      by A2,TARSKI:def 1;
A4:   AddressPart I = 0 by Lm3;
      InsCode I = 0 by MCART_1:def 1;
      hence a in A by A1,A3,A4;
    end;
    let a be set;
    assume a in A;
    then ex I being Instruction of Trivial-AMI(IL,N)
    st a = AddressPart I & InsCode I = T;
    then a = 0 by Lm3;
    hence a in {0} by TARSKI:def 1;
  end;
  hence thesis;
end;

registration
  let N be with_non-empty_elements set;
  cluster STC N -> with_explicit_jumps without_implicit_jumps regular;
  coherence
  proof
    thus STC N is with_explicit_jumps
    proof
      let I be Instruction of STC N;
      let f be set;
      thus thesis;
    end;
    thus STC N is without_implicit_jumps
    proof
      let I be Instruction of STC N;
      let f be set;
      the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
      then I = [0,0] or I = [1,0] by TARSKI:def 2;
      then AddressPart I = 0 by MCART_1:def 2;
      hence thesis by RELAT_1:60;
    end;
    let T be InsType of STC N;
    take {};
    thus thesis by Th19,CARD_3:19;
  end;
end;

registration
  let N be with_non-empty_elements set;
  cluster standard regular halting realistic steady-programmed programmable
    with_explicit_jumps without_implicit_jumps
    (IC-Ins-separated definite standard-ins
    (non empty stored-program AMI-Struct over NAT,N));
  existence
  proof
    take STC N;
    thus thesis;
  end;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  cluster Trivial-AMI(IL,N) -> regular;
  coherence
  proof
    let T be InsType of Trivial-AMI(IL,N);
    take {};
    thus thesis by Lm4,CARD_3:19;
  end;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  cluster regular (standard-ins AMI-Struct over IL,N);
  existence
  proof
    take Trivial-AMI(IL,N);
    thus thesis;
  end;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  let S be regular (standard-ins AMI-Struct over IL,N);
  let T be InsType of S;
  cluster AddressParts T -> product-like;
  coherence by Def11;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  let S be homogeneous (standard-ins AMI-Struct over IL,N);
  let T be InsType of S;
  cluster AddressParts T -> with_common_domain;
  coherence
  proof
    let f, g be Function;
    assume f in AddressParts T & g in AddressParts T;
    then (ex I being Instruction of S st f = AddressPart I & InsCode I = T) &
    ex J being Instruction of S st g = AddressPart J & InsCode J = T;
    hence dom f = dom g by Def4;
  end;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set, I be Instruction of Trivial-AMI(IL,N);
  cluster JUMP I -> empty;
  coherence
  proof
    for f being Instruction-Location of Trivial-AMI(IL,N) holds NIC(I,f)={f}
    by AMISTD_1:15,56;
    hence thesis by AMISTD_1:14;
  end;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set;
  cluster Trivial-AMI(IL,N)
    -> with_explicit_jumps without_implicit_jumps regular;
  coherence
  proof
    thus Trivial-AMI(IL,N) is with_explicit_jumps
    proof
      let I be Instruction of Trivial-AMI(IL,N);
      let f be set;
      thus thesis;
    end;
    thus Trivial-AMI(IL,N) is without_implicit_jumps
    proof
      let I be Instruction of Trivial-AMI(IL,N);
      let f be set;
      the Instructions of Trivial-AMI(IL,N) = {[0,{}]} by AMI_1:def 2;
      then I = [0,0] by TARSKI:def 1;
      then AddressPart I = 0 by MCART_1:def 2;
      hence thesis by RELAT_1:60;
    end;
    let T be InsType of Trivial-AMI(IL,N);
    take {};
    thus thesis by Lm4,CARD_3:19;
  end;
end;

registration
  let IL be non trivial set, N;
  cluster regular
    (non empty stored-program standard-ins AMI-Struct over IL,N);
  existence
  proof
    take Trivial-AMI(IL,N);
    thus thesis;
  end;
end;

theorem Th20:
  for IL being non trivial set for S being homogeneous
  (non empty stored-program standard-ins AMI-Struct over IL,N),
  I being Instruction of S, x being set st x in dom AddressPart I holds
  (product" AddressParts InsCode I).x = IL implies
  (AddressPart I).x is Instruction-Location of S
proof
  let IL be non trivial set;
  let S be homogeneous
  (non empty stored-program standard-ins AMI-Struct over IL,N),
  I be Instruction of S, x be set such that
A1: x in dom AddressPart I;
A2: AddressPart I in AddressParts InsCode I;
  assume
A3: (product" AddressParts InsCode I).x = IL;
  for f being Function st f in AddressParts InsCode I holds x in dom f
  proof
    let f be Function;
    assume f in AddressParts InsCode I;
    then ex J being Instruction of S st f = AddressPart J & InsCode I =
    InsCode J;
    hence x in dom f by A1,Def4;
  end;
  then x in dom product" AddressParts InsCode I by A2,CARD_3:def 13;
  then (product" AddressParts InsCode I).x = pi(AddressParts InsCode I,x)
  by A2,CARD_3:def 13;
  then (AddressPart I).x is Element of IL by A2,A3,CARD_3:def 6;
  hence (AddressPart I).x is Instruction-Location of S by AMI_1:def 4;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  cluster Trivial-AMI(IL,N) -> halting;
  coherence;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set;
  cluster without_implicit_jumps with_explicit_jumps halting realistic
    (standard-ins IC-Ins-separated definite
    (non empty stored-program AMI-Struct over IL,N));
  existence
  proof
    take Trivial-AMI(IL,N);
    thus thesis;
  end;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set;
  let S be with_explicit_jumps (IC-Ins-separated
  definite (non empty stored-program standard-ins AMI-Struct over IL,N));
  cluster -> with_explicit_jumps Instruction of S;
  coherence by Def8;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set;
  let S be without_implicit_jumps (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N));
  cluster -> without_implicit_jumps Instruction of S;
  coherence by Def9;
end;

theorem Th21:
  for IL being non trivial set for S being realistic IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I being Instruction of S st I is halting holds JUMP I is empty
proof
  let IL be non trivial set;
  let S be realistic IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of S;
  assume I is halting;
  then for l being Instruction-Location of S holds NIC(I,l)={l}
  by AMISTD_1:15;
  hence thesis by AMISTD_1:14;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set, S be halting realistic
  (IC-Ins-separated definite (non empty stored-program AMI-Struct over IL,N)),
  I be halting Instruction of S;
  cluster JUMP I -> empty;
  coherence by Th21;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set, S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N);
  cluster non trivial programmed FinPartState of S;
  existence
  proof
    consider l1, l2 being Element of IL such that
A1: l1 <> l2 by YELLOW_8:def 1;
    reconsider l1,l2 as Instruction-Location of S by AMI_1:def 4;
    consider I being Instruction of S;
    take f = (l1,l2) --> (I,I);
    thus f is non trivial
    proof
      f = { [l1,I], [l2,I] } by A1,FUNCT_4:71;
      then reconsider x = [l1,I], y = [l2,I] as Element of f by TARSKI:def 2;
      take x, y;
      thus x <> y by A1,ZFMISC_1:33;
    end;
    let a be set;
    assume a in dom f;
    then a in {l1,l2} by FUNCT_4:65;
    then a = l1 or a = l2 by TARSKI:def 2;
    hence thesis;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster trivial -> unique-halt (non empty programmed FinPartState of S);
  coherence
  proof
    let F be non empty programmed FinPartState of S;
    assume
A1: F is trivial;
    let f be Instruction-Location of S such that F.f = halt S and
A2: f in dom F;
    consider x being set such that
A3: F = {x} by A1,REALSET1:def 4;
    x in F by A3,TARSKI:def 1;
    then consider a, b being set such that
A4: [a,b] = x by RELAT_1:def 1;
A5: LastLoc F in dom F by AMISTD_1:51;
A6: dom F = {a} by A3,A4,RELAT_1:23;
    hence f = a by A2,TARSKI:def 1
      .= LastLoc F by A5,A6,TARSKI:def 1;
  end;
end;

definition
  let IL,N be set;
  let S be standard-ins AMI-Struct over IL,N;
  let I be Instruction of S;
  attr I is ins-loc-free means
  :Def12:
  for x being set st x in dom AddressPart I
  holds (product" AddressParts InsCode I).x <> IL;
end;

theorem
  for IL being non trivial set for S being halting with_explicit_jumps
  realistic (IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over IL,N)),
  I being Instruction of S st I is ins-loc-free holds JUMP I is empty
proof
  let IL be non trivial set;
  let S be halting with_explicit_jumps realistic (IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over IL,N)),
  I be Instruction of S such that
A1: for x being set st x in dom AddressPart I holds
  (product" AddressParts InsCode I).x <> IL;
  assume JUMP I is non empty;
  then consider f being set such that
A2: f in JUMP I by XBOOLE_0:def 1;
  ex k being set st k in dom AddressPart I & f = (AddressPart I).k &
  (product" AddressParts InsCode I).k = IL by A2,Def6;
  hence thesis by A1;
end;

theorem Th23:
  for IL being non trivial set for S being without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N)),
  I being Instruction of S st I is halting holds I is ins-loc-free
proof
  let IL be non trivial set;
  let S be without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N)),
  I be Instruction of S such that
A1: I is halting;
  let x be set such that
A2: x in dom AddressPart I;
  assume (product" AddressParts InsCode I).x = IL;
  then (AddressPart I).x in JUMP I by A2,Def7;
  hence contradiction by A1,Th21;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set, S be without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N));
  cluster halting -> ins-loc-free Instruction of S;
  coherence by Th23;
end;

theorem Th24:
  for S being standard without_implicit_jumps standard-ins
  (IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of S st I is sequential holds I is ins-loc-free
proof
  let S be standard without_implicit_jumps standard-ins
  (IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over NAT,N)),
  I be Instruction of S;
  assume
A1: I is sequential;
  assume not thesis;
  then consider k being set such that
A2: k in dom AddressPart I & (product" AddressParts InsCode I).k = NAT
  by Def12;
  (AddressPart I).k in JUMP I by A2,Def7;
  hence thesis by A1,AMISTD_1:43;
end;

registration
  let N be with_non-empty_elements set,
  S be standard without_implicit_jumps standard-ins (IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over NAT,N));
  cluster sequential -> ins-loc-free Instruction of S;
  coherence by Th24;
end;

definition
  let N be with_non-empty_elements set, S be standard halting
  (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  func Stop S -> FinPartState of S equals

  il.(S,0) .--> halt S;
  coherence;
end;

Lm5: now
  let N be with_non-empty_elements set,
  S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  thus dom Stop S = {il.(S,0)} by FUNCOP_1:19;
  hence il.(S,0) in dom Stop S by TARSKI:def 1;
end;

registration
  let N be with_non-empty_elements set, S be standard halting
  (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster Stop S -> lower non empty programmed trivial;
  coherence by AMISTD_1:48;
end;

registration
  let N be with_non-empty_elements set, S be standard realistic halting
  (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster Stop S -> closed;
  coherence by AMISTD_1:46;
end;

registration
  let N be with_non-empty_elements set,
  S be standard halting steady-programmed (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster Stop S -> autonomic;
  coherence by AMISTD_1:12;
end;

theorem Th25:
  for S being standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)) holds card Stop S = 1
proof
  let S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  thus card Stop S = card {[il.(S,0),halt S]} by FUNCT_4:87
    .= 1 by CARD_1:79;
end;

theorem Th26:
  for S being standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being pre-Macro of S st card F = 1 holds F = Stop S
proof
  let S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F be pre-Macro of S;
  assume
A1: card F = 1;
  then consider x being set such that
A2: F = {x} by CARD_2:60;
  x in F by A2,TARSKI:def 1;
  then consider a, b being set such that
A3: [a,b] = x by RELAT_1:def 1;
A4: dom F = {a} by A2,A3,RELAT_1:23;
A5: il.(S,0) in dom F by AMISTD_1:49;
  then
A6: a = il.(S,0) by A4,TARSKI:def 1;
  card F -' 1 = card F - 1 by PRE_CIRC:25
    .= 0 by A1;
  then LastLoc F = il.(S,0) by AMISTD_1:55;
  then F.il.(S,0) = halt S by AMISTD_1:def 22;
  then halt S in rng F by A5,FUNCT_1:def 5;
  then halt S in {b} by A2,A3,RELAT_1:23;
  then F = {[il.(S,0),halt S]} by A2,A3,A6,TARSKI:def 1
    .= il.(S,0) .--> halt S by FUNCT_4:87;
  hence F = Stop S;
end;

Lm6: for S being standard halting (IC-Ins-separated definite
(non empty stored-program AMI-Struct over NAT,N)) holds card Stop S -' 1 = 0
proof
  let S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  thus card Stop S -' 1 = card Stop S - 1 by PRE_CIRC:25
    .= 1 - 1 by Th25
    .= 0;
end;

theorem Th27:
  for S being standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N))
  holds LastLoc Stop S = il.(S,0)
proof
  let S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  card Stop S -' 1 = 0 by Lm6;
  hence LastLoc Stop S = il.(S,0) by AMISTD_1:55;
end;

registration
  let N be with_non-empty_elements set,
  S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster Stop S -> halt-ending unique-halt;
  coherence
  proof
    thus (Stop S).(LastLoc Stop S) = (il.(S,0) .--> halt S).il.(S,0) by Th27
      .= halt S by FUNCOP_1:87;
    let l be Instruction-Location of S such that (Stop S).l = halt S;
    assume l in dom Stop S;
    then l in {il.(S,0)} by Lm5;
    then l = il.(S,0) by TARSKI:def 1;
    hence l = LastLoc Stop S by Th27;
  end;
end;

definition
  let N be with_non-empty_elements set,
  S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  redefine func Stop S -> pre-Macro of S;
  coherence;
end;

begin  :: On the composition of macro instructions

definition
  let N be with_non-empty_elements set;
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let I be Element of the Instructions of S;
  let k be natural number;
  func IncAddr(I,k) -> Instruction of S means
  :Def14:
  InsCode it = InsCode I &
  dom AddressPart it = dom AddressPart I &
  for n being set st n in dom AddressPart I holds
  ((product" AddressParts InsCode I).n = NAT implies
  ex f being Instruction-Location of S st
  f = (AddressPart I).n & (AddressPart it).n = il.(S,k + locnum f)) &
  ((product" AddressParts InsCode I).n <> NAT implies
  (AddressPart it).n = (AddressPart I).n);
  existence
  proof
    set D = (union N) \/ the carrier of S;
    defpred P[set,set] means ((product" AddressParts InsCode I).$1 = NAT
    implies ex il being Instruction-Location of S st
    il = (AddressPart I).$1 & $2 = il.(S,k + locnum il)) &
    ((product" AddressParts InsCode I).$1 <> NAT implies
    $2 = (AddressPart I).$1);
A1: for m being Nat st m in Seg len AddressPart I
    ex x being Element of D st P[m,x]
    proof
      let m be Nat;
      assume m in Seg len AddressPart I;
      then
A2:   m in dom AddressPart I by FINSEQ_1:def 3;
      then
A3:   (AddressPart I).m in rng AddressPart I by FUNCT_1:def 5;
      per cases;
      suppose
A4:     (product" AddressParts InsCode I).m = NAT;
        then reconsider il = (AddressPart I).m as Instruction-Location of S
        by A2,Th20;
        reconsider x = il.(S,k + locnum il) as Element of D by XBOOLE_0:def 2;
        take x;
        thus thesis by A4;
      end;
      suppose
A5:     (product" AddressParts InsCode I).m <> NAT;
        rng AddressPart I c= D by FINSEQ_1:def 4;
        then reconsider x = (AddressPart I).m as Element of D by A3;
        take x;
        thus thesis by A5;
      end;
    end;
    consider p being FinSequence of D such that
A6: dom p = Seg len AddressPart I and
A7: for k being Nat st k in Seg len AddressPart I holds P[k,p.k]
    from FINSEQ_1:sch 5(A1);
    set f = product" AddressParts InsCode I;
A8: AddressPart I in AddressParts InsCode I;
    then
A9: AddressParts InsCode I = product f by CARD_3:95;
A10: dom p = dom AddressPart I by A6,FINSEQ_1:def 3
      .= DOM AddressParts InsCode I by A8,CARD_3:def 12
      .= dom f by CARD_3:92;
    for z being set st z in dom p holds p.z in f.z
    proof
      let z be set;
      assume
A11:  z in dom p;
      then
A12:  f.z = pi(AddressParts InsCode I,z) by A8,A10,CARD_3:def 13;
      reconsider z as Element of NAT by A11;
      per cases;
      suppose
A13:    f.z = NAT;
        then ex il being Instruction-Location of S st
        il = (AddressPart I).z & p.z = il.(S,k + locnum il) by A6,A7,A11;
        hence thesis by A13,AMI_1:def 4;
      end;
      suppose f.z <> NAT;
        then p.z = (AddressPart I).z by A6,A7,A11;
        hence thesis by A8,A12,CARD_3:def 6;
      end;
    end;
    then p in AddressParts InsCode I by A9,A10,CARD_3:18;
    then consider IT being Instruction of S such that
A14: p = AddressPart IT and
A15: InsCode I = InsCode IT;
    take IT;
    thus InsCode IT = InsCode I by A15;
    thus dom AddressPart IT = dom AddressPart I by A6,A14,FINSEQ_1:def 3;
    let n be set;
    assume
A16: n in dom AddressPart I;
    then reconsider n as Element of NAT;
    n in Seg len AddressPart I by A16,FINSEQ_1:def 3;
    hence thesis by A7,A14;
  end;
  uniqueness
  proof
    let a, b be Instruction of S such that
A17: InsCode a = InsCode I and
A18: dom AddressPart a = dom AddressPart I and
A19: for n being set st n in dom AddressPart I holds
    ((product" AddressParts InsCode I).n = NAT implies
    ex f being Instruction-Location of S st
    f = (AddressPart I).n & (AddressPart a).n = il.(S,k + locnum f)) &
    ((product" AddressParts InsCode I).n <> NAT implies
    (AddressPart a).n = (AddressPart I).n) and
A20: InsCode b = InsCode I and
A21: dom AddressPart b = dom AddressPart I and
A22: for n being set st n in dom AddressPart I holds
    ((product" AddressParts InsCode I).n = NAT implies
    ex f being Instruction-Location of S st
    f = (AddressPart I).n & (AddressPart b).n = il.(S,k + locnum f)) &
    ((product" AddressParts InsCode I).n <> NAT implies
    (AddressPart b).n = (AddressPart I).n);
A23: Seg len AddressPart a = dom AddressPart a by FINSEQ_1:def 3;
    for n being Nat st n in Seg len AddressPart a holds
    (AddressPart a).n = (AddressPart b).n
    proof
      let n be Nat;
      assume n in Seg len AddressPart a;
      then ((product" AddressParts InsCode I).n = NAT implies
      ex f being Instruction-Location of S st
      f = (AddressPart I).n & (AddressPart a).n = il.(S,k + locnum f)) &
      ((product" AddressParts InsCode I).n <> NAT implies
      (AddressPart a).n = (AddressPart I).n) &
      ((product" AddressParts InsCode I).n = NAT implies
      ex f being Instruction-Location of S st
      f = (AddressPart I).n & (AddressPart b).n = il.(S,k + locnum f)) &
      ((product" AddressParts InsCode I).n <> NAT implies
      (AddressPart b).n = (AddressPart I).n) by A18,A19,A22,A23;
      hence (AddressPart a).n = (AddressPart b).n;
    end;
    then AddressPart a = AddressPart b by A18,A21,A23,FINSEQ_1:17;
    hence thesis by A17,A20,Th16;
  end;
end;

theorem Th28:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Element of the Instructions of S holds IncAddr(I, 0) = I
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I be Element of the Instructions of S;
A1: InsCode IncAddr(I, 0) = InsCode I by Def14;
A2: dom AddressPart I = dom AddressPart IncAddr(I, 0) by Def14;
  for k being Nat st k in dom AddressPart I holds
  (AddressPart IncAddr(I, 0)).k = (AddressPart I).k
  proof
    let k be Nat;
    assume
A3: k in dom AddressPart I;
    per cases;
    suppose (product" AddressParts InsCode I).k = NAT;
      then ex f being Instruction-Location of S st f = (AddressPart I).k &
      (AddressPart IncAddr(I,0)).k = il.(S,0 + locnum f) by A3,Def14;
      hence thesis by AMISTD_1:def 13;
    end;
    suppose (product" AddressParts InsCode I).k <> NAT;
      hence thesis by A3,Def14;
    end;
  end;
  then AddressPart IncAddr(I, 0) = AddressPart I by A2,FINSEQ_1:17;
  hence IncAddr(I, 0) = I by A1,Th16;
end;

theorem Th29:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of S st I is ins-loc-free holds IncAddr(I, k) = I
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I be Instruction of S such that
A1: for x being set st x in dom AddressPart I
  holds (product" AddressParts InsCode I).x <> NAT;
  set f = IncAddr(I, k);
A2: InsCode f = InsCode I by Def14;
A3: dom AddressPart f = dom AddressPart I by Def14;
  for x being set st x in dom AddressPart I holds
  (AddressPart f).x = (AddressPart I).x
  proof
    let x be set such that
A4: x in dom AddressPart I;
    (product" AddressParts InsCode I).x = NAT or
    (product" AddressParts InsCode I).x <> NAT;
    hence thesis by A1,A4,Def14;
  end;
  then AddressPart f = AddressPart I by A3,FUNCT_1:9;
  hence thesis by A2,Th16;
end;

theorem
  for S being halting standard without_implicit_jumps realistic
  regular (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N))
  holds IncAddr(halt S, k) = halt S by Th29;

registration
  let N be with_non-empty_elements set,
  S be halting standard without_implicit_jumps
  realistic regular (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I be halting Instruction of S, k be natural number;
  cluster IncAddr(I,k) -> halting;
  coherence by Th29;
end;

theorem Th31:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I being Instruction of S
  holds AddressParts InsCode I = AddressParts InsCode IncAddr(I,k)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of S;
  set A = { AddressPart J where J is Instruction of S:
  InsCode I = InsCode J }, B = { AddressPart J where J is Instruction of S:
  InsCode IncAddr(I,k) = InsCode J };
  A = B
  proof
    hereby
      let a be set;
      assume a in A;
      then consider J being Instruction of S such that
A1:   a = AddressPart J and
A2:   InsCode J = InsCode I;
      InsCode J = InsCode IncAddr(I,k) by A2,Def14;
      hence a in B by A1;
    end;
    let a be set;
    assume a in B;
    then consider J being Instruction of S such that
A3: a = AddressPart J and
A4: InsCode J = InsCode IncAddr(I,k);
    InsCode J = InsCode I by A4,Def14;
    hence a in A by A3;
  end;
  hence AddressParts InsCode I = AddressParts InsCode IncAddr(I,k);
end;

theorem Th32:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I, J being Instruction of S st
  (ex k being natural number st IncAddr(I,k) = IncAddr(J,k)) holds
  (product" AddressParts InsCode I).x = NAT implies
  (product" AddressParts InsCode J).x = NAT
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I, J be Instruction of S;
  given k being natural number such that
A1: IncAddr(I,k) = IncAddr(J,k);
  assume
A2: (product" AddressParts InsCode I).x = NAT;
  assume
A3: (product" AddressParts InsCode J).x <> NAT;
  (product" AddressParts InsCode IncAddr(I,k)).x = NAT by A2,Th31;
  hence thesis by A1,A3,Def14;
end;

theorem Th33:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I, J being Instruction of S st
  (ex k being natural number st IncAddr(I,k) = IncAddr(J,k)) holds
  (product" AddressParts InsCode I).x <> NAT implies
  (product" AddressParts InsCode J).x <> NAT
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I, J be Instruction of S;
  given k being natural number such that
A1: IncAddr(I,k) = IncAddr(J,k);
  assume
A2: (product" AddressParts InsCode I).x <> NAT;
  assume (product" AddressParts InsCode J).x = NAT;
  then (product" AddressParts InsCode IncAddr(J,k)).x = NAT by Th31;
  hence contradiction by A1,A2,Th31;
end;

theorem Th34:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I, J being Instruction of S st
  ex k being natural number st IncAddr(I,k) = IncAddr(J,k) holds I = J
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I, J be Instruction of S;
  given k being natural number such that
A1: IncAddr(I,k) = IncAddr(J,k);
A2: InsCode I = InsCode IncAddr(I,k) by Def14
    .= InsCode J by A1,Def14;
  then
A3: dom AddressPart I = dom AddressPart J by Def4;
  for x being set st x in dom AddressPart I holds
  (AddressPart I).x = (AddressPart J).x
  proof
    let x be set;
    assume
A4: x in dom AddressPart I;
    per cases;
    suppose
A5:   (product" AddressParts InsCode I).x = NAT;
      then consider f being Instruction-Location of S such that
A6:   f = (AddressPart I).x and
A7:   (AddressPart IncAddr(I,k)).x = il.(S,k + locnum f) by A4,Def14;
      (product" AddressParts InsCode J).x = NAT by A1,A5,Th32;
      then consider g being Instruction-Location of S such that
A8:   g = (AddressPart J).x and
A9:   (AddressPart IncAddr(J,k)).x = il.(S,k + locnum g) by A3,A4,Def14;
      k + locnum f = k + locnum g by A1,A7,A9,AMISTD_1:25;
      hence (AddressPart I).x = (AddressPart J).x by A6,A8,AMISTD_1:27;
    end;
    suppose
A10:  (product" AddressParts InsCode I).x <> NAT;
      then
A11:  (product" AddressParts InsCode J).x <> NAT by A1,Th33;
      thus (AddressPart I).x = (AddressPart IncAddr(I,k)).x by A4,A10,Def14
        .= (AddressPart J).x by A1,A3,A4,A11,Def14;
    end;
  end;
  then AddressPart I = AddressPart J by A3,FUNCT_1:9;
  hence I = J by A2,Th16;
end;

theorem Th35:
  for S being regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of S st IncAddr(I,k) = halt S holds I = halt S
proof
  let S be regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of S;
  assume IncAddr(I,k) = halt S;
  then IncAddr(I,k) = IncAddr(halt S,k) by Th29;
  hence I = halt S by Th34;
end;

theorem
  for S being regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of S st I is sequential
  holds IncAddr(I,k) is sequential by Th24,Th29;

theorem Th37:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I being Instruction of S
  holds IncAddr(IncAddr(I,k),m) = IncAddr(I,k+m)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of S;
A1: InsCode IncAddr(IncAddr(I,k),m) = InsCode IncAddr(I,k) by Def14
    .= InsCode I by Def14
    .= InsCode IncAddr(I,k+m) by Def14;
A2: dom AddressPart IncAddr(I,k+m) = dom AddressPart I by Def14
    .= dom AddressPart IncAddr(I,k) by Def14
    .= dom AddressPart IncAddr(IncAddr(I,k),m) by Def14;
  for n being set st n in dom AddressPart IncAddr(IncAddr(I,k),m) holds
  (AddressPart IncAddr(IncAddr(I,k),m)).n = (AddressPart IncAddr(I,k+m)).n
  proof
    let n be set such that
A3: n in dom AddressPart IncAddr(IncAddr(I,k),m);
A4: n in dom AddressPart IncAddr(I,k) by A3,Def14;
    then
A5: n in dom AddressPart I by Def14;
    per cases;
    suppose
A6:   (product" AddressParts InsCode I).n = NAT;
      then consider f being Instruction-Location of S such that
A7:   f = (AddressPart I).n and
A8:   (AddressPart IncAddr(I,k)).n = il.(S,k + locnum f) by A5,Def14;
      (product" AddressParts InsCode IncAddr(I,k)).n = NAT by A6,Th31;
      then consider g being Instruction-Location of S such that
A9:   g = (AddressPart IncAddr(I,k)).n and
A10:  (AddressPart IncAddr(IncAddr(I,k),m)).n = il.(S,m + locnum g)
      by A4,Def14;
      consider h being Instruction-Location of S such that
A11:  h = (AddressPart I).n and
A12:  (AddressPart IncAddr(I,k+m)).n = il.(S,k + m + locnum h) by A5,A6,Def14;
      locnum g = k + locnum f by A8,A9,AMISTD_1:def 13;
      hence (AddressPart IncAddr(IncAddr(I,k),m)).n
      = (AddressPart IncAddr(I,k+m)).n by A7,A10,A11,A12;
    end;
    suppose
A13:  (product" AddressParts InsCode I).n <> NAT;
      then (product" AddressParts InsCode IncAddr(I,k)).n <> NAT by Def14;
      hence (AddressPart IncAddr(IncAddr(I,k),m)).n
      = (AddressPart IncAddr(I,k)).n by A4,Def14
        .= (AddressPart I).n by A5,A13,Def14
        .= (AddressPart IncAddr(I,k+m)).n by A5,A13,Def14;
    end;
  end;
  then AddressPart IncAddr(IncAddr(I,k),m) = AddressPart IncAddr(I,k+m)
  by A2,FUNCT_1:9;
  hence IncAddr(IncAddr(I,k),m) = IncAddr(I,k+m) by A1,Th16;
end;

definition
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  p be programmed FinPartState of S, k be natural number;
A1: dom p c= NAT by AMI_1:def 40;
  func IncAddr(p,k) -> FinPartState of S means
  :Def15:
  dom it = dom p &
  for m being natural number st il.(S,m) in dom p holds
  it.il.(S,m) = IncAddr(pi(p,il.(S,m)),k);
  existence
  proof
    defpred P[set,set] means ex m being Element of NAT st $1 = il.(S,m) &
    $2 = IncAddr(pi(p,il.(S,m)),k);
A2: for e being set st e in dom p ex u being set st P[e,u]
    proof
      let e be set;
      assume e in dom p;
      then reconsider l=e as Instruction-Location of S by A1,AMI_1:def 4;
      consider m being natural number such that
A3:   l = il.(S,m) by AMISTD_1:26;
      take IncAddr(pi(p,il.(S,m)),k);
      reconsider m as Element of NAT by ORDINAL1:def 13;
      e = il.(S,m) by A3;
      hence thesis;
    end;
    consider f being Function such that
A4: dom f = dom p and
A5: for e being set st e in dom p holds P[e,f.e] from CLASSES1:sch 1(A2);
    NAT c= the carrier of S by AMI_1:def 3;
    then dom p c= the carrier of S by A1,XBOOLE_1:1;
    then
A6: dom f c= dom the Object-Kind of S by A4,FUNCT_2:def 1;
    for x being set st x in dom f holds f.x in (the Object-Kind of S).x
    proof
      let x be set;
      assume
A7:   x in dom f;
      then
A8:   ex m being Element of NAT st x = il.(S,m) & f.x = IncAddr(pi
      (p,il.(S,m)),k) by A4,A5;
      reconsider y = x as Instruction-Location of S by A1,A4,A7,AMI_1:def 4;
      (the Object-Kind of S).y = ObjectKind y
        .= the Instructions of S by AMI_1:def 14;
      hence f.x in (the Object-Kind of S).x by A8;
    end;
    then reconsider f as finite Element of sproduct the Object-Kind of S
    by A4,A6,CARD_3:def 9,FINSET_1:29;
    reconsider f as FinPartState of S;
    take f;
    thus dom f = dom p by A4;
    let m be natural number;
    assume il.(S,m) in dom p;
    then ex j being Element of NAT st il.(S,m) = il.(S,j) &
    f.il.(S,m) = IncAddr(pi(p,il.(S,j)),k) by A5;
    hence f.il.(S,m) = IncAddr(pi(p,il.(S,m)),k);
  end;
  uniqueness
  proof
    let IT1,IT2 be FinPartState of S such that
A9: dom IT1 = dom p and
A10: for m being natural number st il.(S,m) in dom p holds
    IT1.il.(S,m) = IncAddr(pi(p,il.(S,m)),k) and
A11: dom IT2 = dom p and
A12: for m being natural number st il.(S,m) in dom p holds
    IT2.il.(S,m) = IncAddr(pi(p,il.(S,m)),k);
    for x being set st x in dom p holds IT1.x = IT2.x
    proof
      let x be set;
      assume
A13:  x in dom p;
      then reconsider l=x as Instruction-Location of S by A1,AMI_1:def 4;
      consider m being natural number such that
A14:  l = il.(S,m) by AMISTD_1:26;
      reconsider m as Element of NAT by ORDINAL1:def 13;
      thus IT1.x = IncAddr(pi(p,il.(S,m)),k) by A10,A13,A14
        .= IT2.x by A12,A13,A14;
    end;
    hence IT1=IT2 by A9,A11,FUNCT_1:9;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be programmed FinPartState of S, k be natural number;
  cluster IncAddr(F,k) -> programmed;
  coherence
  proof
    dom IncAddr(F,k) = dom F by Def15;
    hence dom IncAddr(F,k) c= NAT by AMI_1:def 40;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be empty programmed FinPartState of S, k be natural number;
  cluster IncAddr(F,k) -> empty;
  coherence
  proof
    assume not thesis;
    then reconsider f = IncAddr(F,k) as non empty Function;
A1: dom f <> {};
    dom IncAddr(F,k) = dom F by Def15;
    hence thesis by A1;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be non empty programmed FinPartState of S, k be natural number;
  cluster IncAddr(F,k) -> non empty;
  coherence
  proof
    dom IncAddr(F,k) = dom F by Def15;
    hence thesis by RELAT_1:60;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower programmed FinPartState of S, k be natural number;
  cluster IncAddr(F,k) -> lower;
  coherence
  proof
    dom IncAddr(F,k) = dom F by Def15;
    hence thesis by Th13;
  end;
end;

theorem Th38:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being programmed FinPartState of S holds IncAddr(F,0) = F
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be programmed FinPartState of S;
  for m being natural number st il.(S,m) in dom F holds
  F.il.(S,m) = IncAddr(pi(F,il.(S,m)),0)
  proof
    let m be natural number;
    assume il.(S,m) in dom F;
    then pi(F,il.(S,m)) = F.il.(S,m) by AMI_1:def 47;
    hence F.il.(S,m) = IncAddr(pi(F,il.(S,m)),0) by Th28;
  end;
  hence thesis by Def15;
end;

theorem
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being lower programmed FinPartState of S
  holds IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower programmed FinPartState of S;
A1: dom IncAddr(IncAddr(F,k),m) = dom IncAddr(F,k) by Def15
    .= dom F by Def15;
A2: dom IncAddr(F,k+m) = dom F by Def15;
  for x being set st x in dom F holds
  IncAddr(IncAddr(F,k),m).x = IncAddr(F,k+m).x
  proof
    let x be set such that
A3: x in dom F;
    dom F c= NAT by AMI_1:def 40;
    then reconsider x as Instruction-Location of S by A3,AMI_1:def 4;
A4: x = il.(S,locnum x) by AMISTD_1:def 13;
    then
A5: il.(S,locnum x) in dom IncAddr(F,k) by A3,Def15;
A6: IncAddr(pi(F,il.(S,locnum x)),k) = IncAddr(F,k).il.(S,locnum x)
    by A3,A4,Def15
      .= pi(IncAddr(F,k),il.(S,locnum x)) by A5,AMI_1:def 47;
    IncAddr(IncAddr(F,k),m).il.(S,locnum x)
    = IncAddr(pi(IncAddr(F,k),il.(S,locnum x)),m) by A5,Def15
      .= IncAddr(pi(F,il.(S,locnum x)),k+m) by A6,Th37
      .= IncAddr(F,k+m).il.(S,locnum x) by A3,A4,Def15;
    hence thesis by A4;
  end;
  hence IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m) by A1,A2,FUNCT_1:9;
end;

definition
  let N be with_non-empty_elements set,
  S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), p be FinPartState of S,
  k be natural number;
  func Shift(p,k) -> FinPartState of S means
  :Def16:
  dom it = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p } &
  for m being Element of NAT st il.(S,m) in dom p
  holds it.il.(S,m+k) = p.il.(S,m);
  existence
  proof
    deffunc F(Element of NAT) = il.(S,$1+k);
    deffunc G(Element of NAT) = il.(S,$1);
    set A = { F(m) where m is Element of NAT: G(m) in dom p };
    defpred P [set,set] means
    ex m being Element of NAT st $1 = il.(S,m+k) & $2 = p.il.(S,m);
A1: for e being set st e in A ex u being set st P[e,u]
    proof
      let e be set;
      assume e in A;
      then consider m being Element of NAT such that
A2:   e = il.(S,m+k) & il.(S,m) in dom p;
      take p.il.(S,m);
      thus thesis by A2;
    end;
    consider f being Function such that
A3: dom f = A and
A4: for e being set st e in A holds P[e,f.e] from CLASSES1:sch 1(A1);
A5: NAT c= the carrier of S by AMI_1:def 3;
A6: A c= NAT
    proof
      let x be set;
      assume x in A;
      then ex m being Element of NAT st x = il.(S,m+k) & il.(S,m) in dom p;
      hence x in NAT by AMI_1:def 4;
    end;
    then A c= the carrier of S by A5,XBOOLE_1:1;
    then
A7: dom f c= dom the Object-Kind of S by A3,FUNCT_2:def 1;
    for x being set st x in dom f holds f.x in (the Object-Kind of S).x
    proof
      let x be set;
      assume
A8:   x in dom f;
      then consider m being Element of NAT such that
A9:   x = il.(S,m+k) and
A10:  f.x = p.il.(S,m) by A3,A4;
      reconsider y = x as Instruction-Location of S by A3,A6,A8,AMI_1:def 4;
A11:  (the Object-Kind of S).x = ObjectKind y
        .= the Instructions of S by AMI_1:def 14;
      consider s being State of S such that
A12:  p c= s by AMI_1:82;
      consider j being Element of NAT such that
A13:  il.(S,m+k) = il.(S,j+k) and
A14:  il.(S,j) in dom p by A3,A8,A9;
A15:  j+k = m+k by A13,AMISTD_1:25;
      s.il.(S,m) in the Instructions of S;
      hence f.x in (the Object-Kind of S).x by A10,A11,A12,A14,A15,GRFUNC_1:8;
    end;
    then reconsider f as Element of sproduct the Object-Kind of S
    by A7,CARD_3:def 9;
A16: dom p is finite;
A17: for m1, m2 being Element of NAT st G(m1) = G(m2)
    holds m1 = m2 by AMISTD_1:25;
    A is finite from FUNCT_7:sch 2(A16,A17);
    then reconsider f as FinPartState of S by A3,FINSET_1:29;
    take f;
    thus dom f = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p }
    by A3;
    let m be Element of NAT;
    assume il.(S,m) in dom p;
    then il.(S,m+k) in A;
    then consider j being Element of NAT such that
A18: il.(S,m+k) = il.(S,j+k) and
A19: f.il.(S,m+k) = p.il.(S,j) by A4;
    m+k = j+k by A18,AMISTD_1:25;
    hence f.il.(S,m+k) = p.il.(S,m) by A19;
  end;
  uniqueness
  proof
    let IT1, IT2 be FinPartState of S such that
A20: dom IT1 = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p } and
A21: for m being Element of NAT st il.(S,m) in dom p
    holds IT1.il.(S,m+k) = p.il.(S,m) and
A22: dom IT2 = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p } and
A23: for m being Element of NAT st il.(S,m) in dom p
    holds IT2.il.(S,m+k) = p.il.(S,m);
    for x being set
    st x in { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p }
    holds IT1.x = IT2.x
    proof
      let x be set;
      assume x in { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p };
      then consider m being Element of NAT such that
A24:  x = il.(S,m+k) and
A25:  il.(S,m) in dom p;
      thus IT1.x = p.il.(S,m) by A21,A24,A25
        .= IT2.x by A23,A24,A25;
    end;
    hence IT1=IT2 by A20,A22,FUNCT_1:9;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F be FinPartState of S,
  k be natural number;
  cluster Shift(F,k) -> programmed;
  coherence
  proof
A1: dom Shift(F,k) =
    { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom F } by Def16;
    let x be set;
    assume x in dom Shift(F,k);
    then ex m being Element of NAT st x = il.(S,m+k) & il.(S,m) in dom F by A1;
    hence x in NAT by AMI_1:def 4;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be empty FinPartState of S, k be natural number;
  cluster Shift(F,k) -> empty;
  coherence
  proof
A1: dom Shift(F,k) =
    { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom F } by Def16;
    assume Shift(F,k) is non empty;
    then reconsider f = Shift(F,k) as non empty Function;
    dom f is non empty;
    then consider a being set such that
A2: a in dom Shift(F,k) by XBOOLE_0:def 1;
    ex m being Element of NAT st a = il.(S,m+k) & il.(S,m) in dom F by A1,A2;
    hence thesis;
  end;
end;

registration
  let N be with_non-empty_elements set,
  S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be non empty programmed FinPartState of S, k be natural number;
  cluster Shift(F,k) -> non empty;
  coherence
  proof
A1: dom Shift(F,k) =
    { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom F } by Def16;
    consider a being set such that
A2: a in dom F by XBOOLE_0:def 1;
    dom F c= NAT by AMI_1:def 40;
    then reconsider a as Instruction-Location of S by A2,AMI_1:def 4;
    consider m being natural number such that
A3: a = il.(S,m) by AMISTD_1:26;
    reconsider m as Element of NAT by ORDINAL1:def 13;
    il.(S,m+k) in dom Shift(F,k) by A1,A2,A3;
    hence thesis by RELAT_1:60;
  end;
end;

theorem Th40:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being programmed FinPartState of S holds Shift(F,0) = F
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be programmed FinPartState of S;
A1: dom F c= NAT by AMI_1:def 40;
A2: dom F = { il.(S,m+0) where m is Element of NAT: il.(S,m) in dom F }
  proof
    hereby
      let a be set;
      assume
A3:   a in dom F;
      then reconsider l=a as Instruction-Location of S by A1,AMI_1:def 4;
      consider k being natural number such that
A4:   l = il.(S,k) by AMISTD_1:26;
      reconsider k as Element of NAT by ORDINAL1:def 13;
      a = il.(S,k+0) by A4;
      hence a in
      { il.(S,m+0) where m is Element of NAT: il.(S,m) in dom F } by A3;
    end;
    let a be set;
    assume a in { il.(S,m+0) where m is Element of NAT: il.(S,m) in dom F };
    then ex m being Element of NAT st a = il.(S,m+0) & il.(S,m) in dom F;
    hence thesis;
  end;
  for m being Element of NAT
  st il.(S,m) in dom F holds F.il.(S,m+0) = F.il.(S,m);
  hence thesis by A2,Def16;
end;

theorem Th41:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being FinPartState of S, k being natural number st k > 0
  holds not il.(S,0) in dom Shift(F,k)
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F be FinPartState of S,
  k be natural number such that
A1: k > 0 and
A2: il.(S,0) in dom Shift(F,k);
  dom Shift(F,k) = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom F }
  by Def16;
  then consider m being Element of NAT such that
A3: il.(S,0) = il.(S,m+k) and il.(S,m) in dom F by A2;
  m+k=0 by A3,AMISTD_1:25;
  hence contradiction by A1,NAT_1:7;
end;

theorem
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F being FinPartState of S
  holds Shift(Shift(F,m),k) = Shift(F,m+k)
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F be FinPartState of S;
  set A = {il.(S,l+m) where l is Element of NAT: il.(S,l) in dom F};
A1: dom Shift(F,m) = A by Def16;
  {il.(S,r+k) where r is Element of NAT: il.(S,r) in A} =
  {il.(S,q+(m+k)) where q is Element of NAT: il.(S,q) in dom F}
  proof
    hereby
      let x be set;
      assume x in {il.(S,r+k) where r is Element of NAT: il.(S,r) in A };
      then consider r being Element of NAT such that
A2:   x = il.(S,r+k) and
A3:   il.(S,r) in A;
      consider l being Element of NAT such that
A4:   il.(S,r) = il.(S,l+m) and
A5:   il.(S,l) in dom F by A3;
      r = l+m by A4,AMISTD_1:25;
      then x = il.(S,l+(m+k)) by A2;
      hence x in
      {il.(S,q+(m+k)) where q is Element of NAT: il.(S,q) in dom F} by A5;
    end;
    let x be set;
    assume x in {il.(S,q+(m+k)) where q is Element of NAT: il.(S,q) in dom F};
    then consider q being Element of NAT such that
A6: x = il.(S,q+(m+k)) and
A7: il.(S,q) in dom F;
A8: x = il.(S,q+m+k) by A6;
    il.(S,q+m) in A by A7;
    hence x in {il.(S,r+k) where r is Element of NAT: il.(S,r) in A} by A8;
  end;
  then
A9: dom Shift(Shift(F,m),k)
  = {il.(S,l+(m+k)) where l is Element of NAT: il.(S,l) in dom F} by A1,Def16;
  now
    let l be Element of NAT;
    assume
A10: il.(S,l) in dom F;
    then
A11: il.(S,l+m) in dom Shift(F,m) by A1;
    thus Shift(Shift(F,m),k).il.(S,l+(m+k)) = Shift(Shift(F,m),k).il.(S,l+m+k)
      .= Shift(F,m).il.(S,l+m) by A11,Def16
      .= F.il.(S,l) by A10,Def16;
  end;
  hence Shift(Shift(F,m),k) = Shift(F,m+k) by A9,Def16;
end;

theorem Th43:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being programmed FinPartState of S
  holds dom F,dom Shift(F,k) are_equipotent
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be programmed FinPartState of S;
A1: dom F c= NAT by AMI_1:def 40;
  defpred P[set,set] means
  ex il being Instruction-Location of S st $1 = il & $2 = il.(S,k+locnum il);
A2: for e being set st e in dom F ex u being set st P[e,u]
  proof
    let e be set;
    assume e in dom F;
    then reconsider e as Instruction-Location of S by A1,AMI_1:def 4;
    take il.(S,k+locnum e), e;
    thus thesis;
  end;
  consider f being Function such that
A3: dom f = dom F and
A4: for x being set st x in dom F holds P[x,f.x] from CLASSES1:sch 1(A2);
  take f;
  hereby
    let x1, x2 be set such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f.x1 = f.x2;
    consider i1 being Instruction-Location of S such that
A8: x1 = i1 and
A9: f.x1 = il.(S,k+locnum i1) by A3,A4,A5;
    consider i2 being Instruction-Location of S such that
A10: x2 = i2 and
A11: f.x2 = il.(S,k+locnum i2) by A3,A4,A6;
    k+locnum i1 = k+locnum i2 by A7,A9,A11,AMISTD_1:25;
    hence x1 = x2 by A8,A10,AMISTD_1:27;
  end;
  thus dom f = dom F by A3;
A12: dom Shift(F,k) =
  { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom F } by Def16;
  hereby
    let y be set;
    assume y in rng f;
    then consider x being set such that
A13: x in dom f and
A14: f.x = y by FUNCT_1:def 5;
    consider il being Instruction-Location of S such that
A15: x = il & f.x = il.(S,k+locnum il) by A3,A4,A13;
    consider a being natural number such that
A16: il = il.(S,a) by AMISTD_1:26;
    reconsider a as Element of NAT by ORDINAL1:def 13;
    a = locnum il by A16,AMISTD_1:def 13;
    hence y in dom Shift(F,k) by A3,A12,A13,A14,A15,A16;
  end;
  let y be set;
  assume y in dom Shift(F,k);
  then consider m being Element of NAT such that
A17: y = il.(S,m+k) and
A18: il.(S,m) in dom F by A12;
  consider il being Instruction-Location of S such that
A19: il.(S,m) = il & f.il.(S,m) = il.(S,k+locnum il) by A4,A18;
  m = locnum il by A19,AMISTD_1:def 13;
  hence y in rng f by A3,A17,A18,A19,FUNCT_1:def 5;
end;

definition
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of S;
  attr I is IC-good means
  :Def17:
  for k being natural number,
  s1, s2 being State of S st s2 = s1 +* (IC S .--> (IC s1 + k))
  holds IC Exec(I,s1) + k = IC Exec(IncAddr(I,k), s2);
end;

definition
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  attr S is IC-good means
  :Def18:
  for I being Instruction of S holds I is IC-good;
end;

definition
  let IL;
  let N be with_non-empty_elements set,
  S be stored-program AMI-Struct over IL,N, I be Instruction of S;
  attr I is Exec-preserving means
  :Def19:
  for s1, s2 being State of S
  st s1, s2 equal_outside IL holds Exec(I,s1), Exec(I,s2) equal_outside IL;
end;

definition
  let IL;
  let N be with_non-empty_elements set,
  S be stored-program AMI-Struct over IL,N;
  attr S is Exec-preserving means
  :Def20:
  for I being Instruction of S holds I is Exec-preserving;
end;

theorem Th44:
  for S being regular standard without_implicit_jumps
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of S st I is sequential holds I is IC-good
proof
  let S be regular standard without_implicit_jumps
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I be Instruction of S such that
A1: I is sequential;
  let k be natural number, s1, s2 be State of S such that
A2: s2 = s1 +* (IC S .--> (IC s1 + k));
  dom (IC S .--> (IC s1 + k)) = {IC S} by FUNCOP_1:19;
  then IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
  then
A3: IC s2 = (IC S .--> (IC s1 + k)).IC S by A2,FUNCT_4:14
    .= il.(S,locnum IC s1 + k) by FUNCOP_1:87;
A4: IC Exec(I, s2) = NextLoc IC s2 by A1,AMISTD_1:def 16
    .= il.(S,locnum IC s1 + k + 1) by A3,AMISTD_1:def 13
    .= il.(S,locnum IC s1 + 1 + k);
  IC Exec(I,s1) = NextLoc IC s1 by A1,AMISTD_1:def 16
    .= il.(S,locnum IC s1 + 1);
  hence IC Exec(I,s1) + k = IC Exec(I,s2) by A4,AMISTD_1:def 13
    .= IC Exec(IncAddr(I,k), s2) by A1,Th24,Th29;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard without_implicit_jumps
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster sequential -> IC-good Instruction of S;
  coherence by Th44;
end;

theorem Th45:
  for S being regular standard without_implicit_jumps realistic
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of S st I is halting holds I is IC-good
proof
  let S be regular standard without_implicit_jumps realistic
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I be Instruction of S such that
A1: I is halting;
  let k be natural number, s1, s2 be State of S such that
A2: s2 = s1 +* (IC S .--> (IC s1 + k));
  dom (IC S .--> (IC s1 + k)) = {IC S} by FUNCOP_1:19;
  then
A3: IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
  thus IC Exec(I,s1) + k = IC s1 + k by A1,AMI_1:def 8
    .= (IC S .--> (IC s1 + k)).IC S by FUNCOP_1:87
    .= IC s2 by A2,A3,FUNCT_4:14
    .= IC Exec(I,s2) by A1,AMI_1:def 8
    .= IC Exec(IncAddr(I,k), s2) by A1,Th23,Th29;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard without_implicit_jumps realistic
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  cluster halting -> IC-good Instruction of S;
  coherence by Th45;
end;

theorem Th46:
  for S being stored-program AMI-Struct over IL,N,
  I being Instruction of S st I is halting holds I is Exec-preserving
proof
  let S be stored-program AMI-Struct over IL,N,
  I be Instruction of S such that
A1: for s being State of S holds Exec(I,s) = s;
  let s1, s2 be State of S such that
A2: s1, s2 equal_outside IL;
  Exec(I,s1) = s1 & Exec(I,s2) = s2 by A1;
  hence thesis by A2;
end;

registration
  let IL;
  let N be with_non-empty_elements set,
  S be stored-program AMI-Struct over IL,N;
  cluster halting -> Exec-preserving Instruction of S;
  coherence by Th46;
end;

registration
  let N be with_non-empty_elements set;
  cluster STC N -> IC-good Exec-preserving;
  coherence
  proof
    thus STC N is IC-good
    proof
      let I be Instruction of STC N, k be natural number,
      s1, s2 be State of STC N such that
A1:   s2 = s1 +* (IC STC N .--> (IC s1 + k));
      {IC STC N} = dom (IC STC N .--> (IC s1 + k)) by FUNCOP_1:19;
      then IC STC N in dom (IC STC N .--> (IC s1 + k)) by TARSKI:def 1;
      then
A2:   IC s2 = (IC STC N .--> (IC s1 + k)).IC STC N by A1,FUNCT_4:14
        .= IC s1 + k by FUNCOP_1:87;
      per cases by AMISTD_1:22;
      suppose
A3:     InsCode I = 1;
        then
A4:     InsCode IncAddr(I,k) = 1 by Def14;
        Exec(I,s1).IC STC N = NextLoc IC s1 by A3,AMISTD_1:38
          .= il.(STC N,locnum IC s1 + 1);
        then locnum IC Exec(I,s1) = locnum IC s1 + 1 by AMISTD_1:def 13;
        hence IC Exec(I,s1) + k = locnum IC s1 + k + 1 by AMISTD_1:37
          .= locnum (IC s1 + k) + 1 by AMISTD_1:33
          .= NextLoc IC s2 by A2,AMISTD_1:37
          .= IC Exec(IncAddr(I,k), s2) by A4,AMISTD_1:38;
      end;
      suppose InsCode I = 0;
        then
A5:     I is halting by AMISTD_1:20;
        then
A6:     IncAddr(I,k) is halting by Th23,Th29;
        thus IC Exec(I,s1) + k = IC s1 + k by A5,AMI_1:def 8
          .= IC Exec(IncAddr(I,k), s2) by A2,A6,AMI_1:def 8;
      end;
    end;
    let I be Instruction of STC N;
    per cases by AMISTD_1:22;
    suppose
A7:   InsCode I = 1;
      the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
      then
A8:   I = [0,0] or I = [1,0] by TARSKI:def 2;
      let s1, s2 be State of STC N such that
A9:   s1, s2 equal_outside NAT;
      consider f being Function of product the Object-Kind of STC N,
      product the Object-Kind of STC N such that
A10:  for s being Element of product the Object-Kind of STC N
      holds f.s = s+*(NAT .-->succ(s.NAT)) and
A11:  the Execution of STC N
      = ([1,0] .--> f) +* ([0,0] .--> id product the Object-Kind of STC N)
      by AMISTD_1:def 11;
      [0,0] <> [1,0] by ZFMISC_1:33;
      then not I in {[0,0]} by A7,A8,MCART_1:7,TARSKI:def 1;
      then not I in dom ([0,0] .--> id product the Object-Kind of STC N)
      by FUNCOP_1:19;
      then
A12:  (the Execution of STC N).I = ([1,0] .--> f).I by A11,FUNCT_4: 12;
A13:  I in {[1,0]} by A7,A8,MCART_1:7,TARSKI:def 1;
      then
A14:  Exec(I,s1) = f.s1 by A12,FUNCOP_1:13
        .= s1+*(NAT .-->succ(s1.NAT)) by A10;
A15:  Exec(I,s2) = f.s2 by A12,A13,FUNCOP_1:13
        .= s2+*(NAT .-->succ(s2.NAT)) by A10;
      dom Exec(I,s1) = dom the Object-Kind of STC N by CARD_3:18;
      then
A16:  dom Exec(I,s1) = dom Exec(I,s2) by CARD_3:18;
      for x being set st x in dom Exec(I,s1) \ NAT
      holds Exec(I,s1).x = Exec(I,s2).x
      proof
        let x be set;
        assume
A17:    x in dom Exec(I,s1) \ NAT;
        then
A18:    not x in NAT by XBOOLE_0:def 4;
A19:    s1.NAT = IC s1 by AMISTD_1:def 11
          .= IC s2 by A9,AMI_1:121
          .= s2.NAT by AMISTD_1:def 11;
        x in dom Exec(I,s1) by A17;
        then x in the carrier of STC N by AMI_1:79;
        then x in NAT \/ {NAT} by AMISTD_1:def 11;
        then
A20:    x in {NAT} by A18,XBOOLE_0:def 2;
        then
A21:    x in dom (NAT .-->succ(s2.NAT)) by FUNCOP_1:19;
        x in dom (NAT .-->succ(s1.NAT)) by A20,FUNCOP_1:19;
        hence Exec(I,s1).x = (NAT .-->succ(s1.NAT)).x by A14,FUNCT_4:14
          .= Exec(I,s2).x by A15,A19,A21,FUNCT_4:14;
      end;
      hence Exec(I,s1)|(dom Exec(I,s1) \ NAT) =
      Exec(I,s2)|(dom Exec(I,s2) \ NAT) by A16,FUNCT_1:165;
    end;
    suppose InsCode I = 0;
      hence thesis by Th46,AMISTD_1:20;
    end;
  end;
end;

registration
  let N be with_non-empty_elements set;
  cluster halting realistic steady-programmed programmable
    with_explicit_jumps without_implicit_jumps IC-good Exec-preserving
    (regular standard (standard-ins IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N)));
  existence
  proof
    take STC N;
    thus thesis;
  end;
end;

registration
  let IL;
  let N be with_non-empty_elements set;
  cluster regular (standard-ins IC-Ins-separated definite
    (non empty stored-program AMI-Struct over IL,N));
  existence
  proof
    take Trivial-AMI(IL,N);
    thus thesis;
  end;
end;

registration
  let IL be non empty set;
  let N be with_non-empty_elements set;
  cluster Trivial-AMI(IL,N) -> Exec-preserving;
  coherence
  proof
    let I be Instruction of Trivial-AMI(IL,N);
    thus thesis by Th46,AMISTD_1:56;
  end;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set;
  cluster halting realistic steady-programmed programmable
    with_explicit_jumps without_implicit_jumps Exec-preserving
    (regular (standard-ins IC-Ins-separated definite
    (non empty stored-program AMI-Struct over IL,N)));
  existence
  proof
    take Trivial-AMI(IL,N);
    thus thesis;
  end;
end;

registration
  let N be with_non-empty_elements set, S be IC-good (regular standard
  (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)));
  cluster -> IC-good Instruction of S;
  coherence by Def18;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set,
  S be Exec-preserving (stored-program AMI-Struct over IL,N);
  cluster -> Exec-preserving Instruction of S;
  coherence by Def20;
end;

definition
  let N be with_non-empty_elements set;
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F be non empty programmed FinPartState of S;
  func CutLastLoc F -> FinPartState of S equals
  F \ ( LastLoc F .--> F.LastLoc F );
  coherence by CARD_3:80;
end;

theorem Th47:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being non empty programmed FinPartState of S
  holds dom CutLastLoc F = (dom F) \ {LastLoc F}
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be non empty programmed FinPartState of S;
A1: dom (LastLoc F .--> (F.LastLoc F)) = {LastLoc F} by FUNCOP_1:19;
  reconsider R = {[LastLoc F, F.LastLoc F]} as Relation;
A2: R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:87;
  then
A3: dom R = {LastLoc F} by FUNCOP_1:19;
  thus dom CutLastLoc F c= (dom F) \ {LastLoc F}
  proof
    let x be set;
    assume x in dom CutLastLoc F;
    then consider y being set such that
A4: [x,y] in F \ R by A2,RELAT_1:def 4;
A5: [x,y] in F & not [x,y] in R by A4,XBOOLE_0:def 4;
A6: x in dom F by A4,RELAT_1:def 4;
    per cases by A5,TARSKI:def 1;
    suppose x <> LastLoc F;
      then not x in dom R by A3,TARSKI:def 1;
      hence thesis by A1,A2,A6,XBOOLE_0:def 4;
    end;
    suppose
A7:   y <> F.LastLoc F;
      now
        assume x in dom R;
        then x = LastLoc F by A3,TARSKI:def 1;
        hence contradiction by A4,A7,FUNCT_1:8;
      end;
      hence thesis by A1,A2,A6,XBOOLE_0:def 4;
    end;
  end;
  thus thesis by A1,RELAT_1:15;
end;

theorem Th48:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being non empty programmed FinPartState of S
  holds dom F = dom CutLastLoc F \/ {LastLoc F}
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be non empty programmed FinPartState of S;
  LastLoc F in dom F by AMISTD_1:51;
  then
A1: {LastLoc F} c= dom F by ZFMISC_1:37;
  dom CutLastLoc F = (dom F) \ {LastLoc F} by Th47;
  hence thesis by A1,XBOOLE_1:45;
end;

registration
  let N be with_non-empty_elements set;
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F be non empty trivial programmed FinPartState of S;
  cluster CutLastLoc F -> empty;
  coherence
  proof
    LastLoc F in dom F by AMISTD_1:51;
    then
A1: [LastLoc F,F.LastLoc F] in F by FUNCT_1:def 4;
    assume not thesis;
    then consider a being set such that
A2: a in CutLastLoc F by XBOOLE_0:def 1;
A3: a = [LastLoc F,F.LastLoc F] by A1,A2,YELLOW_8:def 1;
    not a in LastLoc F .--> F.LastLoc F by A2,XBOOLE_0:def 4;
    then not a in {[LastLoc F,F.LastLoc F]} by FUNCT_4:87;
    hence thesis by A3,TARSKI:def 1;
  end;
end;

registration
  let N be with_non-empty_elements set;
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F be non empty programmed FinPartState of S;
  cluster CutLastLoc F -> programmed;
  coherence by Th12;
end;

registration
  let N be with_non-empty_elements set;
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F be lower non empty programmed FinPartState of S;
  cluster CutLastLoc F -> lower;
  coherence
  proof
    set G = CutLastLoc F;
    per cases;
    suppose G is empty;
      then reconsider H = G as empty FinPartState of S;
      H is lower;
      hence thesis;
    end;
    suppose G is non empty;
      then reconsider G as non empty FinPartState of S;
      G is lower
      proof
        let l be Instruction-Location of S such that
A1:     l in dom G;
        let m be Instruction-Location of S such that
A2:     m <= l;
        consider M being finite non empty natural-membered set such that
A3:     M = { locnum w where w is Instruction-Location of S : w in dom F } and
A4:     LastLoc F = il.(S, max M) by AMISTD_1:def 21;
        reconsider R = {[LastLoc F, F.LastLoc F]} as Relation;
        R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:87;
        then
A5:     dom R = {LastLoc F} by FUNCOP_1:19;
        then
A6:     dom F \ dom R = dom G by Th47;
        then
A7:     m in dom F by A1,A2,AMISTD_1:def 20;
        locnum l in M by A1,A3,A6;
        then
A8:     locnum l <= max M by PRE_CIRC:def 1;
        now
          assume m = LastLoc F;
          then LastLoc F <= il.(S,locnum l) by A2,AMISTD_1:def 13;
          then max M <= locnum l by A4,AMISTD_1:28;
          then il.(S,locnum l) = il.(S,max M) by A8,XXREAL_0:1;
          then LastLoc F in dom G by A1,A4,AMISTD_1:def 13;
          then not LastLoc F in {LastLoc F} by A5,A6,XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
        end;
        then not m in {LastLoc F} by TARSKI:def 1;
        hence m in dom G by A5,A6,A7,XBOOLE_0:def 4;
      end;
      hence thesis;
    end;
  end;
end;

theorem Th49:
  for S being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being non empty programmed FinPartState of S
  holds card CutLastLoc F = card F - 1
proof
  let S be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be non empty programmed FinPartState of S;
  LastLoc F .--> F.LastLoc F c= F
  proof
    let a, b be set;
    assume [a,b] in LastLoc F .--> F.LastLoc F;
    then [a,b] in {[LastLoc F,F.LastLoc F]} by FUNCT_4:87;
    then
A1: [a,b] = [LastLoc F,F.LastLoc F] by TARSKI:def 1;
    LastLoc F in dom F by AMISTD_1:51;
    hence [a,b] in F by A1,FUNCT_1:def 4;
  end;
  hence card CutLastLoc F = card F - card (LastLoc F .--> F.LastLoc F)
  by CARD_2:63
    .= card F - card {[LastLoc F,F.LastLoc F]} by FUNCT_4:87
    .= card F - 1 by CARD_1:79;
end;

theorem Th50:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being lower non empty programmed FinPartState of S,
  G being non empty programmed FinPartState of S
  holds dom CutLastLoc F misses dom Shift(IncAddr(G,card F -' 1),card F -' 1)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower non empty programmed FinPartState of S,
  G be non empty programmed FinPartState of S;
  set k = card F -' 1;
  assume not thesis;
  then consider il being set such that
A1: il in dom CutLastLoc F /\ dom Shift(IncAddr(G,k),k) by XBOOLE_0:4;
A2: il in dom CutLastLoc F by A1,XBOOLE_0:def 3;
A3: il in dom Shift(IncAddr(G,k),k) by A1,XBOOLE_0:def 3;
  dom Shift(IncAddr(G,k),k) = { il.(S,m+k) where m is Element of NAT:
  il.(S,m) in dom IncAddr(G,k) } by Def16;
  then consider m being Element of NAT such that
A4: il = il.(S,m+k) and il.(S,m) in dom IncAddr(G,k) by A3;
  reconsider f = CutLastLoc F as non empty programmed FinPartState of S
  by A1,RELAT_1:60;
  il.(S,m+k) <= LastLoc f by A2,A4,AMISTD_1:53;
  then il.(S,m+k) <= il.(S, card f -' 1) by AMISTD_1:55;
  then
A5: m+k <= card f -' 1 by AMISTD_1:28;
A6: card f = card F - 1 by Th49
    .= card F -' 1 by PRE_CIRC:25;
  per cases;
  suppose k - 1 >= 0;
    then m + k <= k - 1 by A5,A6,BINARITH:def 3;
    then m + k - k <= k - 1 - k by XREAL_1:11;
    hence thesis by Lm1;
  end;
  suppose k - 1 < 0;
    then m + k = 0 or m + k < 0 by A5,A6,BINARITH:def 3;
    then m = 0 & k = 0 by NAT_1:7;
    hence thesis by A6;
  end;
end;

theorem Th51:
  for S being standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being unique-halt (lower non empty programmed FinPartState of S),
  I being Instruction-Location of S st I in dom CutLastLoc F
  holds (CutLastLoc F).I <> halt S
proof
  let S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be unique-halt (lower non empty programmed FinPartState of S),
  I be Instruction-Location of S such that
A1: I in dom CutLastLoc F and
A2: (CutLastLoc F).I = halt S;
A3: dom CutLastLoc F c= dom F by GRFUNC_1:8;
  F.I = halt S by A1,A2,GRFUNC_1:8;
  then
A4: I = LastLoc F by A1,A3,AMISTD_1:def 23;
  dom CutLastLoc F = (dom F) \ {LastLoc F} by Th47;
  then not I in {LastLoc F} by A1,XBOOLE_0:def 4;
  hence thesis by A4,TARSKI:def 1;
end;

definition
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G be non empty programmed FinPartState of S;
  func F ';' G -> FinPartState of S equals
  CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1);
  coherence;
end;

registration
  let N be with_non-empty_elements set,
  S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G be non empty programmed FinPartState of S;
  cluster F ';' G -> non empty programmed;
  coherence;
end;

theorem Th52:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F being lower non empty programmed FinPartState of S,
  G being non empty programmed FinPartState of S
  holds card (F ';' G) = card F + card G - 1 &
  card (F ';' G) = card F + card G -' 1
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F be lower non empty programmed FinPartState of S,
  G be non empty programmed FinPartState of S;
  set k = card F -' 1;
  dom IncAddr(G,k),dom Shift(IncAddr(G,k),k) are_equipotent by Th43;
  then
A1: IncAddr(G,k),Shift(IncAddr(G,k),k) are_equipotent by PRE_CIRC:26;
  dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
  hence card (F ';' G)
  = card CutLastLoc F + card Shift(IncAddr(G,k),k) by PRE_CIRC:27
    .= card CutLastLoc F + card IncAddr(G,k) by A1,CARD_1:21
    .= card CutLastLoc F + card dom IncAddr(G,k) by PRE_CIRC:21
    .= card CutLastLoc F + card dom G by Def15
    .= card CutLastLoc F + card G by PRE_CIRC:21
    .= card F - 1 + card G by Th49
    .= card F + card G - 1;
  hence thesis by BINARITH:def 3;
end;

registration
  let N be with_non-empty_elements set;
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F, G be lower non empty programmed FinPartState of S;
  cluster F ';' G -> lower;
  coherence
  proof
    set P = F ';' G;
    let n be Instruction-Location of S such that
A1: n in dom P;
    let f be Instruction-Location of S such that
A2: f <= n;
    set k = card F -' 1;
A3: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by FUNCT_4:def 1;
    per cases by A1,A3,XBOOLE_0:def 2;
    suppose n in dom CutLastLoc F;
      then f in dom CutLastLoc F by A2,AMISTD_1:def 20;
      hence f in dom P by A3,XBOOLE_0:def 2;
    end;
    suppose n in dom Shift(IncAddr(G,k),k);
      then n in { il.(S,w+k) where w is Element of NAT:
      il.(S,w) in dom IncAddr(G,k) } by Def16;
      then consider m being Element of NAT such that
A4:   n = il.(S,m+k) and
A5:   il.(S,m) in dom IncAddr(G,k);
A6:   locnum f <= locnum n by A2,AMISTD_1:29;
A7:   il.(S,m) in dom G by A5,Def15;
      now per cases;
        case
A8:       locnum f < k;
          then locnum f < card F - 1 by PRE_CIRC:25;
          then 1+locnum f < 1 + (card F - 1) by XREAL_1:8;
          then
A9:       il.(S,1+locnum f) in dom F by AMISTD_1:50;
          locnum f <= 1+locnum f by NAT_1:11;
          then il.(S,locnum f) <= il.(S,1+locnum f) by AMISTD_1:28;
          then il.(S,locnum f) in dom F by A9,AMISTD_1:def 20;
          then
A10:      f in dom F by AMISTD_1:def 13;
          now
            assume f = LastLoc F;
            then f = il.(S,k) by AMISTD_1:55;
            hence contradiction by A8,AMISTD_1:def 13;
          end;
          then not f in {LastLoc F} by TARSKI:def 1;
          then f in (dom F) \ {LastLoc F} by A10,XBOOLE_0:def 4;
          hence f in dom CutLastLoc F by Th47;
        end;
        case locnum f >= k;
          then consider l1 being Nat such that
A11:      locnum f = k + l1 by NAT_1:10;
          reconsider l1 as Element of NAT by ORDINAL1:def 13;
A12:      dom Shift(IncAddr(G,k),k) =

{ il.(S,w+k) where w is Element of NAT: il.(S,w) in dom IncAddr(G,k) }
          by Def16;
A13:      f = il.(S,l1+k) by A11,AMISTD_1:def 13;
          locnum f <= k+m by A4,A6,AMISTD_1:def 13;
          then l1 <= m by A11,XREAL_1:8;
          then il.(S,l1) <= il.(S,m) by AMISTD_1:28;
          then il.(S,l1) in dom G by A7,AMISTD_1:def 20;
          then il.(S,l1) in dom IncAddr(G,k) by Def15;
          hence f in dom Shift(IncAddr(G,k),k) by A12,A13;
        end;
      end;
      hence f in dom P by A3,XBOOLE_0:def 2;
    end;
  end;
end;

theorem Th53:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G being lower non empty programmed FinPartState of S
  holds dom F c= dom (F ';' G)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G be lower non empty programmed FinPartState of S;
  set P = F ';' G;
A1: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,card F -' 1),card F -' 1)
  by FUNCT_4:def 1;
A2: dom F = dom CutLastLoc F \/ {LastLoc F} by Th48;
  let x be set;
  assume
A3: x in dom F;
  per cases by A2,A3,XBOOLE_0:def 2;
  suppose x in dom CutLastLoc F;
    hence x in dom P by A1,XBOOLE_0:def 2;
  end;
  suppose
A4: x in {LastLoc F};
    then
A5: x = LastLoc F by TARSKI:def 1;
    reconsider f = x as Instruction-Location of S by A4,TARSKI:def 1;
A6: locnum f = locnum il.(S,card F -' 1) by A5,AMISTD_1:55
      .= card F -' 1 by AMISTD_1:def 13
      .= card F - 1 + 0 by PRE_CIRC:25;
A7: card P = card F + card G - 1 by Th52
      .= card F - 1 + card G;
    locnum f < card P by A6,A7,XREAL_1:8;
    then il.(S,locnum f) in dom P by AMISTD_1:50;
    hence x in dom P by AMISTD_1:def 13;
  end;
end;

theorem Th54:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G being lower non empty programmed FinPartState of S
  holds CutLastLoc F c= CutLastLoc (F ';' G)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G be lower non empty programmed FinPartState of S;
  set k = card F -' 1;
  set P = F ';' G;
A1: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by FUNCT_4:def 1;
A2: dom CutLastLoc F =
  { il.(S,m) where m is Element of NAT: m < card CutLastLoc F } by Th15;
A3: card CutLastLoc P = card P - 1 by Th49
    .= card F + card G - 1 - 1 by Th52
    .= card F - 1 + (card G - 1);
A4: for m being Element of NAT
  st m < card CutLastLoc F holds m < card CutLastLoc P
  proof
    let m be Element of NAT such that
A5: m < card CutLastLoc F;
A6: card CutLastLoc F = card F - 1 by Th49;
    1 <= card G by NAT_1:14;
    then 1 - 1 <= card G - 1 by XREAL_1:11;
    then card F - 1 + 0 <= card F - 1 + (card G - 1) by XREAL_1:8;
    hence m < card CutLastLoc P by A3,A5,A6,XXREAL_0:2;
  end;
A7: dom CutLastLoc F c= dom CutLastLoc P
  proof
    let x be set;
    assume x in dom CutLastLoc F;
    then consider m being Element of NAT such that
A8: x = il.(S,m) and
A9: m < card CutLastLoc F by A2;
    m < card CutLastLoc P by A4,A9;
    hence x in dom CutLastLoc P by A8,AMISTD_1:50;
  end;
  for x being set st x in dom CutLastLoc F holds
  (CutLastLoc F).x = (CutLastLoc P).x
  proof
    let x be set;
    assume
A10: x in dom CutLastLoc F;
    then consider m being Element of NAT such that
A11: x = il.(S,m) and
A12: m < card CutLastLoc F by A2;
A13: dom Shift(IncAddr(G,k),k) = { il.(S,w+k) where w is Element of NAT:
    il.(S,w) in dom IncAddr(G,k) } by Def16;
A14: now
      assume x in dom Shift(IncAddr(G,k),k);
      then consider w being Element of NAT such that
A15:  x = il.(S,w+k) and il.(S,w) in dom IncAddr(G,k) by A13;
      m < card F - 1 by A12,Th49;
      then
A16:  m < k by PRE_CIRC:25;
      m = w+k by A11,A15,AMISTD_1:25;
      hence contradiction by A16,NAT_1:11;
    end;
A17: x in dom P by A1,A10,XBOOLE_0:def 2;
    now
      assume x = LastLoc P;
      then il.(S,m) = il.(S,card P -' 1) by A11,AMISTD_1:55;
      then
A18:  m = card P -' 1 by AMISTD_1:25
        .= card P - 1 by PRE_CIRC:25;
      card CutLastLoc P = card P - 1 by Th49;
      hence contradiction by A4,A12,A18;
    end;
    then not x in {LastLoc P} by TARSKI:def 1;
    then not x in dom ( LastLoc P .--> P.LastLoc P ) by FUNCOP_1:19;
    then x in dom P \ dom ( LastLoc P .--> P.LastLoc P ) by A17,
    XBOOLE_0:def 4;
    hence (CutLastLoc P).x = (CutLastLoc F +* Shift(IncAddr(G,k),k)).x
    by GRFUNC_1:93
      .= (CutLastLoc F).x by A14,FUNCT_4:12;
  end;
  hence CutLastLoc F c= CutLastLoc P by A7,GRFUNC_1:8;
end;

theorem Th55:
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G being lower non empty programmed FinPartState of S
  holds (F ';' G).LastLoc F = IncAddr(G,card F -' 1).il.(S,0)
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G be lower non empty programmed FinPartState of S;
  set k = card F -' 1;
A1: LastLoc F = il.(S,0+k) by AMISTD_1:55;
A2: il.(S,0) in dom IncAddr(G,k) by AMISTD_1:49;
  dom Shift(IncAddr(G,k),k) =
  {il.(S,m+k) where m is Element of NAT: il.(S,m) in dom IncAddr(G,k)}
  by Def16;
  then LastLoc F in dom Shift(IncAddr(G,k),k) by A1,A2;
  hence (F ';' G).LastLoc F = (Shift(IncAddr(G,k),k)).LastLoc F by FUNCT_4:14
    .= IncAddr(G,k).il.(S,0) by A1,A2,Def16;
end;

theorem
  for S being regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G being lower non empty programmed FinPartState of S,
  f being Instruction-Location of S st locnum f < card F - 1
  holds IncAddr(F,card F -' 1).f = IncAddr(F ';' G, card F -' 1).f
proof
  let S be regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  F, G be lower non empty programmed FinPartState of S,
  f be Instruction-Location of S;
  set k = card F -' 1, P = F ';' G;
  assume locnum f < card F - 1;
  then locnum f < card CutLastLoc F by Th49;
  then
A1: il.(S,locnum f) in dom CutLastLoc F by AMISTD_1:50;
A2: f = il.(S,locnum f) by AMISTD_1:def 13;
A3: dom CutLastLoc F c= dom F by GRFUNC_1:8;
  CutLastLoc F c= CutLastLoc P & CutLastLoc P c= P by Th54;
  then CutLastLoc F c= P by XBOOLE_1:1;
  then
A4: dom CutLastLoc F c= dom P by GRFUNC_1:8;
A5: F.il.(S,locnum f) = pi(F,il.(S,locnum f)) by A1,A3,AMI_1:def 47;
  dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
  then dom CutLastLoc F /\ dom Shift(IncAddr(G,k),k) = {} by XBOOLE_0:def 7;
  then not il.(S,locnum f) in dom Shift(IncAddr(G,k),k) by A1,XBOOLE_0:def 3;
  then
A6: P.il.(S,locnum f) = (CutLastLoc F).il.(S,locnum f) by FUNCT_4:12
    .= F.il.(S,locnum f) by A1,GRFUNC_1:8;
  thus IncAddr(F,k).f = IncAddr(pi(F,il.(S,locnum f)),k) by A1,A2,A3,Def15
    .= IncAddr(pi(P,il.(S,locnum f)),k) by A1,A4,A5,A6,AMI_1:def 47
    .= IncAddr(P,k).f by A1,A2,A4,Def15;
end;

registration
  let N be with_non-empty_elements set;
  let S be regular standard realistic halting steady-programmed
  without_implicit_jumps (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F be lower non empty programmed FinPartState of S;
  let G be halt-ending (lower non empty programmed FinPartState of S);
  cluster F ';' G -> halt-ending;
  coherence
  proof
    set P = F ';' G, k = card F -' 1;
A1: dom Shift(IncAddr(G,k),k) = { il.(S,m+k) where m is Element of NAT:
    il.(S,m) in dom IncAddr(G,k) } by Def16;
A2: il.(S, card G -' 1) = LastLoc G by AMISTD_1:55;
    then
A3: il.(S, card G -' 1) in dom G by AMISTD_1:51;
    then
A4: il.(S, card G -' 1) in dom IncAddr(G,k) by Def15;
    then
A5: il.(S, k + (card G -' 1)) in dom Shift(IncAddr(G,k),k) by A1;
A6: pi(G,il.(S,card G -' 1)) = G.il.(S,card G -' 1) by A3,AMI_1:def 47
      .= halt S by A2,AMISTD_1:def 22;
A8: card G - 1 >= 0 by NAT_1:14,XREAL_1:50;
    then k + (card G - 1) >= k+0 by XREAL_1:8;
    then
A9: k + card G -' 1 = k + card G - 1 by BINARITH:def 3
      .= k + (card G - 1)
      .= k + (card G -' 1) by A8,BINARITH:def 3;
    thus P.(LastLoc P) = P.il.(S,card P -' 1) by AMISTD_1:55
      .= P.il.(S, card F + card G -' 1 -' 1) by Th52
      .= P.il.(S, k + card G -' 1) by BINARITH:56,NAT_1:14
      .= Shift(IncAddr(G,k),k).il.(S, k + (card G -' 1)) by A5,A9,FUNCT_4:14
      .= IncAddr(G,k).il.(S,card G -' 1) by A4,Def16
      .= IncAddr(pi(G,il.(S,card G -' 1)),k) by A3,Def15
      .= halt S by A6,Th29;
  end;
end;

registration
  let N be with_non-empty_elements set;
  let S be regular standard realistic halting steady-programmed
  without_implicit_jumps (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F, G be halt-ending unique-halt
  (lower non empty programmed FinPartState of S);
  cluster F ';' G -> unique-halt;
  coherence
  proof
    set P = F ';' G, k = card F -' 1;
A1: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by FUNCT_4:def 1;
A2: dom Shift(IncAddr(G,k),k) = { il.(S,m+k) where m is Element of NAT:
    il.(S,m) in dom IncAddr(G,k) } by Def16;
A4: card G - 1 >= 0 by NAT_1:14,XREAL_1:50;
    then k + (card G - 1) >= k+0 by XREAL_1:8;
    then
A5: k + card G -' 1 = k + card G - 1 by BINARITH:def 3
      .= k + (card G - 1)
      .= k + (card G -' 1) by A4,BINARITH:def 3;
    let f be Instruction-Location of S such that
A6: P.f = halt S and
A7: f in dom P;
    per cases by A1,A7,XBOOLE_0:def 2;
    suppose
A8:   f in dom CutLastLoc F;
      then
A9:   (CutLastLoc F).f <> halt S by Th51;
      dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
      then CutLastLoc F c= P by FUNCT_4:33;
      hence f = LastLoc P by A6,A8,A9,GRFUNC_1:8;
    end;
    suppose
A10:  f in dom Shift(IncAddr(G,k),k);
      then consider m being Element of NAT such that
A11:  f = il.(S,m+k) and
A12:  il.(S,m) in dom IncAddr(G,k) by A2;
A13:  il.(S,m) in dom G by A12,Def15;
      then
A14:  pi(G,il.(S,m)) = G.il.(S,m) by AMI_1:def 47;
      IncAddr(pi(G,il.(S,m)),k) = IncAddr(G,k).il.(S,m) by A13,Def15
        .= Shift(IncAddr(G,k),k).il.(S,m+k) by A12,Def16
        .= halt S by A6,A10,A11,FUNCT_4:14;
      then G.il.(S,m) = halt S by A14,Th35;
      then il.(S,m) = LastLoc G by A13,AMISTD_1:def 23
        .= il.(S,card G -' 1) by AMISTD_1:55;
      then m = card G -' 1 by AMISTD_1:25;
      then m+k = card F + card G -' 1 -' 1 by A5,BINARITH:56,NAT_1:14
        .= card P -' 1 by Th52;
      hence f = LastLoc P by A11,AMISTD_1:55;
    end;
  end;
end;

definition
  let N be with_non-empty_elements set;
  let S be regular standard realistic halting steady-programmed
  without_implicit_jumps (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
  let F, G be pre-Macro of S;
  redefine func F ';' G -> pre-Macro of S;
  coherence;
end;

registration
  let N be with_non-empty_elements set,
  S be realistic halting steady-programmed IC-good Exec-preserving
  (regular standard (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N))),
  F, G be closed lower non empty (programmed FinPartState of S);
  cluster F ';' G -> closed;
  coherence
  proof
    set P = F ';' G, k = card F -' 1;
    let f be Instruction-Location of S such that
A1: f in dom P;
A2: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by FUNCT_4:def 1;
    dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
    then
A3: dom CutLastLoc F /\ dom Shift(IncAddr(G,k),k) = {} by XBOOLE_0:def 7;
A4: dom CutLastLoc F c= dom F by GRFUNC_1:8;
A5: dom Shift(IncAddr(G,k),k) =
    {il.(S,m+k) where m is Element of NAT: il.(S,m) in dom IncAddr(G,k)}
    by Def16;
    let x be set;
    assume x in NIC(pi(P,f),f);
    then consider s2 being State of S such that
A6: x = IC Following s2 and
A7: IC s2 = f and
A8: s2.f = pi(P,f);
A9: pi(P,f) = P.f by A1,AMI_1:def 47;
    per cases by A1,A2,XBOOLE_0:def 2;
    suppose
A10:  f in dom CutLastLoc F;
      then
A11:  NIC(pi(F,f),f) c= dom F by A4,AMISTD_1:def 17;
      not f in dom Shift(IncAddr(G,k),k) by A3,A10,XBOOLE_0:def 3;
      then s2.f = (CutLastLoc F).f by A8,A9,FUNCT_4:12
        .= F.f by A10,GRFUNC_1:8
        .= pi(F,f) by A4,A10,AMI_1:def 47;
      then IC Following s2 in NIC(pi(F,f),f) by A7;
      then
A12:  x in dom F by A6,A11;
      dom F c= dom P by Th53;
      hence x in dom P by A12;
    end;
    suppose
A13:  f in dom Shift(IncAddr(G,k),k);
      then consider m being Element of NAT such that
A14:  f = il.(S,m+k) and
A15:  il.(S,m) in dom IncAddr(G,k) by A5;
A16:  il.(S,m) in dom G by A15,Def15;
      then
A17:  NIC(pi(G,il.(S,m)),il.(S,m)) c= dom G by AMISTD_1:def 17;
A18:  ObjectKind IC S = NAT by AMI_1:def 11;
      il.(S,m) in NAT by AMI_1:def 4;
      then reconsider v = IC S .--> il.(S,m) as FinPartState of S
      by A18,AMI_1:59;
      set s1 = s2 +* v;
A19:  pi(P,f) = Shift(IncAddr(G,k),k).f by A9,A13,FUNCT_4:14
        .= IncAddr(G,k).il.(S,m) by A14,A15,Def16;
A20:  (IC S .--> il.(S,m)).IC S = il.(S,m) by FUNCOP_1:87;
A21:  IC S in {IC S} by TARSKI:def 1;
A22:  dom (IC S .--> il.(S,m)) = {IC S} by FUNCOP_1:19;
      then
A23:  IC s1 = il.(S,m) by A20,A21,FUNCT_4:14;
A24:  dom s2 = the carrier of S by AMI_1:79;
      IC s1 + k in NAT by AMI_1:def 4;
      then reconsider w = IC S .--> (IC s1 + k) as FinPartState of S
      by A18,AMI_1:59;
      s1 +* w is State of S;
      then
A25:  dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by AMI_1:79;
      for a being set st a in dom s2 holds
      s2.a = (s1 +* (IC S .--> (IC s1 + k))).a
      proof
        let a be set such that a in dom s2;
A26:    dom (IC S .--> (IC s1 + k)) = {IC S} by FUNCOP_1:19;
        per cases;
        suppose
A27:      a = IC S;
          hence s2.a = il.(S,locnum IC s1 + k) by A7,A14,A23,AMISTD_1:def 13
            .= (IC S .--> (IC s1 + k)).a by A27,FUNCOP_1:87
            .= (s1 +* (IC S .--> (IC s1 + k))).a by A21,A26,A27,FUNCT_4:14;
        end;
        suppose
A28:      a <> IC S;
          then
A29:      not a in dom (IC S .--> (IC s1 + k)) by A26,TARSKI:def 1;
          not a in dom (IC S .--> il.(S,m)) by A22,A28,TARSKI:def 1;
          then s1.a = s2.a by FUNCT_4:12;
          hence s2.a = (s1 +* (IC S .--> (IC s1 + k))).a by A29,FUNCT_4:12;
        end;
      end;
      then
A30:  s2 = s1 +* (IC S .--> (IC s1 + k)) by A24,A25,FUNCT_1:9;
      set s3 = s1 +* (il.(S,m) .--> pi(G,il.(S,m)));
A31:  dom (il.(S,m) .--> pi(G,il.(S,m))) = {il.(S,m)} by FUNCOP_1:19;
      then
A32:  il.(S,m) in dom (il.(S,m) .--> pi(G,il.(S,m))) by TARSKI:def 1;
      now
        assume IC S in dom (il.(S,m) .--> pi(G,il.(S,m)));
        then reconsider l=IC S as Instruction-Location of S
        by A31,TARSKI:def 1;
        l=IC S;
        hence contradiction by AMI_1:48;
      end;
      then
A33:  IC s3 = s1.IC S by FUNCT_4:12
        .= il.(S,m) by A20,A21,A22,FUNCT_4:14;
A34:  s3.il.(S,m) = (il.(S,m) .--> pi(G,il.(S,m))).il.(S,m) by A32,FUNCT_4:14
        .= pi(G,il.(S,m)) by FUNCOP_1:87;
      s1, s3 equal_outside NAT
      proof
A35:    dom s1 = the carrier of S & dom s3 = the carrier of S by AMI_1:79;
        for x being set st x in dom s1 \ NAT holds s1.x = s3.x
        proof
          let x be set;
A36:      dom (il.(S,m) .--> pi(G,il.(S,m))) c= NAT by AMI_1:def 40;
          assume x in dom s1 \ NAT;
          then not x in dom (il.(S,m) .--> pi(G,il.(S,m)))
          by A36,XBOOLE_0:def 4;
          hence s1.x = s3.x by FUNCT_4:12;
        end;
        hence s1|(dom s1 \ NAT) = s3|(dom s3 \ NAT) by A35,FUNCT_1:165;
      end;
      then
A37:  Exec(pi(G,il.(S,m)),s1), Exec(pi(G,il.(S,m)),s3)
      equal_outside NAT by Def19;
      reconsider k,m as Element of NAT;
A38:  x = IC Exec(IncAddr(pi(G,il.(S,m)),k),s2) by A6,A7,A8,A16,A19,Def15
        .= IC Exec(pi(G,il.(S,m)), s1) + k by A30,Def17
        .= il.(S,locnum IC Exec(pi(G,il.(S,m)), s3) + k) by A37,AMI_1:121;
      IC Following s3 = il.(S,locnum IC Exec(pi(G,il.(S,m)), s3))
      by A33,A34,AMISTD_1:def 13;

then il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in NIC(pi(G,il.(S,m)),il.(S
      ,m)) by A33,A34;
      then il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in dom G by A17;
      then
A39:  il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in dom IncAddr(G,k) by Def15;
      x in dom Shift(IncAddr(G,k),k) by A5,A38,A39;
      hence x in dom P by A2,XBOOLE_0:def 2;
    end;
  end;
end;

theorem Th57:
  for S being regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N))
  holds IncAddr(Stop S, k) = Stop S
proof
  let S be regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
A1: dom IncAddr(Stop S, k) = dom Stop S by Def15
    .= {il.(S,0)} by Lm5;
A2: dom Stop S = {il.(S,0)} by Lm5;
  for x being set st x in {il.(S,0)} holds IncAddr(Stop S, k).x = (Stop S). x
  proof
    let x be set;
    assume
A3: x in {il.(S,0)};
    then
A4: x = il.(S,0) by TARSKI:def 1;
    then
A5: pi(Stop S,il.(S,0)) = (Stop S).il.(S,0) by A2,A3,AMI_1:def 47
      .= halt S by FUNCOP_1:87;
    thus IncAddr(Stop S, k).x
    = IncAddr(pi(Stop S,il.(S,0)),k) by A2,A3,A4,Def15
      .= halt S by A5,Th29
      .= (Stop S).x by A4,FUNCOP_1:87;
  end;
  hence IncAddr(Stop S, k) = Stop S by A1,A2,FUNCT_1:9;
end;

theorem Th58:
  for S being standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N))
  holds Shift(Stop S, k) = il.(S,k) .--> halt S
proof
  let S be standard halting (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N));
A1: dom Shift(Stop S,k) =
  {il.(S,m+k) where m is Element of NAT: il.(S,m) in dom Stop S} by Def16;
A2: il.(S,0) in dom Stop S by Lm5;
A3: dom Shift(Stop S,k) = {il.(S,k)}
  proof
    hereby
      let x be set;
      assume x in dom Shift(Stop S,k);
      then consider m being Element of NAT such that
A4:   x = il.(S,m+k) and
A5:   il.(S,m) in dom Stop S by A1;
      il.(S,m) in {il.(S,0)} by A5,Lm5;
      then il.(S,m) = il.(S,0) by TARSKI:def 1;
      then m = 0 by AMISTD_1:25;
      hence x in {il.(S,k)} by A4,TARSKI:def 1;
    end;
    let x be set;
    assume x in {il.(S,k)};
    then x = il.(S,0+k) by TARSKI:def 1;
    hence thesis by A1,A2;
  end;
A6: dom (il.(S,k) .--> halt S) = {il.(S,k)} by FUNCOP_1:19;
  for x being set st x in {il.(S,k)} holds
  (Shift(Stop S, k)).x = (il.(S,k) .--> halt S).x
  proof
    let x be set;
    assume x in {il.(S,k)};
    then
A7: x = il.(S,0+k) by TARSKI:def 1;
    il.(S,0) in dom Stop S by Lm5;
    hence (Shift(Stop S, k)).x = (Stop S).il.(S,0) by A7,Def16
      .= halt S by FUNCOP_1:87
      .= (il.(S,k) .--> halt S).x by A7,FUNCOP_1:87;
  end;
  hence thesis by A3,A6,FUNCT_1:9;
end;

theorem Th59:
  for S being regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F being pre-Macro of S
  holds F ';' Stop S = F
proof
  let S be regular standard halting without_implicit_jumps
  realistic (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F be pre-Macro of S;
  set k = card F -' 1;
A1: F ';' Stop S = CutLastLoc F +* Shift(Stop S,k) by Th57;
A2: dom F = dom CutLastLoc F \/ {LastLoc F} by Th48;
  dom Shift(Stop S,k) = dom (il.(S,k) .--> halt S) by Th58
    .= {il.(S,k)} by FUNCOP_1:19
    .= {LastLoc F} by AMISTD_1:55;
  then
A3: dom (F ';' Stop S) = dom F by A1,A2,FUNCT_4:def 1;
  for x being set st x in dom F holds (F ';' Stop S).x = F.x
  proof
    let x be set such that
A4: x in dom F;
    dom CutLastLoc F misses dom Shift(IncAddr(Stop S,k),k) by Th50;
    then
A5: {} = dom CutLastLoc F /\ dom Shift(IncAddr(Stop S,k),k) by XBOOLE_0:def 7;
    per cases by A2,A4,XBOOLE_0:def 2;
    suppose
A6:   x in dom CutLastLoc F;
      then not x in dom Shift(IncAddr(Stop S,k),k) by A5,XBOOLE_0:def 3;
      hence (F ';' Stop S).x = (CutLastLoc F).x by FUNCT_4:12
        .= F.x by A6,GRFUNC_1:8;
    end;
    suppose x in {LastLoc F};
      then
A7:   x = LastLoc F by TARSKI:def 1;
      then
A8:   x = il.(S,k) by AMISTD_1:55;
A9:   il.(S,0) in dom Stop S by Lm5;
      dom Shift(Stop S,k)
      = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom Stop S }
      by Def16;
      then il.(S,0+k) in dom Shift(Stop S,k) by A9;
      hence (F ';' Stop S).x = Shift(Stop S,0+k).x by A1,A8,FUNCT_4:14
        .= (Stop S).il.(S,0) by A8,A9,Def16
        .= halt S by FUNCOP_1:87
        .= F.x by A7,AMISTD_1:def 22;
    end;
  end;
  hence F ';' Stop S = F by A3,FUNCT_1:9;
end;

theorem Th60:
  for S being regular standard halting (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F being pre-Macro of S
  holds Stop S ';' F = F
proof
  let S be regular standard halting (standard-ins IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), F be pre-Macro of S;
  set k = card Stop S -' 1;
A1: k = 0 by Lm6;
  hence Stop S ';' F = CutLastLoc Stop S +* Shift(F,k) by Th38
    .= CutLastLoc Stop S +* F by A1,Th40
    .= F by FUNCT_4:21;
end;

theorem
  for S being regular standard realistic halting steady-programmed
  without_implicit_jumps (standard-ins IC-Ins-separated
  definite (non empty stored-program AMI-Struct over NAT,N)),
  F, G, H being pre-Macro of S holds F ';' G ';' H = F ';' (G ';' H)
proof
  let S be regular standard realistic halting steady-programmed
  without_implicit_jumps (standard-ins IC-Ins-separated
  definite (non empty stored-program AMI-Struct over NAT,N)),
  F, G, H be pre-Macro of S;
  per cases;
  suppose
A1: F = Stop S;
    hence F ';' G ';' H = G ';' H by Th60
      .= F ';' (G ';' H) by A1,Th60;
  end;
  suppose
A2: G = Stop S;
    hence F ';' G ';' H = F ';' H by Th59
      .= F ';' (G ';' H) by A2,Th60;
  end;
  suppose that
A3: F <> Stop S and
A4: G <> Stop S;
    set X = {il.(S,k) where k is Element of NAT:
    k < card F + card G + card H - 1 - 1};
A5: card (F ';' G ';' H) = card (F ';' G) + card H - 1 by Th52
      .= card F + card G - 1 + card H - 1 by Th52
      .= card F + card G + card H - 1 - 1;
A6: card (F ';' (G ';' H)) = card F + card (G ';' H) - 1 by Th52
      .= card F + (card G + card H - 1) - 1 by Th52
      .= card F + card G + card H - 1 - 1;
A7: dom (F ';' G ';' H) = X by A5,Th15;
A8: dom (F ';' (G ';' H)) = X by A6,Th15;
    for x being set st x in X holds (F ';' G ';' H).x = (F ';' (G ';' H)) . x
    proof
      let x be set;
      assume x in X;
      then consider k being Element of NAT such that
A9:   x = il.(S,k) and
A10:  k < card F + card G + card H - 1 - 1;
A11:  dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) =
      { il.(S,m+(card F -' 1)) where m is Element of NAT:
      il.(S,m) in dom IncAddr(G ';' H,card F -' 1) } by Def16;
A12:  dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1) =
      { il.(S,m+(card (F ';' G) -' 1)) where m is Element of NAT:
      il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) } by Def16;
A13:  dom Shift(IncAddr(H,card G -' 1),card G -' 1) =
      { il.(S,m+(card G -' 1)) where m is Element of NAT:
      il.(S,m) in dom IncAddr(H,card G -' 1) } by Def16;
A14:  card (F ';' G) -' 1 = card (F ';' G) - 1 by PRE_CIRC:25
        .= card F + card G - 1 - 1 by Th52;
      then card (F ';' G) -' 1 = card F - 1 + (card G - 1);
      then
A15:  card (F ';' G) -' 1 = (card G -' 1) + (card F - 1) by PRE_CIRC :25
        .= (card G -' 1) + (card F -' 1) by PRE_CIRC:25;
A16:  dom Shift(IncAddr(G,card F -' 1),card F -' 1) =
      { il.(S,m+(card F -' 1)) where m is Element of NAT:
      il.(S,m) in dom IncAddr(G,card F -' 1) } by Def16;
A17:  card F -' 1 = card F - 1 by PRE_CIRC:25;
A18:  card G -' 1 = card G - 1 by PRE_CIRC:25;
A19:  for W being pre-Macro of S st W <> Stop S holds 2 <= card W
      proof
        let W be pre-Macro of S;
        assume
A20:    W <> Stop S;
        assume 2 > card W;
        then 1 + 1 > card W;
        then card W <= 1 by NAT_1:13;
        hence contradiction by A20,Th26,NAT_1:26;
      end;
      then 2 <= card F by A3;
      then
A22:  1 <= card F by XXREAL_0:2;
A23:  2 <= card G by A4,A19;
      per cases by A22,A23,Lm2;
      suppose
A24:    k < card F - 1;
A25:    CutLastLoc F c= CutLastLoc (F ';' G) by Th54;
A26:    now
          assume x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1);
          then consider m being Element of NAT such that
A27:      x = il.(S,m+(card F -' 1)) and
          il.(S,m) in dom IncAddr(G ';' H,card F -' 1) by A11;
          k = m + (card F -' 1) by A9,A27,AMISTD_1:25
            .= m + (card F - 1) by PRE_CIRC:25;
          then m + (card F - 1) < card F -' 1 by A24,PRE_CIRC:25;
          then m + (card F -' 1) < card F -' 1 by PRE_CIRC:25;
          hence contradiction by NAT_1:11;
        end;
A28:    now
          assume x in dom
          Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1);
          then consider m being Element of NAT such that
A29:      x = il.(S,m+(card (F ';' G) -' 1)) and
          il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) by A12;
          k = m + (card G -' 1) + (card F -' 1) by A9,A15,A29,AMISTD_1:25;
          then m + (card G -' 1) + (card F -' 1) < card F -' 1
          by A24,PRE_CIRC:25;
          hence contradiction by NAT_1:11;
        end;
        k < card CutLastLoc F by A24,Th49;
        then
A30:    x in dom CutLastLoc F by A9,AMISTD_1:50;
        thus (F ';' G ';' H).x = (CutLastLoc (F ';' G)).x by A28,FUNCT_4:12
          .= (CutLastLoc F).x by A25,A30,GRFUNC_1:8
          .= (F ';' (G ';' H)).x by A26,FUNCT_4:12;
      end;
      suppose
A31:    k = card F - 1;
A32:    now
          assume x in dom
          Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1);
          then consider m being Element of NAT such that
A33:      x = il.(S,m+(card (F ';' G) -' 1)) and
          il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) by A12;
          k = m + (card G -' 1) + (card F -' 1) by A9,A15,A33,AMISTD_1:25;
          then m + (card G -' 1) + (card F -' 1) = card F -' 1
          by A31,PRE_CIRC:25;
          then card G -' 1 = 0 by NAT_1:7;
          then card G - 1 = 0 by PRE_CIRC:25;
          hence contradiction by A4,Th26;
        end;
A34:    il.(S,0) in dom IncAddr(G ';' H,card F -' 1) by AMISTD_1:49;
A35:    il.(S,0) in dom IncAddr(G,card F -' 1) by AMISTD_1:49;
A36:    il.(S,0) in dom G by AMISTD_1:49;
A37:    il.(S,0) in dom (G ';' H) by AMISTD_1:49;
        k = 0 + (card F -' 1) by A31,PRE_CIRC:25;
        then
A38:    x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A9,A11
        ,A34;
A39:    k = card F -' 1 by A31,PRE_CIRC:25;
A40:    x = il.(S,0+k) by A9;
        il.(S,0) in dom IncAddr(G,card F -' 1) by AMISTD_1:49;
        then
A41:    x in dom Shift(IncAddr(G,card F -' 1),card F -' 1) by A16, A39,A40;

then x in dom CutLastLoc F \/ dom Shift(IncAddr(G,card F -' 1),card F -' 1)
        by XBOOLE_0:def 2;
        then
A42:    x in dom (F ';' G) by FUNCT_4:def 1;
        now
A43:      dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
          = {LastLoc (F ';' G)} by FUNCOP_1:19
            .= {il.(S,card (F ';' G) -' 1)} by AMISTD_1:55;

assume x in dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ));
          then x = il.(S,card (F ';' G) -' 1) by A43,TARSKI:def 1;
          then k = (card G -' 1) + (card F -' 1) by A9,A15,AMISTD_1:25;
          then card G - 1 = 0 by A39,PRE_CIRC:25;
          hence contradiction by A4,Th26;
        end;
        then
A44:    x in dom (F ';' G) \
        dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
        by A42,XBOOLE_0:def 4;
        card G > 1
        proof
          thus 1 <= card G & 1 <> card G by A4,Th26,NAT_1:14;
        end;
        then
A45:    card G - 1 > 1 - 1 by XREAL_1:11;
        then card G -' 1 > 1 - 1 by PRE_CIRC:25;
        then
A46:    not il.(S,0) in dom Shift(IncAddr(H,card G -' 1), card G -' 1) by
        Th41;
        card CutLastLoc G <> {} by A45,Th49;
        then
A47:    il.(S,0) in dom CutLastLoc G by AMISTD_1:49,CARD_1:78;
A48:    pi(G,il.(S,0)) = G.il.(S,0) by A36,AMI_1:def 47
          .= (CutLastLoc G).il.(S,0) by A47,GRFUNC_1:8
          .= (G ';' H).il.(S,0) by A46,FUNCT_4:12
          .= pi(G ';' H,il.(S,0)) by A37,AMI_1:def 47;
        thus (F ';' G ';' H).x = ((F ';' G) \
        ( LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))).x by A32,
        FUNCT_4:12

.= (CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1)).x by A44
        ,GRFUNC_1:93
          .= Shift(IncAddr(G,card F -' 1),card F -' 1).x by A41,FUNCT_4:14
          .= IncAddr(G,card F -' 1).il.(S,0) by A35,A39,A40,Def16
          .= IncAddr(pi(G ';' H,il.(S,0)),card F -' 1) by A36,A48,Def15
          .= IncAddr(G ';' H,card F -' 1).il.(S,0) by A37,Def15
          .= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x
        by A34,A39,A40,Def16
          .= (F ';' (G ';' H)).x by A38,FUNCT_4:14;
      end;
      suppose that
A49:    card F <= k and
A50:    k <= card F + card G - 3;
A51:    now
          assume
          x in dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1);
          then consider m being Element of NAT such that
A52:      x = il.(S,m+(card (F ';' G) -' 1)) and
          il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) by A12;
          m + ((card G -' 1) + (card F -' 1))
          <= - 1 + ((card G -' 1) + (card F -' 1)) by A9,A15,A17,A18,A50,A52,
          AMISTD_1:25;
          then m <= -1 by XREAL_1:8;
          hence contradiction by Lm1;
        end;
        card F -' 1 <= card F by BINARITH:52;
        then
A53:    x = il.(S, k -' (card F -' 1) + (card F -' 1)) by A9,A49, BINARITH:
        53,XXREAL_0:2;
A54:    card F - card F <= k - card F by A49,XREAL_1:11;
        card F - 1 < card F - 0 by REAL_1:92;
        then k - (card F - 1) >= 0 by A54,REAL_1:92;
        then
A55:    k - (card F -' 1) >= 0 by PRE_CIRC:25;
A56:    card F + card G - 3 < card F + card G - 3 + 1 by XREAL_1:31;
        then
A57:    k < (card G - 1) + (card F - 1) by A50,XXREAL_0:2;
        k - (card F - 1) + (card F - 1) < (card G - 1) + (card F - 1)
        by A50,A56,XXREAL_0:2;
        then k - (card F - 1) < card G - 1 by XREAL_1:9;
        then k - (card F -' 1) < card G - 1 by PRE_CIRC:25;
        then k -' (card F -' 1) < card G - 1 by A55,BINARITH:def 3;
        then k -' (card F -' 1) < card CutLastLoc G by Th49;
        then
A58:    il.(S,k -' (card F -' 1)) in dom CutLastLoc G by AMISTD_1: 50;
        then il.(S,k -' (card F -' 1)) in
        dom CutLastLoc G \/ dom Shift(IncAddr(H,card G -' 1),card G -' 1)
        by XBOOLE_0:def 2;
        then
A59:    il.(S,k -' (card F -' 1)) in dom (G ';' H) by FUNCT_4:def 1;
        then
A60:    il.(S,k -' (card F -' 1)) in dom IncAddr(G ';' H,card F -' 1)
        by Def15;
        then
A61:    x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A11,A53;
        card G + card F - 2 < card F + card G - 1 by REAL_1:92;
        then k < card F + card G - 1 by A57,XXREAL_0:2;
        then k < card (F ';' G) by Th52;
        then
A62:    x in dom (F ';' G) by A9,AMISTD_1:50;
        now
          assume x in dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G));
          then x in {LastLoc (F ';' G)} by FUNCOP_1:19;
          then x = LastLoc (F ';' G) by TARSKI:def 1
            .= il.(S,card (F ';' G) -' 1) by AMISTD_1:55;
          then k = card (F ';' G) -' 1 by A9,AMISTD_1:25
            .= (card G - 1) + (card F - 1) by A15,A18,PRE_CIRC:25;
          hence contradiction by A50,A56;
        end;
        then
A63:    x in dom (F ';' G) \
        dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G))
        by A62,XBOOLE_0:def 4;
A64:    dom CutLastLoc G c= dom G by GRFUNC_1:8;
        then il.(S,k -' (card F -' 1)) in dom G by A58;
        then
A65:    il.(S,k -' (card F -' 1)) in dom IncAddr(G,card F -' 1) by Def15;
        then
A66:    x in dom Shift(IncAddr(G,card F -' 1),card F -' 1) by A16, A53;
A67:    now
          assume il.(S,k -' (card F -' 1)) in
          dom Shift(IncAddr(H,card G -' 1),card G -' 1);
          then consider m being Element of NAT such that
A68:      il.(S,k -' (card F -' 1)) = il.(S,m+(card G -' 1)) and
          il.(S,m) in dom IncAddr(H,card G -' 1) by A13;
          k -' (card F -' 1) = m + (card G -' 1) by A68,AMISTD_1:25;
          then
A69:      m = k -' (card F -' 1) - (card G -' 1)
            .= k - (card F -' 1) - (card G -' 1) by A55,BINARITH:def 3
            .= k - (card F - 1) - (card G -' 1) by PRE_CIRC:25
            .= k - (card F - 1) - (card G - 1) by PRE_CIRC:25
            .= k - (card F + card G - 2);
          k - (card F + card G - 2)
          <= card F + card G - 3 - (card F + card G - 2) by A50,XREAL_1:11;
          hence contradiction by A69,Lm1;
        end;
A70:    pi(G ';' H,il.(S,k -' (card F -' 1)))
        = (CutLastLoc G +* Shift(IncAddr(H,card G -' 1),card G -' 1))
        .il.(S,k -' (card F -' 1)) by A59,AMI_1:def 47
          .= (CutLastLoc G).il.(S,k -' (card F -' 1)) by A67,FUNCT_4:12
          .= G.il.(S,k -' (card F -' 1)) by A58,GRFUNC_1:8;
        thus (F ';' G ';' H).x
        = ((F ';' G) \ (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G))).x
        by A51,FUNCT_4:12

.= (CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1)).x by A63,
        GRFUNC_1:93
          .= Shift(IncAddr(G,card F -' 1),card F -' 1).x by A66,FUNCT_4:14
          .= IncAddr(G,card F -' 1).il.(S,k -' (card F -' 1)) by A53,A65,Def16
          .= IncAddr(pi(G,il.(S,k -' (card F -' 1))),card F -' 1)
        by A58,A64,Def15
          .= IncAddr(pi(G ';' H,il.(S,k -' (card F -' 1))),card F -' 1)
        by A58,A64,A70,AMI_1:def 47
          .= IncAddr(G ';' H,card F -' 1).il.(S,k -' (card F -' 1))
        by A59,Def15
          .= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x by A53,A60,Def16
          .= (F ';' (G ';' H)).x by A61,FUNCT_4:14;
      end;
      suppose
A71:    k = card F + card G - 2;
        then
A72:    x = il.(S,k -' (card (F ';' G) -' 1) + (card (F ';' G) -' 1))
        by A9,A14,BINARITH:53;
        k - (card (F ';' G) -' 1) = 0 by A14,A71;
        then
A73:    k -' (card (F ';' G) -' 1) = 0 by BINARITH:def 3;
        then
A74:    il.(S,k -' (card (F ';' G) -' 1)) in dom IncAddr(H,card (F ';' G)
        -' 1) by AMISTD_1:49;
        then
A75:    x in dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1)
        by A12,A72;
A76:    x = il.(S, (card G -' 1) + (card F -' 1)) by A9,A17,A18,A71;
        card G - 1 + 0 < card G - 1 + card H by XREAL_1:8;
        then card G -' 1 < card G + card H - 1 by PRE_CIRC:25;
        then card G -' 1 < card (G ';' H) by Th52;
        then
A77:    il.(S,card G -' 1) in dom (G ';' H) by AMISTD_1:50;
        then
A78:    il.(S,card G -' 1) in dom IncAddr(G ';' H,card F -' 1) by Def15;
        then
A79:    x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A11,A76;
A80:    il.(S,0) in dom H by AMISTD_1:49;
A81:    pi(G ';' H,il.(S,card G -' 1)) = (G ';' H).il.(S,card G -' 1)
        by A77,AMI_1:def 47;
A82:    il.(S,0) in dom IncAddr(H,card G -' 1) by AMISTD_1:49;
        then
A83:    pi(IncAddr(H,card G -' 1),il.(S,0))
        = IncAddr(H,card G -' 1).il.(S,0) by AMI_1:def 47
          .= IncAddr(pi(H,il.(S,0)),(card G -' 1)) by A80,Def15;
        pi(G ';' H,il.(S,card G -' 1))
        = (G ';' H).LastLoc G by A81,AMISTD_1:55
          .= IncAddr(H,card G -' 1).il.(S,0) by Th55
          .= pi(IncAddr(H,card G -' 1),il.(S,0)) by A82,AMI_1:def 47;
        then
A84:    IncAddr(pi(G ';' H,il.(S,card G -' 1)),card F -' 1)
        = IncAddr(pi(H,il.(S,0)),card (F ';' G) -' 1) by A15,A83,Th37;
        thus (F ';' G ';' H).x
        = Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1).x
        by A75,FUNCT_4:14
          .= IncAddr(H,card (F ';' G) -' 1).il.(S,k -' (card (F ';' G) -' 1))
        by A72,A74,Def16
          .= IncAddr(pi(H,il.(S,0)),card (F ';' G) -' 1) by A73,A80,Def15
          .= IncAddr(G ';' H,card F -' 1).il.(S,card G -' 1) by A77,A84,Def15
          .= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x by A76,A78,Def16
          .= (F ';' (G ';' H)).x by A79,FUNCT_4:14;
      end;
      suppose
A85:    card F + card G - 2 < k;
        then
A86:    x = il.(S,k -' (card (F ';' G) -' 1) + (card (F ';' G) -' 1))
        by A9,A14,BINARITH:53;
        k + 0 < card F + card G - (1 + 1) + card H by A10;
        then k - (card F + card G - (1 + 1)) < card H - 0 by XREAL_1:23;
        then k -' (card (F ';' G) -' 1) < card H by A14,BINARITH:def 3;
        then
A88:    il.(S,k -' (card (F ';' G) -' 1)) in dom H by AMISTD_1:50;
        then
A89:    il.(S,k -' (card (F ';' G) -' 1)) in dom IncAddr(H,card (F ';' G)
        -' 1) by Def15;
        then
A90:    x in dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1)
        by A12,A86;
A91:    card F -' 1 <= (card G -' 1) + (card F -' 1) by NAT_1:11;
        then
A92:    k >= card F -' 1 by A14,A15,A85,XXREAL_0:2;
A93:    x = il.(S,k -' (card F -' 1) + (card F -' 1)) by A9,A14,A15,A85,A91,
        BINARITH:53,XXREAL_0:2;
A94:    k - (card F -' 1) >= 0 by A92,XREAL_1:50;
A95:    k - (card F -' 1) < card F + card G + card H - 1 - 1 - (card F -' 1)
        by A10,XREAL_1:11;
        then
A96:    k -' (card F -' 1) < card F + card G + card H - card F - 1
        by A17,A94,BINARITH:def 3;
        k -' (card F -' 1) < card F - card F + card G + card H - 1
        by A17,A94,A95,BINARITH:def 3;
        then k -' (card F -' 1) < card (G ';' H) by Th52;
        then
A97:    il.(S,k -' (card F -' 1)) in dom (G ';' H) by AMISTD_1:50;
        then il.(S,k -' (card F -' 1)) in dom IncAddr(G ';' H,card F -' 1)
        by Def15;
        then
A98:    x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A11,A93;
A99:    il.(S,k -' (card F -' 1)) in dom IncAddr(G ';' H,card F -' 1)
        by A97,Def15;
A100:   k - (card F -' 1) >= card (F ';' G) -' 1 - (card F -' 1)
        by A14,A85,XREAL_1:11;
        then
A101:   k -' (card F -' 1) >= (card F -' 1) + (card G -' 1) - ( card F -' 1)
        by A14,A15,A85,A91,BINARITH:50,XXREAL_0:2;
A102:   k -' (card F -' 1) >= card G -' 1 by A14,A15,A85,A91,A100,BINARITH:50,
        XXREAL_0:2;
A103:   il.(S,k -' (card F -' 1)) =
        il.(S, k -' (card F -' 1) -' (card G -' 1) + (card G -' 1))
        by A101,BINARITH:53;
        k -' (card F -' 1) - (card G -' 1) < card G + card H - 1 - (card G -
        1) by A18,A96,XREAL_1:11;
        then k -' (card F -' 1) -' (card G -' 1) <
        card H + (card G - 1) - (card G - 1) by A102,BINARITH:50;

then il.(S,k -' (card F -' 1) -' (card G -' 1)) in dom H by AMISTD_1:50;
        then
A104:   il.(S,k -' (card F -' 1) -' (card G -' 1)) in
        dom IncAddr(H,card G -' 1) by Def15;
        then
A105:   il.(S,k -' (card F -' 1)) in
        dom Shift(IncAddr(H,card G -' 1),card G -' 1) by A13,A103;
A106:   k -' (card F -' 1) -' (card G -' 1)
        = k -' (card F -' 1) - (card G -' 1) by A101,BINARITH:50
          .= k - (card F -' 1) - (card G -' 1) by A14,A15,A85,A91,BINARITH:50,
        XXREAL_0:2
          .= k - ((card F -' 1) + (card G -' 1))
          .= k -' (card (F ';' G) -' 1) by A14,A15,A85,BINARITH:50;
A107:   pi(G ';' H,il.(S,k -' (card F -' 1)))
        = ((CutLastLoc G) +* Shift(IncAddr(H,card G -' 1),card G -' 1)).
        il.(S,k -' (card F -' 1)) by A97,AMI_1:def 47

.= Shift(IncAddr(H,card G -' 1),card G -' 1).il.(S,k -' (card F -' 1))
        by A105,FUNCT_4:14

.= IncAddr(H,card G -' 1).il.(S,k -' (card (F ';' G) -' 1)) by A103,A104
        ,A106,Def16
          .= IncAddr(pi(H,il.(S,k -' (card (F ';' G) -' 1))),card G -' 1)
        by A88,Def15;
        thus (F ';' G ';' H).x
        = Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1).x
        by A90,FUNCT_4:14
          .= IncAddr(H,card (F ';' G) -' 1).il.(S,k -' (card (F ';' G) -' 1))
        by A86,A89,Def16

.= IncAddr(pi(H,il.(S,k -' (card (F ';' G) -' 1))),card (F ';' G) -' 1)
        by A88,Def15
          .= IncAddr(pi(G ';' H,il.(S,k -' (card F -' 1))),card F -' 1)
        by A15,A107,Th37
          .= IncAddr(G ';' H,card F -' 1).il.(S,k -' (card F -' 1))
        by A97,Def15
          .= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x by A93,A99,Def16
          .= (F ';' (G ';' H)).x by A98,FUNCT_4:14;
      end;
    end;
    hence thesis by A7,A8,FUNCT_1:9;
  end;
end;

theorem
  for S being regular
  (standard-ins non empty stored-program AMI-Struct over IL,N),
  I being Instruction of S, x being set st x in dom AddressPart I holds
  (AddressPart I).x in (product" AddressParts InsCode I).x
proof
  let S be regular
  (standard-ins non empty stored-program AMI-Struct over IL,N),
  I be Instruction of S, x be set such that
A1: x in dom AddressPart I;
A2: AddressPart I in AddressParts InsCode I;
A3: dom product" AddressParts InsCode I = DOM AddressParts InsCode I
  by CARD_3:92
    .= dom AddressPart I by A2,CARD_3:def 12;
  (AddressPart I).x in pi(AddressParts InsCode I,x) by A2,CARD_3:def 6;
  hence (AddressPart I).x in (product" AddressParts InsCode I).x
  by A1,A3,CARD_3:93;
end;

theorem
  for I being Instruction of Trivial-AMI(IL,N) holds AddressPart I = 0 by Lm3;

theorem
  for T being InsType of Trivial-AMI(IL,N) holds AddressParts T = {0} by Lm4;