:: 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, SGRAPH1, CARD_5, FRECHET, PRE_TOPC,
      RELOC, FUNCT_7, ORDINAL1, SQUARE_1, SCMFSA6A, AMISTD_2, MEMBERED, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED, FINSET_1,
      RELAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, FRAENKEL, REALSET1, FUNCT_4,
      NUMBERS, XCMPLX_0, NAT_1, NAT_D, CARD_3, CARD_1, FINSEQ_1, FINSEQ_2,
      CQC_LANG, BINARITH, FUNCT_7, STRUCT_0, AMI_1, AMI_3, AMI_5, SCMFSA_4,
      PRE_CIRC, PRALG_2, AMISTD_1, XXREAL_0;
 constructors WELLORD2, DOMAIN_1, XXREAL_0, REAL_1, NAT_1, BINARITH, PRE_CIRC,
      FUNCT_7, PRALG_2, AMI_5, SCMFSA_4, AMISTD_1, NAT_D;
 registrations AMI_1, AMISTD_1, XREAL_0, FINSEQ_1, FINSEQ_2, FINSET_1,
      FRAENKEL, FUNCT_7, INT_1, RELAT_1, RELSET_1, SUBSET_1, NAT_1, SCMFSA_4,
      TEX_2, YELLOW13, XBOOLE_0, MEMBERED, PRE_CIRC, SETFAM_1, STRUCT_0,
      CARD_4, XXREAL_0, CARD_3, REALSET1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions TARSKI, RELAT_1, FUNCT_1, WELLORD2, FRAENKEL, REAL_1, FUNCT_7,
      AMI_1, AMI_3, PRALG_2, YELLOW_8, AMISTD_1, XBOOLE_0, CQC_LANG;
 theorems AMI_1, AMI_3, AMI_5, BINARITH, CARD_1, CARD_2, AMISTD_1, CQC_LANG,
      FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, FUNCT_4, FUNCOP_1,
      GRFUNC_1, INT_1, KNASTER, MCART_1, SCMFSA6A, CATALG_1, NAT_1, PRE_CIRC,
      REAL_1, REALSET1, RELAT_1, SETFAM_1, TARSKI, YELLOW_8, ZFMISC_1, CARD_3,
      PRALG_2, ORDINAL1, XBOOLE_0, XBOOLE_1, FINSET_1, XREAL_1, XXREAL_0;
 schemes FUNCT_7, FINSEQ_1, ZFREFLE1, XBOOLE_0;

begin  :: Preliminaries

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

Lm1:
 for R being Relation st dom R <> {} holds R <> {} by RELAT_1:60;

 Lm2:
 for f, g being Function holds
  dom f,dom g are_equipotent iff f,g are_equipotent by PRE_CIRC:26;

 Lm3:
 for f, g being finite Function st dom f misses dom g
  holds card (f +* g) = card f + card g by PRE_CIRC:27;

registration
   let f be Function,
       A be set;
 cluster f \ A -> Function-like Relation-like;
coherence by GRFUNC_1:38;
end;

canceled 2;

theorem Th3:
 for f, g being Function st x in dom f \ dom g holds (f \ g).x = f.x
  proof
    let f, g be Function such that
A1:   x in dom f \ dom g;
A2: dom f \ dom g c= dom (f \ g) by RELAT_1:15;
    thus (f \ g).x = f.x by A1,A2,GRFUNC_1:8;
  end;

 Lm4:
 for F being non empty finite set holds card F - 1 = card F -' 1
    by PRE_CIRC:25;

begin  :: Product like sets

definition
  let S be functional set;
  func PA S -> Function means :Def1:
  (for x being set holds x in dom it iff
       for f being Function st f in S holds x in dom f) &
  (for i being set st i in dom it holds it.i = pi(S,i)) if S is non empty
  otherwise it = {};
existence
  proof
    thus S is non empty implies ex g being Function st
     (for x being set holds x in dom g iff
          for f being Function st f in S holds x in dom f) &
     (for i being set st i in dom g holds g.i = pi(S,i))
    proof
      assume S is non empty;
      then reconsider S1 = S as non empty functional set;
      set D = {dom f where f is Element of S1: not contradiction};
      defpred P[set,set] means $2 = pi(S,$1);
A1:   for e being set st e in meet D ex u being set st P[e,u];
      consider g being Function such that
A2:     dom g = meet D and
A3:     for e being set st e in meet D holds P[e,g.e] from ZFREFLE1:sch 1(A1);
      take g;
      hereby
        let x be set;
        hereby
          assume
A4:         x in dom g;
          let f be Function;
          assume f in S;
          then dom f in D;
          hence x in dom f by A2,A4,SETFAM_1:def 1;
        end;
        assume
A5:       for f being Function st f in S holds x in dom f;
        consider f being Element of S1;
A6:     dom f in D;
            for Y being set holds Y in D implies x in Y
        proof
          let Y be set;
          assume Y in D;
          then ex f being Element of S1 st Y = dom f & not contradiction;
          hence x in Y by A5;
        end;
        hence x in dom g by A2,A6,SETFAM_1:def 1;
      end;
      thus thesis by A2,A3;
    end;
    thus thesis;
  end;
uniqueness
  proof
    let A, B be Function;
    thus S is non empty &
     (for x being set holds x in dom A iff
       for f being Function st f in S holds x in dom f) &
     (for i being set st i in dom A holds A.i = pi(S,i)) &
     (for x being set holds x in dom B iff
       for f being Function st f in S holds x in dom f) &
     (for i being set st i in dom B holds B.i = pi(S,i))
     implies A = B
    proof
      defpred P[set] means for f being Function st f in S holds $1 in dom f;
      assume that
         S is non empty and
A7:  for x being set holds x in dom A iff P[x] and
A8:  for i being set st i in dom A holds A.i = pi(S,i) and
A9:  for x being set holds x in dom B iff P[x] and
A10:  for i being set st i in dom B holds B.i = pi(S,i);
A11:   dom A = dom B from XBOOLE_0:sch 2(A7,A9);
          now
        let i be set;
        assume
A12:       i in dom A;
        hence A.i = pi(S,i) by A8
                 .= B.i by A10,A11,A12;
      end;
      hence A = B by A11,FUNCT_1:9;
    end;
    thus thesis;
  end;
consistency;
end;

canceled;

theorem
  for S being non empty functional set holds
  dom PA S = meet {dom f where f is Element of S: not contradiction}
  proof
    let S be non empty functional set;
    set D = {dom f where f is Element of S: not contradiction};
    hereby
      let x be set;
      assume
A1:     x in dom PA S;
      consider f being Element of S;
A2:   dom f in D;
      for Y being set holds Y in D implies x in Y
      proof
        let Y be set;
        assume Y in D;
        then ex f being Element of S st Y = dom f & not contradiction;
        hence x in Y by A1,Def1;
      end;
      hence x in meet D by A2,SETFAM_1:def 1;
    end;
    let x be set;
    assume
A3:   x in meet D;
        for f being Function st f in S holds x in dom f
    proof
      let f be Function;
      assume f in S;
      then dom f in D;
      hence x in dom f by A3,SETFAM_1:def 1;
    end;
    hence thesis by Def1;
  end;

theorem
     for S being non empty functional set,
     i being set st i in dom PA S holds
  (PA S).i = {f.i where f is Element of S: not contradiction}
  proof
    let S be non empty functional set,
        i be set;
    assume
A1:   i in dom PA S;
    hereby
      let x be set;
      assume x in (PA S).i;
      then x in pi(S,i) by A1,Def1;
      then ex f being Function st f in S & x = f.i by CARD_3:def 6;
      hence x in {f.i where f is Element of S: not contradiction};
    end;
    let x be set;
    assume x in {f.i where f is Element of S: not contradiction};
    then ex f being Element of S st x = f.i & not contradiction;
    then x in pi(S,i) by CARD_3:def 6;
    hence thesis by A1,Def1;
  end;

definition
  let S be set;
 attr S is product-like means :Def2:
  ex f being Function st S = product f;
end;

registration
  let f be Function;
 cluster product f -> product-like;
coherence by Def2;
end;

registration
 cluster product-like -> functional with_common_domain set;
coherence
  proof
    let S be set;
    given f being Function such that
A1:   S = product f;
    thus S is functional by A1;
    let h, g be Function such that
A2:   h in S and
A3:   g in S;
    thus dom h = dom f by A1,A2,CARD_3:18
      .= dom g by A1,A3,CARD_3:18;
  end;
end;

registration
 cluster product-like non empty set;
existence
  proof
    consider B being with_non-empty_elements set,
             f being Function of 0,B;
    take product f;
    thus thesis;
  end;
end;

theorem Th7:
 for S being functional with_common_domain set holds dom PA S = DOM S
  proof
    let S be functional with_common_domain set;
    per cases;
    suppose
A1:   S is empty;
    hence dom PA S = {} by Def1,RELAT_1:60
     .= DOM S by A1,PRALG_2:def 2;
    end;
    suppose
A2:   S is non empty;
    consider f being Element of S;
    hereby
      let x be set;
      assume x in dom PA S;
      then x in dom f by A2,Def1;
      hence x in DOM S by A2,PRALG_2:def 2;
    end;
    let x be set;
    assume
      x in DOM S;
    then for f being Function st f in S holds x in dom f by PRALG_2:def 2;
    hence thesis by A2,Def1;
  end;
  end;

theorem
     for S being functional set, i being set st i in dom PA S
  holds (PA S).i = pi(S,i)
  proof
    let S be functional set,
        i be set;
    per cases;
    suppose S = {};
    then dom PA S = dom {} by Def1;
    hence thesis;
    end;
    suppose
A1:   S <> {};
    assume i in dom PA S;
    hence thesis by A1,Def1;
  end;
  end;

theorem Th9:
 for S being functional with_common_domain set holds S c= product PA S
  proof
    let S be functional with_common_domain set;
    let f be set;
    assume
A1:   f in S;
    then reconsider f as Element of S;
A2: dom f = DOM S by A1,PRALG_2:def 2
         .= dom PA S by Th7;
        for i being set st i in dom PA S holds f.i in (PA S).i
    proof
      let i be set;
      assume i in dom PA S;
      then (PA S).i = pi(S,i) by A1,Def1;
      hence f.i in (PA S).i by A1,CARD_3:def 6;
    end;
    hence thesis by A2,CARD_3:18;
  end;

theorem Th10:
 for S being non empty product-like set holds S = product PA S
  proof
    let S be non empty product-like set;
    thus S c= product PA S by Th9;
    let x be set;
    assume x in product PA S;
    then consider g being Function such that
A1:   x = g and
A2:   dom g = dom PA S and
A3:   for z being set st z in dom PA S holds g.z in (PA S).z by CARD_3:def 5;
    consider p being Function such that
A4:   S = product p by Def2;
    consider s being Element of S;
A5: dom g = DOM S by A2,Th7
         .= dom s by PRALG_2:def 2
         .= dom p by A4,CARD_3:18;
        for z being set st z in dom p holds g.z in p.z
    proof
      let z be set;
      assume
A6:     z in dom p;
      then g.z in (PA S).z by A2,A3,A5;
      then g.z in pi(S,z) by A2,A5,A6,Def1;
      then ex f being Function st f in S & g.z = f.z by CARD_3:def 6;
      hence g.z in p.z by A4,A6,CARD_3:18;
    end;
    hence x in S by A1,A4,A5,CARD_3:18;
  end;

registration
  let D be set;
 cluster -> functional FinSequenceSet of D;
coherence
  proof
    let f be FinSequenceSet of D;
    let x be set;
    thus x in f implies x is Function by FINSEQ_2:def 3;
  end;
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 CQC_LANG:5;
    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 PA S;
        S = product PA S
    proof
      thus S c= product PA S by Th9;
      let x be set;
      assume x in product PA S;
      then consider g being Function such that
A2:     x = g and
A3:     dom g = dom PA S and
A4:     for z being set st z in dom PA S holds g.z in (PA 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,Th7
           .= dom s by PRALG_2:def 2;
          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 (PA S).a by A3,A4,A10;
        then g.a in pi(S,a) by A3,A10,Def1;
        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,PRALG_2:def 1;
        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;

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

Lm6:
 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

theorem Th11:
 for N be set,
     S being AMI-Struct over N,
     F being FinPartState of S holds F \ X is FinPartState of S
  proof
    let N be set,
        S be AMI-Struct over N,
        F be FinPartState of S;
    F \ X in sproduct the Object-Kind of S by AMI_1:40;
    hence F \ X is FinPartState of S by AMI_1:def 24;
  end;

theorem Th12:
 for S being IC-Ins-separated definite (non empty non void AMI-Struct over 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 non void AMI-Struct over N),
        F be programmed FinPartState of S;
    reconsider G = F \ X as FinPartState of S by Th11;
    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= the Instruction-Locations of S by AMI_3:def 13;
      hence dom G c= the Instruction-Locations of S by A1,XBOOLE_1:1;
    end;
    hence thesis;
  end;
  end;

definition
   let N be with_non-empty_elements set,
       S be IC-Ins-separated definite (non empty non void AMI-Struct over 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 N be with_non-empty_elements set;
   let S be halting (non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over N)),
        F be lower programmed FinPartState of S;
A1: dom F c= the Instruction-Locations of S by AMI_3:def 13;
    hereby
      let x be set;
      assume
A2:     x in dom F;
      then reconsider f = x as Instruction-Location of S by A1;
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 N be set;
   let S be AMI-Struct over N;
   let I be Element of the Instructions of S;
 func AddressPart I equals
  I`2;
coherence;
end;

definition
   let N be set;
   let S be AMI-Struct over N;
   let I be Element of the Instructions of S;
 redefine func AddressPart I -> FinSequence of (union N) \/ the carrier of S;
coherence by FINSEQ_1:def 11;
end;

theorem Th16:
 for N being set,
     S being AMI-Struct over 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 AMI-Struct over N,
        I, J be Element of the Instructions of S;
    assume
A1:   InsCode I = InsCode J & AddressPart I = AddressPart J;
        (ex x, y being set st x in the Instruction-Codes of S &
      y in ((union N) \/ the carrier of S)* & I = [x,y]) &
    (ex x, y being set st x in the Instruction-Codes of S &
      y in ((union N) \/
 the carrier of S)* & J = [x,y]) by ZFMISC_1:def 2;
then A2: I = [I`1,I`2] & J = [J`1,J`2] by MCART_1:8;
        InsCode I = I`1 & InsCode J = J`1 &
      AddressPart I = I`2 & AddressPart J = J`2 by AMI_5:def 1;
    hence thesis by A1,A2;
  end;

definition
   let N be set;
   let S be AMI-Struct over 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 A1: I = [0,0] or I = [1,0] by TARSKI:def 2;
    thus AddressPart I = 0 by A1,MCART_1:def 2;
  end;

definition
   let N be set;
   let S be AMI-Struct over 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 N be set;
   let S be AMI-Struct over 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 N be with_non-empty_elements set,
       S be IC-Ins-separated definite (non empty non void AMI-Struct over 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 &
     (PA AddressParts InsCode I).k = the Instruction-Locations of S;

 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 &
     (PA AddressParts InsCode I).k = the Instruction-Locations of S
    holds f in JUMP I;
end;

definition
   let N be with_non-empty_elements set,
       S be IC-Ins-separated definite (non empty non void AMI-Struct over 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;

definition
   let N be set,
       S be AMI-Struct over N;
 attr S is with-non-trivial-Instruction-Locations means :Def10:
  the Instruction-Locations of S is non trivial;
end;

registration
   let N be with_non-empty_elements set;
 cluster standard -> with-non-trivial-Instruction-Locations
        (IC-Ins-separated definite (non empty non void AMI-Struct over N));
coherence
  proof
    let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
    given f being Function of NAT, the Instruction-Locations of S such that
A1:   f is bijective and
          for m, n being Element of NAT holds m <= n iff f.m <= f.n;
A2: NAT,the Instruction-Locations of S are_equipotent by A1,KNASTER:13;
    thus the Instruction-Locations of S is non trivial
    proof
      assume not thesis;
      then reconsider a = the Instruction-Locations of S as trivial set;
          a is finite;
      hence thesis by A2,CARD_1:68;
    end;
  end;
end;

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

registration
   let N be with_non-empty_elements set,
       S be with-non-trivial-Instruction-Locations AMI-Struct over N;
 cluster the Instruction-Locations of S -> non trivial;
coherence by Def10;
end;

theorem Th18:
 for S being standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over N)),
        I be Instruction of S;
    assume
A1:   for f being Instruction-Location of S holds NIC(I,f)={NextLoc f};
    consider p, q being Element of the Instruction-Locations of S such that
A2:   p <> q by YELLOW_8:def 1;
    set X = { NIC(I,f) where f is Instruction-Location of S:
        not contradiction };
    assume not thesis;
    then meet X is non empty;
    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 A2,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 I is halting by AMISTD_1:20;
    then for f being Instruction-Location of STC N holds NIC(I,f)={f}
      by AMISTD_1:15;
    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 N be set;
   let S be AMI-Struct over N;
 attr S is regular means :Def11:
  for T being InsType of S holds AddressParts T is product-like;
end;

registration let N be set;
 cluster regular -> homogeneous AMI-Struct over N;
coherence
  proof
    let S be AMI-Struct over 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 Def2;
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;
A3:     the Instruction-Codes of STC N = {0,1} by AMISTD_1:def 11;
        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 = I`1 by AMI_5:def 1
                 .= 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 = I`1 by AMI_5:def 1
                 .= 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;

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 A1:   I = [0,0] or I = [1,0] by TARSKI:def 2;
          AddressPart I = 0 by A1,MCART_1:def 2;
      hence thesis by FINSEQ_1:26;
    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 (non empty non void AMI-Struct over N));
existence
  proof
    take STC N;
    thus thesis;
  end;
end;

registration
   let N be with_non-empty_elements set;
   let S be regular AMI-Struct over N;
   let T be InsType of S;
 cluster AddressParts T -> product-like;
coherence by Def11;
end;

registration
   let N be with_non-empty_elements set;
   let S be homogeneous AMI-Struct over 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;

theorem Th20:
 for S being homogeneous non empty non void AMI-Struct over N,
     I being Instruction of S,
     x being set st x in dom AddressPart I holds
  (PA AddressParts InsCode I).x = the Instruction-Locations of S implies
   (AddressPart I).x is Instruction-Location of S
  proof
    let S be homogeneous non empty non void AMI-Struct over 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:   (PA AddressParts InsCode I).x = the Instruction-Locations of S;
        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 PA AddressParts InsCode I by A2,Def1;
    then (PA AddressParts InsCode I).x = pi(AddressParts InsCode I,x)
      by A2,Def1;
    hence (AddressPart I).x is Instruction-Location of S by A2,A3,CARD_3:def 6
;
  end;

registration
   let N be with_non-empty_elements set;
   let S be with_explicit_jumps (IC-Ins-separated
       definite (non empty non void AMI-Struct over N));
 cluster -> with_explicit_jumps Instruction of S;
coherence by Def8;
end;

registration
   let N be with_non-empty_elements set;
   let S be without_implicit_jumps
 (IC-Ins-separated definite (non empty non void AMI-Struct over N));
 cluster -> without_implicit_jumps Instruction of S;
coherence by Def9;
end;

theorem Th21:
 for S being with-non-trivial-Instruction-Locations
       realistic IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     I being Instruction of S st I is halting
  holds JUMP I is empty
  proof
    let S be with-non-trivial-Instruction-Locations
          realistic IC-Ins-separated definite
          (non empty non void AMI-Struct over 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 N be with_non-empty_elements set,
      S be with-non-trivial-Instruction-Locations halting realistic
           (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
      I be halting Instruction of S;
 cluster JUMP I -> empty;
coherence by Th21;
end;

registration
   let N be with_non-empty_elements set,
       S be with-non-trivial-Instruction-Locations IC-Ins-separated definite
            (non empty non void AMI-Struct over N);
 cluster non trivial programmed FinPartState of S;
existence
  proof
    consider l1, l2 being Element of the Instruction-Locations of S such that
A1:   l1 <> l2 by YELLOW_8:def 1;
    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 non void AMI-Struct over 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 N be set;
   let S be AMI-Struct over 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 (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
end;

theorem
     for S being halting with_explicit_jumps
             with-non-trivial-Instruction-Locations
             realistic (IC-Ins-separated definite
             (non empty non void AMI-Struct over N)),
     I being Instruction of S st I is ins-loc-free
  holds JUMP I is empty
  proof
    let S be halting with_explicit_jumps
             with-non-trivial-Instruction-Locations
             realistic (IC-Ins-separated definite
             (non empty non void AMI-Struct over N)),
        I be Instruction of S such that
A1:  for x being set st x in dom AddressPart I
      holds (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
    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 &
       (PA AddressParts InsCode I).k = the Instruction-Locations of S
        by A2,Def6;
    hence thesis by A1;
  end;

theorem Th23:
 for S being without_implicit_jumps with-non-trivial-Instruction-Locations
       realistic (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     I being Instruction of S st I is halting
  holds I is ins-loc-free
  proof
    let S be without_implicit_jumps with-non-trivial-Instruction-Locations
          realistic (IC-Ins-separated definite
          (non empty non void AMI-Struct over 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 (PA AddressParts InsCode I).x = the Instruction-Locations of S;
    then (AddressPart I).x in JUMP I by A2,Def7;
    hence contradiction by A1,Th21;
  end;

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

theorem Th24:
 for S being standard without_implicit_jumps
             (IC-Ins-separated definite
             (non empty non void AMI-Struct over N)),
     I being Instruction of S st I is sequential
  holds I is ins-loc-free
  proof
    let S be standard without_implicit_jumps
             (IC-Ins-separated definite
             (non empty non void AMI-Struct over 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 &
      (PA AddressParts InsCode I).k = the Instruction-Locations of S
        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
            (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 non void AMI-Struct over N));
 func Stop S -> FinPartState of S equals
  il.(S,0) .--> halt S;
coherence;
end;

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

Lm8:
    for N be with_non-empty_elements set,
        S be standard halting (IC-Ins-separated definite
        (non empty non void AMI-Struct over N))
    holds (Stop S).il.(S,0) = halt S by CQC_LANG:6;

registration
   let N be with_non-empty_elements set,
       S be standard halting
          (IC-Ins-separated definite (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over N));
 cluster Stop S -> autonomic;
coherence by AMISTD_1:12;
end;

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

theorem Th26:
 for S being standard halting (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 Lm4
               .= 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 CQC_LANG:45;
    hence F = Stop S;
  end;

Lm9:
 for S being standard halting (IC-Ins-separated definite
     (non empty non void AMI-Struct over N))
  holds card Stop S -' 1 = 0
  proof
    let S be standard halting (IC-Ins-separated definite
        (non empty non void AMI-Struct over N));
    thus card Stop S -' 1 = card Stop S - 1 by Lm4
                         .= 1 - 1 by Th25
                         .= 0;
  end;

theorem Th27:
 for S being standard halting (IC-Ins-separated definite
     (non empty non void AMI-Struct over N))
  holds LastLoc Stop S = il.(S,0)
  proof
    let S be standard halting (IC-Ins-separated definite
        (non empty non void AMI-Struct over N));
        card Stop S -' 1 = 0 by Lm9;
    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 non void AMI-Struct over 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 CQC_LANG:6;
    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 Lm7;
    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 non void AMI-Struct over 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 (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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
    ((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
      ex f being Instruction-Location of S st
         f = (AddressPart I).n & (AddressPart it).n = il.(S,k + locnum f)) &
    ((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
     (AddressPart it).n = (AddressPart I).n);
existence
  proof
    set D = (union N) \/ the carrier of S;
defpred P[set,set] means
    ((PA AddressParts InsCode I).$1 = the Instruction-Locations of S implies
      ex il being Instruction-Location of S st
         il = (AddressPart I).$1 & $2 = il.(S,k + locnum il)) &
    ((PA AddressParts InsCode I).$1 <> the Instruction-Locations of S implies
      $2 = (AddressPart I).$1);
A1: for m being Element of NAT st m in Seg len AddressPart I
      ex x being Element of D st P[m,x]
    proof
      let m be Element of 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:     (PA AddressParts InsCode I).m = the Instruction-Locations of S;
      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:     (PA AddressParts InsCode I).m <> the Instruction-Locations of S;
          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 Element of NAT st k in Seg len AddressPart I holds P[k,p.k]
        from FINSEQ_1:sch 5(A1);
    set f = PA AddressParts InsCode I;
A8: AddressPart I in AddressParts InsCode I;
then A9: AddressParts InsCode I = product f by Th10;
A10: dom p = dom AddressPart I by A6,FINSEQ_1:def 3
         .= DOM AddressParts InsCode I by A8,PRALG_2:def 2
         .= dom f by Th7;
        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,Def1;
      reconsider z as Element of NAT by A11;
      per cases;
      suppose
A13:     f.z = the Instruction-Locations of S;
      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;
      end;
      suppose f.z <> the Instruction-Locations of S;
      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 n in dom AddressPart I;
    then n in Seg len AddressPart I by FINSEQ_1:def 3;
    hence thesis by A7,A14;
  end;
uniqueness
  proof
    let a, b be Instruction of S such that
A16:   InsCode a = InsCode I and
A17:   dom AddressPart a = dom AddressPart I and
A18:   for n being set st n in dom AddressPart I holds
      ((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
        ex f being Instruction-Location of S st
           f = (AddressPart I).n & (AddressPart a).n = il.(S,k + locnum f)) &
      ((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
       (AddressPart a).n = (AddressPart I).n) and
A19:   InsCode b = InsCode I and
A20:   dom AddressPart b = dom AddressPart I and
A21:   for n being set st n in dom AddressPart I holds
      ((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
        ex f being Instruction-Location of S st
           f = (AddressPart I).n & (AddressPart b).n = il.(S,k + locnum f)) &
      ((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
       (AddressPart b).n = (AddressPart I).n);
A22: Seg len AddressPart a = dom AddressPart a by FINSEQ_1:def 3;
        for n being Element of NAT st n in Seg len AddressPart a holds
     (AddressPart a).n = (AddressPart b).n
    proof
      let n be Element of NAT;
      assume n in Seg len AddressPart a;
      then ((PA AddressParts InsCode I).n = the Instruction-Locations of S
implies
        ex f being Instruction-Location of S st
           f = (AddressPart I).n & (AddressPart a).n = il.(S,k + locnum f)) &
      ((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
       (AddressPart a).n = (AddressPart I).n) &
      ((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
        ex f being Instruction-Location of S st
           f = (AddressPart I).n & (AddressPart b).n = il.(S,k + locnum f)) &
      ((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
       (AddressPart b).n = (AddressPart I).n)
        by A17,A18,A21,A22;
      hence (AddressPart a).n = (AddressPart b).n;
    end;
    then AddressPart a = AddressPart b by A17,A20,A22,FINSEQ_1:17;
    hence thesis by A16,A19,Th16;
  end;
end;

theorem Th28:
 for S being regular standard
       (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
     I being Element of the Instructions of S
  holds IncAddr(I, 0) = I
  proof
    let S be regular standard
       (IC-Ins-separated definite (non empty non void AMI-Struct over 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 Element of NAT st k in dom AddressPart I holds
     (AddressPart IncAddr(I, 0)).k = (AddressPart I).k
    proof
      let k be Element of NAT;
      assume
A3:     k in dom AddressPart I;
      per cases;
      suppose (PA AddressParts InsCode I).k = the Instruction-Locations of S;
      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 (PA AddressParts InsCode I).k <> the Instruction-Locations of S;
      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
       (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
     I being Instruction of S st I is ins-loc-free
  holds IncAddr(I, k) = I
  proof
    let S be regular standard
        (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
        I be Instruction of S such that
A1:  for x being set st x in dom AddressPart I
      holds (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
    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;
          (PA AddressParts InsCode I).x = the Instruction-Locations of S or
      (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
      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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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
            (IC-Ins-separated definite (non empty non void AMI-Struct over 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
     (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
     I being Instruction of S
  holds AddressParts InsCode I = AddressParts InsCode IncAddr(I,k)
  proof
    let S be regular standard
        (IC-Ins-separated definite (non empty non void AMI-Struct over 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 };
A1: A = B
    proof
      hereby
        let a be set;
        assume a in A;
        then consider J being Instruction of S such that
A2:       a = AddressPart J and
A3:       InsCode J = InsCode I;
            InsCode J = InsCode IncAddr(I,k) by A3,Def14;
        hence a in B by A2;
      end;
      let a be set;
      assume a in B;
      then consider J being Instruction of S such that
A4:       a = AddressPart J and
A5:       InsCode J = InsCode IncAddr(I,k);
          InsCode J = InsCode I by A5,Def14;
      hence a in A by A4;
    end;
    thus AddressParts InsCode I = AddressParts InsCode IncAddr(I,k) by A1;
  end;

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

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

theorem Th34:
 for S being regular standard
    (IC-Ins-separated definite (non empty non void AMI-Struct over 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
        (IC-Ins-separated definite (non empty non void AMI-Struct over 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:    (PA AddressParts InsCode I).x = the Instruction-Locations of S;
     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;
         (PA AddressParts InsCode J).x = the Instruction-Locations of S
       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;
     then locnum f = locnum g;
     hence (AddressPart I).x = (AddressPart J).x by A6,A8,AMISTD_1:27;
     end;
     suppose
A10:    (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
then A11:  (PA AddressParts InsCode J).x <> the Instruction-Locations of S
       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 (IC-Ins-separated definite
             (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
             (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
             (non empty non void AMI-Struct over N)),
     I being Instruction of S st I is sequential
  holds IncAddr(I,k) is sequential
  proof
    let S be regular standard halting without_implicit_jumps
             realistic (IC-Ins-separated definite
             (non empty non void AMI-Struct over N)),
        I be Instruction of S;
    assume
A1:   I is sequential;
    then I is ins-loc-free by Th24;
    hence thesis by A1,Th29;
  end;

theorem Th37:
 for S being regular standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     I being Instruction of S
  holds IncAddr(IncAddr(I,k),m) = IncAddr(I,k+m)
  proof
    let S be regular standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over 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:     (PA AddressParts InsCode I).n = the Instruction-Locations of S;
      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;
          (PA AddressParts InsCode IncAddr(I,k)).n =
        the Instruction-Locations of S 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:     (PA AddressParts InsCode I).n <> the Instruction-Locations of S;
then (PA AddressParts InsCode IncAddr(I,k)).n <>
         the Instruction-Locations of S 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 (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      p be programmed FinPartState of S,
      k be natural number;
A1: dom p c= the Instruction-Locations of S by AMI_3:def 13;
 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 consider m being natural number such that
A3:     e = il.(S,m) by A1,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 ZFREFLE1:sch 1(A2);
        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;
          (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 Element of sproduct the Object-Kind of S by A6,
AMI_1:def 16;
        f is finite by A4,FINSET_1:29;
    then reconsider f as FinPartState of S by AMI_1:def 24;
    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 consider m being natural number such that
A14:    x = il.(S,m) by A1,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 (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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= the Instruction-Locations of S by AMI_3:def 13;
  end;
end;

registration
   let N be with_non-empty_elements set,
       S be regular standard (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 Lm1;
  end;
end;

registration
   let N be with_non-empty_elements set,
       S be regular standard (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     F being programmed FinPartState of S
  holds IncAddr(F,0) = F
  proof
    let S be regular standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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_5:def 5;
      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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     F being lower programmed FinPartState of S
  holds IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m)
  proof
    let S be regular standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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= the Instruction-Locations of S by AMI_3:def 13;
      then reconsider x as Instruction-Location of S by A3;
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_5:def 5;
          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 non void AMI-Struct over 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 ZFREFLE1:sch 1(A1);
A5:  A c= the Instruction-Locations of S
     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 the Instruction-Locations of S;
    end;
    then A c= the carrier of S by XBOOLE_1:1;
then A6: 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
A7:     x in dom f;
      then consider m being Element of NAT such that
A8:      x = il.(S,m+k) and
A9:      f.x = p.il.(S,m) by A3,A4;
      reconsider y = x as Instruction-Location of S by A3,A5,A7;
A10:  (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
A11:    p c= s by AMI_3:39;
      consider j being Element of NAT such that
A12:    il.(S,m+k) = il.(S,j+k) and
A13:    il.(S,j) in dom p by A3,A7,A8;
          j+k = m+k by A12,AMISTD_1:25;
then A14:  il.(S,m) in dom p by A13;
          s.il.(S,m) in the Instructions of S;
      hence f.x in (the Object-Kind of S).x by A9,A10,A11,A14,GRFUNC_1:8;
    end;
    then reconsider f as Element of sproduct the Object-Kind of S
                   by A6,AMI_1:def 16
;
A15:dom p is finite;
A16: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(A15,A16);
    then f is finite by A3,FINSET_1:29;
    then reconsider f as FinPartState of S by AMI_1:def 24;
    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
A17:  il.(S,m+k) = il.(S,j+k) and
A18:  f.il.(S,m+k) = p.il.(S,j) by A4;
        m+k = j+k by A17,AMISTD_1:25;
    hence f.il.(S,m+k) = p.il.(S,m) by A18;
  end;
uniqueness
  proof
    let IT1, IT2 be FinPartState of S such that
A19:  dom IT1 = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p } and
A20:  for m being Element of NAT st il.(S,m) in dom p
holds IT1.il.(S,m+k) = p.il.(S,m)
    and
A21:  dom IT2 = { il.(S,m+k) where m is Element of NAT: il.(S,m) in dom p } and
A22:  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
A23:    x = il.(S,m+k) and
A24:    il.(S,m) in dom p;
      thus IT1.x = p.il.(S,m) by A20,A23,A24
                .= IT2.x by A22,A23,A24;
    end;
    hence IT1=IT2 by A19,A21,FUNCT_1:9;
  end;
end;

registration
   let N be with_non-empty_elements set,
       S be standard (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 the Instruction-Locations of S;
  end;
end;

registration
   let N be with_non-empty_elements set,
       S be standard (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 non void AMI-Struct over 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= the Instruction-Locations of S by AMI_3:def 13;
    then reconsider a as Instruction-Location of S by A2;
    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 Lm1;
  end;
end;

theorem Th40:
 for S being standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     F being programmed FinPartState of S
  holds Shift(F,0) = F
  proof
    let S be standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
        F be programmed FinPartState of S;
A1: dom F c= the Instruction-Locations of S by AMI_3:def 13;
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 consider k being natural number such that
A4:       a = il.(S,k) by A1,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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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;
A9:   q+m is Element of NAT by ORDINAL1:def 13;
          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,A9;
    end;
then A10: 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
A11:    il.(S,l) in dom F;
then A12:  il.(S,l+m) in dom Shift(F,m) by A1;
A13:   l+m is Element of NAT by ORDINAL1:def 13;
      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 A12,A13,Def16
              .= F.il.(S,l) by A11,Def16;
    end;
    hence Shift(Shift(F,m),k) = Shift(F,m+k) by A10,Def16;
  end;

theorem Th43:
 for S being standard (IC-Ins-separated definite
     (non empty non void AMI-Struct over 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 non void AMI-Struct over N)),
        F be programmed FinPartState of S;
A1: dom F c= the Instruction-Locations of S by AMI_3:def 13;
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;
      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 ZFREFLE1: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;
      then locnum i1 = locnum i2;
      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 (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
            (non empty non void AMI-Struct over N));
 attr S is IC-good means :Def18:
  for I being Instruction of S holds I is IC-good;
end;

definition
   let N be with_non-empty_elements set,
       S be non void AMI-Struct over 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 the Instruction-Locations of S
   holds Exec(I,s1), Exec(I,s2)
         equal_outside the Instruction-Locations of S;
end;

definition
   let N be with_non-empty_elements set,
       S be non void AMI-Struct over 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
      (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
     I being Instruction of S st I is sequential
   holds I is IC-good
  proof
    let S be regular standard without_implicit_jumps
        (IC-Ins-separated definite (non empty non void AMI-Struct over 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));
A3: I is ins-loc-free by A1,Th24;
        dom (IC S .--> (IC s1 + k)) = {IC S} by CQC_LANG:5;
then A4: IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
A5: IC s2 = (IC S .--> (IC s1 + k)).IC S by A2,A4,FUNCT_4:14
         .= il.(S,locnum IC s1 + k) by CQC_LANG:6;
A6: IC Exec(I, s2) = NextLoc IC s2 by A1,AMISTD_1:def 16
      .= il.(S,locnum IC s1 + k + 1) by  A5,AMISTD_1:def 13
      .= il.(S,locnum IC s1 + 1 + k);
A7: IC Exec(I,s1) = NextLoc IC s1 by A1,AMISTD_1:def 16
      .= il.(S,locnum IC s1 + 1);
    thus IC Exec(I,s1) + k = IC Exec(I,s2) by A6,A7,AMISTD_1:def 13
      .= IC Exec(IncAddr(I,k), s2) by A3,Th29;
  end;

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

theorem Th45:
 for S being regular standard without_implicit_jumps realistic
      (IC-Ins-separated definite (non empty non void AMI-Struct over 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
          (IC-Ins-separated definite (non empty non void AMI-Struct over 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));
A3: I is ins-loc-free by A1,Th23;
        dom (IC S .--> (IC s1 + k)) = {IC S} by CQC_LANG:5;
then A4: 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 CQC_LANG:6
      .= IC s2 by A2,A4,FUNCT_4:14
      .= IC Exec(I,s2) by A1,AMI_1:def 8
      .= IC Exec(IncAddr(I,k), s2) by A3,Th29;
  end;

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

theorem Th46:
 for S being non void AMI-Struct over N,
     I being Instruction of S st I is halting
  holds I is Exec-preserving
  proof
    let S be non void AMI-Struct over 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 the Instruction-Locations of S;
        Exec(I,s1) = s1 & Exec(I,s2) = s2 by A1;
    hence thesis by A2;
  end;

registration
   let N be with_non-empty_elements set,
       S be non void AMI-Struct over 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 CQC_LANG:5;
then A2:   IC STC N in dom (IC STC N .--> (IC s1 + k)) by TARSKI:def 1;
A3:   IC s2 = (IC STC N .--> (IC s1 + k)).IC STC N by A1,A2,FUNCT_4:14
           .= IC s1 + k by CQC_LANG:6;
      per cases by AMISTD_1:22;
      suppose
A4:     InsCode I = 1;
then A5:   InsCode IncAddr(I,k) = 1 by Def14;
      Exec(I,s1).IC STC N = NextLoc IC s1 by A4,AMISTD_1:38
        .= il.(STC N,locnum IC s1 + 1);
then A6:   locnum IC Exec(I,s1) = locnum IC s1 + 1 by AMISTD_1:def 13;
      thus IC Exec(I,s1) + k = locnum IC s1 + k + 1 by A6,AMISTD_1:37
        .= locnum (IC s1 + k) + 1 by AMISTD_1:33
        .= NextLoc IC s2 by A3,AMISTD_1:37
        .= IC Exec(IncAddr(I,k), s2) by A5,AMISTD_1:38;
      end;
      suppose InsCode I = 0;
then A7:   I is halting by AMISTD_1:20;
      then I is ins-loc-free by Th23;
then A8:   IncAddr(I,k) is halting by A7,Th29;
      thus IC Exec(I,s1) + k = IC s1 + k by A7,AMI_1:def 8
        .= IC Exec(IncAddr(I,k), s2) by A3,A8,AMI_1:def 8;
    end;
    end;
    let I be Instruction of STC N;
    per cases by AMISTD_1:22;
    suppose InsCode I = 1;
then A9: I`1 = 1 by AMI_5:def 1;
        the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
then A10: I = [0,0] or I = [1,0] by TARSKI:def 2;
    let s1, s2 be State of STC N such that
A11:   s1, s2 equal_outside the Instruction-Locations of STC N;
    consider f being Function of product the Object-Kind of STC N,
                                 product the Object-Kind of STC N such that
A12:   for s being Element of product the Object-Kind of STC N
       holds f.s = s+*(NAT .-->succ(s.NAT)) and
A13:   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 A9,A10,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 A14: (the Execution of STC N).I = ([1,0] .--> f).I by A13,FUNCT_4:12;
A15: I in {[1,0]} by A9,A10,MCART_1:7,TARSKI:def 1;
A16: Exec(I,s1) = f.s1 by A14,A15,FUNCOP_1:13
      .= s1+*(NAT .-->succ(s1.NAT)) by A12;
A17: Exec(I,s2) = f.s2 by A14,A15,FUNCOP_1:13
      .= s2+*(NAT .-->succ(s2.NAT)) by A12;
        dom Exec(I,s1) = dom the Object-Kind of STC N by CARD_3:18;
then A18: dom Exec(I,s1) = dom Exec(I,s2) by CARD_3:18;
        for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of
     STC N holds Exec(I,s1).x = Exec(I,s2).x
    proof
      let x be set;
      assume
A19:     x in dom Exec(I,s1) \ the Instruction-Locations of STC N;
      then not x in the Instruction-Locations of STC N by XBOOLE_0:def 4;
then A20:   not x in NAT by AMISTD_1:def 11;
A21:   s1.NAT = IC s1 by AMISTD_1:def 11
            .= IC s2 by A11,SCMFSA6A:29
            .= s2.NAT by AMISTD_1:def 11;
          x in dom Exec(I,s1) by A19;
      then x in the carrier of STC N by AMI_3:36;
      then x in NAT \/ {NAT} by AMISTD_1:def 11;
then A22:   x in {NAT} by A20,XBOOLE_0:def 2;
then A23:   x in dom (NAT .-->succ(s2.NAT)) by FUNCOP_1:19;
          x in dom (NAT .-->succ(s1.NAT)) by A22,FUNCOP_1:19;
      hence Exec(I,s1).x = (NAT .-->succ(s1.NAT)).x by A16,FUNCT_4:14
         .= Exec(I,s2).x by A17,A21,A23,FUNCT_4:14;
    end;
    hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of STC N) =
      Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of STC N)
      by A18,SCMFSA6A:9;
    end;
    suppose InsCode I = 0;
    then I is halting by AMISTD_1:20;
    hence thesis by Th46;
  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 (IC-Ins-separated definite
         (non empty non void AMI-Struct over N)));
existence
  proof
    take STC N;
    thus thesis;
  end;
end;

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

registration
   let N be with_non-empty_elements set,
       S be Exec-preserving (non void AMI-Struct over 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 non void AMI-Struct over 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 Th11;
end;

theorem Th47:
 for S being standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over N)),
        F be non empty programmed FinPartState of S;
A1: dom (LastLoc F .--> (F.LastLoc F)) = {LastLoc F} by CQC_LANG:5;
    reconsider R = {[LastLoc F, F.LastLoc F]} as Relation by RELAT_1:4;
A2: R = LastLoc F .--> (F.LastLoc F) by CQC_LANG:45;
then A3: dom R = {LastLoc F} by CQC_LANG:5;
    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;
then A6:   x in dom F by 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 A5,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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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;
        a in F by A2;
then A3: a = [LastLoc F,F.LastLoc F] by A1,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 CQC_LANG:45;
    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 non void AMI-Struct over 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 non void AMI-Struct over 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 Element of the Instruction-Locations 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 by RELAT_1:4;
          R = LastLoc F .--> (F.LastLoc F) by CQC_LANG:45;
then A5:   dom R = {LastLoc F} by CQC_LANG:5;
then A6:   dom F \ dom R = dom G by Th47;
then A7:   l in dom F by A1;
then A8:   m in dom F by A2,AMISTD_1:def 20;
          locnum l in M by A3,A7;
then A9:   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 A9,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,A8,XBOOLE_0:def 4;
    end;
    hence thesis;
  end;
  end;
end;

theorem Th49:
 for S being standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over N)),
        F be non empty programmed FinPartState of S;
A1: 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 CQC_LANG:45;
then A2:   [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 A2,FUNCT_1:def 4;
    end;
    thus card CutLastLoc F = card F - card (LastLoc F .--> F.LastLoc F)
          by A1,CARD_2:63
       .= card F - card {[LastLoc F,F.LastLoc F]} by CQC_LANG:45
       .= card F - 1 by CARD_1:79;
  end;

theorem Th50:
 for S being regular standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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 A2,Lm1;
        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 Lm4;
    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 Lm5;
    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,CARD_2:59;
  end;
  end;

theorem Th51:
 for S being standard halting (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 (IC-Ins-separated definite
         (non empty non void AMI-Struct over 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;

Lm10:
    for N be with_non-empty_elements set
    for S be regular standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over N))
    for F, G be non empty programmed FinPartState of S
    holds dom (F ';' G)
     = dom CutLastLoc F \/ dom Shift(IncAddr(G,card F -' 1),card F -' 1)
      by FUNCT_4:def 1;

registration
   let N be with_non-empty_elements set,
       S be regular standard (IC-Ins-separated definite
            (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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 Lm2;
A2: dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
    thus
A3:  card (F ';' G)
      = card CutLastLoc F + card Shift(IncAddr(G,k),k) by A2,Lm3
     .= 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;
    thus thesis by A3,BINARITH:def 3;
  end;

registration
   let N be with_non-empty_elements set;
   let S be regular standard (IC-Ins-separated definite
         (non empty non void AMI-Struct over 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 Lm4;
      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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     F, G being lower non empty programmed FinPartState of S
  holds dom F c= dom (F ';' G)
  proof
    let S be regular standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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 Lm10;
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 reconsider f = x as Instruction-Location of S by TARSKI:def 1;
        x = LastLoc F by A4,TARSKI:def 1;
then A5: locnum f = locnum il.(S,card F -' 1) by AMISTD_1:55
      .= card F -' 1 by AMISTD_1:def 13
      .= card F - 1 + 0 by Lm4;
A6: card P = card F + card G - 1 by Th52
      .= card F - 1 + card G;
        0 <> card G by CARD_2:59;
    then 0 < card G;
    then locnum f < card P by A5,A6,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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over N)),
     F, G being lower non empty programmed FinPartState of S
  holds CutLastLoc F c= CutLastLoc (F ';' G)
  proof
    let S be regular standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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;
          0 <> card G by CARD_2:59;
      then 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 Lm4;
             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 Lm4;
            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 CQC_LANG:5;
      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 Th3
         .= (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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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 A3: LastLoc F in dom Shift(IncAddr(G,k),k) by A1,A2;
    thus (F ';' G).LastLoc F
       = (Shift(IncAddr(G,k),k)).LastLoc F by A3,FUNCT_4:14
      .= IncAddr(G,k).il.(S,0) by A1,A2,Def16;
  end;

theorem
     for S being regular standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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_5:def 5;
        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 A6: not il.(S,locnum f) in dom Shift(IncAddr(G,k),k) by A1,XBOOLE_0:def 3;
A7: P.il.(S,locnum f)
       = (CutLastLoc F).il.(S,locnum f) by A6,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,A7,AMI_5:def 5
      .= 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
           (IC-Ins-separated definite (non empty non void AMI-Struct over 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_5:def 5
       .= halt S by A2,AMISTD_1:def 22;
        card F <> 0 by CARD_2:59;
then A7: 1 <= card F by NAT_1:14;
        card G <> 0 by CARD_2:59;
    then card G >= 1 by NAT_1:14;
then A8: card G - 1 >= 0 by XREAL_1:50;
    then A9: k + (card G - 1) >= k+0 by XREAL_1:8;
A10: k + card G -' 1 = k + card G - 1 by A9,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 A7,BINARITH:56
      .= Shift(IncAddr(G,k),k).il.(S, k + (card G -' 1))
         by A5,A10,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
           (IC-Ins-separated definite (non empty non void AMI-Struct over 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;
        card F <> 0 by CARD_2:59;
then A3: 1 <= card F by NAT_1:14;
        card G <> 0 by CARD_2:59;
    then card G >= 1 by NAT_1:14;
then A4: card G - 1 >= 0 by XREAL_1:50;
    then A5: k + (card G - 1) >= k+0 by XREAL_1:8;
A6: k + card G -' 1 = k + card G - 1 by A5,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
A7:   P.f = halt S and
A8:   f in dom P;
    per cases by A1,A8,XBOOLE_0:def 2;
    suppose
A9:   f in dom CutLastLoc F;
then A10: (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 A7,A9,A10,GRFUNC_1:8;
    end;
    suppose
A11:   f in dom Shift(IncAddr(G,k),k);
    then consider m being Element of NAT such that
A12:   f = il.(S,m+k) and
A13:   il.(S,m) in dom IncAddr(G,k) by A2;
A14: il.(S,m) in dom G by A13,Def15;
then A15: pi(G,il.(S,m)) = G.il.(S,m) by AMI_5:def 5;
        IncAddr(pi(G,il.(S,m)),k)
      = IncAddr(G,k).il.(S,m) by A14,Def15
     .= Shift(IncAddr(G,k),k).il.(S,m+k) by A13,Def16
     .= halt S by A7,A11,A12,FUNCT_4:14;
    then G.il.(S,m) = halt S by A15,Th35;
    then il.(S,m) = LastLoc G by A14,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 A3,A6,BINARITH:56
       .= card P -' 1 by Th52;
    hence f = LastLoc P by A12,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 (IC-Ins-separated definite
         (non empty non void AMI-Struct over 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 (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 Lm10;
        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_5:def 5;
A10: x = IC Exec(pi(P,f),s2) by  A6,A7,A8;
    per cases by A1,A2,XBOOLE_0:def 2;
    suppose
A11:   f in dom CutLastLoc F;
then A12: 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,A11,XBOOLE_0:def 3;
    then s2.f = (CutLastLoc F).f by A8,A9,FUNCT_4:12
        .= F.f by A11,GRFUNC_1:8
        .= pi(F,f) by A4,A11,AMI_5:def 5;
    then IC Following s2 in NIC(pi(F,f),f) by A7;
then A13: x in dom F by A6,A12;
        dom F c= dom P by Th53;
    hence x in dom P by A13;
    end;
    suppose
A14:   f in dom Shift(IncAddr(G,k),k);
    then consider m being Element of NAT such that
A15:   f = il.(S,m+k) and
A16:   il.(S,m) in dom IncAddr(G,k) by A5;
A17: il.(S,m) in dom G by A16,Def15;
then A18: NIC(pi(G,il.(S,m)),il.(S,m)) c= dom G by AMISTD_1:def 17;
A19: ObjectKind IC S = the Instruction-Locations of S by AMI_1:def 11;
    then reconsider v = IC S .--> il.(S,m) as FinPartState of S by AMI_1:59;
    set s1 = s2 +* v;
A20: pi(P,f) = Shift(IncAddr(G,k),k).f by A9,A14,FUNCT_4:14
          .= IncAddr(G,k).il.(S,m) by A15,A16,Def16;
A21: (IC S .--> il.(S,m)).IC S = il.(S,m) by CQC_LANG:6;
A22: IC S in {IC S} by TARSKI:def 1;
A23: dom (IC S .--> il.(S,m)) = {IC S} by CQC_LANG:5;
A24: IC s1 = il.(S,m) by A21,A22,A23,FUNCT_4:14;
A25: dom s2 = the carrier of S by AMI_3:36;
    reconsider w = IC S .--> (IC s1 + k) as FinPartState of S by A19,AMI_1:59;
        s1 +* w is State of S;
then A26: dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by AMI_3:36;
        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;
A27:   dom (IC S .--> (IC s1 + k)) = {IC S} by CQC_LANG:5;
      per cases;
      suppose
A28:     a = IC S;
      hence s2.a = il.(S,locnum IC s1 + k) by  A7,A15,A24,AMISTD_1:def 13
        .= (IC S .--> (IC s1 + k)).a by A28,CQC_LANG:6
        .= (s1 +* (IC S .--> (IC s1 + k))).a by A22,A27,A28,FUNCT_4:14;
      end;
      suppose
A29:     a <> IC S;
then A30:   not a in dom (IC S .--> (IC s1 + k)) by A27,TARSKI:def 1;
          not a in dom (IC S .--> il.(S,m)) by A23,A29,TARSKI:def 1;
      then s1.a = s2.a by FUNCT_4:12;
      hence s2.a = (s1 +* (IC S .--> (IC s1 + k))).a by A30,FUNCT_4:12;
    end;
    end;
then A31: s2 = s1 +* (IC S .--> (IC s1 + k)) by A25,A26,FUNCT_1:9;
    set s3 = s1 +* (il.(S,m) .--> pi(G,il.(S,m)));
A32: dom (il.(S,m) .--> pi(G,il.(S,m))) = {il.(S,m)} by CQC_LANG:5;
then A33: il.(S,m) in dom (il.(S,m) .--> pi(G,il.(S,m))) by TARSKI:def 1;
         IC S <> il.(S,m) by AMI_1:48;
then A34: not IC S in dom (il.(S,m) .--> pi(G,il.(S,m))) by A32,TARSKI:def 1;
A35: IC s3 = s1.IC S by A34,FUNCT_4:12
         .= il.(S,m) by A21,A22,A23,FUNCT_4:14;
A36: s3.il.(S,m) = (il.(S,m) .--> pi(G,il.(S,m))).il.(S,m) by A33,FUNCT_4:14
       .= pi(G,il.(S,m)) by CQC_LANG:6;
        s1, s3 equal_outside the Instruction-Locations of S
    proof
A37:   dom s1 = the carrier of S & dom s3 = the carrier of S by AMI_3:36;
          for x being set st x in dom s1 \ the Instruction-Locations of S holds
        s1.x = s3.x
      proof
        let x be set;
        assume A38: x in dom s1 \ the Instruction-Locations of S;
            now
          assume x in dom (il.(S,m) .--> pi(G,il.(S,m)));
          then x = il.(S,m) by A32,TARSKI:def 1;
          hence contradiction by A38,XBOOLE_0:def 4;
        end;
        hence s1.x = s3.x by FUNCT_4:12;
      end;
      hence s1|(dom s1 \ the Instruction-Locations of S) =
         s3|(dom s3 \ the Instruction-Locations of S) by A37,SCMFSA6A:9;
    end;
then A39: Exec(pi(G,il.(S,m)),s1), Exec(pi(G,il.(S,m)),s3)
         equal_outside the Instruction-Locations of S by Def19;
    reconsider k,m as Element of NAT;
A40: x = IC Exec(IncAddr(pi(G,il.(S,m)),k),s2) by A10,A17,A20,Def15
     .= IC Exec(pi(G,il.(S,m)), s1) + k by A31,Def17
     .= il.(S,locnum IC Exec(pi(G,il.(S,m)), s3) + k) by A39,SCMFSA6A:29;
        IC Following s3 = il.(S,locnum IC Exec(pi(G,il.(S,m)), s3))
          by A35,A36,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 A35,A36;
    then il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in dom G by A18;
    then A41:   il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in dom IncAddr(G,k)
       by Def15;
    reconsider nn = locnum IC Exec(pi(G,il.(S,m)), s3) as Element of NAT;
      x in dom Shift(IncAddr(G,k),k) by A5,A40,A41;
    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 (IC-Ins-separated definite
             (non empty non void AMI-Struct over N))
  holds IncAddr(Stop S, k) = Stop S
  proof
    let S be regular standard halting without_implicit_jumps
             realistic (IC-Ins-separated definite
             (non empty non void AMI-Struct over N));
A1: dom IncAddr(Stop S, k) = dom Stop S by Def15
     .= {il.(S,0)} by Lm7;
A2: dom Stop S = {il.(S,0)} by Lm7;
    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_5:def 5
        .= halt S by CQC_LANG:6;
      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,CQC_LANG:6;
    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 non void AMI-Struct over N))
  holds Shift(Stop S, k) = il.(S,k) .--> halt S
  proof
    let S be standard halting (IC-Ins-separated definite
        (non empty non void AMI-Struct over 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 Lm7;
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,Lm7;
        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 CQC_LANG:5;
        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 Lm7;
      hence (Shift(Stop S, k)).x = (Stop S).il.(S,0) by A7,Def16
         .= halt S by Lm8
         .= (il.(S,k) .--> halt S).x by A7,CQC_LANG:6;
    end;
    hence thesis by A3,A6,FUNCT_1:9;
  end;

theorem Th59:
 for S being regular standard halting without_implicit_jumps
             realistic (IC-Ins-separated definite
             (non empty non void AMI-Struct over N)),
     F being pre-Macro of S
  holds F ';' Stop S = F
  proof
    let S be regular standard halting without_implicit_jumps
             realistic (IC-Ins-separated definite
             (non empty non void AMI-Struct over 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 CQC_LANG:5
      .= {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 Lm7;
          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 Lm8
          .= 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
       (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
     F being pre-Macro of S
  holds Stop S ';' F = F
  proof
    let S be regular standard halting
         (IC-Ins-separated definite (non empty non void AMI-Struct over N)),
        F be pre-Macro of S;
    set k = card Stop S -' 1;
A1: k = 0 by Lm9;
    thus Stop S ';' F = CutLastLoc Stop S +* Shift(F,k) by A1,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 (IC-Ins-separated
             definite (non empty non void AMI-Struct over 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 (IC-Ins-separated
             definite (non empty non void AMI-Struct over 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 Lm4
       .= 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 Lm4
       .= (card G -' 1) + (card F -' 1) by Lm4;
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 Lm4;
A18:   card G -' 1 = card G - 1 by Lm4;
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 W <> Stop S;
then A20:     card W <> 1 by Th26;
A21:     card W <> 0 by CARD_2:59;
        assume 2 > card W;
        then 1 + 1 > card W;
        then card W <= 1 by NAT_1:13;
        hence contradiction by A20,A21,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,Lm6;
      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 Lm4;
        then m + (card F - 1) < card F -' 1 by A24,Lm4;
        then m + (card F -' 1) < card F -' 1 by Lm4;
        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,Lm4;
        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,Lm4;
        then m + (card G -' 1) = (card F -' 1) - (card F -' 1);
        then card G -' 1 = 0 by NAT_1:7;
        then card G - 1 = 0 by Lm4;
        then card G = 1;
        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,Lm4;
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,Lm4;
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 Lm10;
          now
A43:     dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
          = {LastLoc (F ';' G)} by CQC_LANG:5
         .= {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;
        then card G - 1 = 0 by Lm4;
        then card G = 1;
        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
            card G <> 0 by CARD_2:59;
        hence 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 Lm4;
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_5:def 5
        .= (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_5:def 5;
      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
,Th3
        .= 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 Lm5;
      end;
          card F -' 1 <= card F by BINARITH:52;
      then k >= card F -' 1 by A49,XXREAL_0:2;
then A53:   x = il.(S, k -' (card F -' 1) + (card F -' 1)) by A9,BINARITH:53;
         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 Lm4;
         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 Lm4;
      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 Lm10;
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 CQC_LANG:5;
        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,Lm4;
        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)