:: Weakly Standard Ordering of Instruction Locations
::  by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 22, 2010
:: Copyright (c) 2010-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, SUBSET_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1,
      RELAT_1, TARSKI, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, NAT_1, GLIB_000,
      XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, GRAPH_2, CARD_1, FUNCT_2,
      FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, WAYBEL_0, MEMBERED, AMISTD_1,
      EXTPRO_1, AMI_WSTD, STRUCT_0, COMPOS_1, QUANTAL1, GOBRD13, MEMSTR_0,
      FUNCT_7, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, ORDINAL1,
      CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1,
      PARTFUN1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1,
      FUNCT_4, FUNCT_7, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0,
      COMPOS_0, FINSEQ_6, COMPOS_1, EXTPRO_1, FUNCT_2, AMISTD_1;
 constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, RELSET_1,
      PRE_POLY, GRAPH_2, AMISTD_1, FUNCT_7, FUNCT_4, PBOOLE,
      FINSEQ_6, XTUPLE_0;
 registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1,
      XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, JORDAN1J, CARD_1,
      XXREAL_2, RELSET_1, FUNCT_4, AMISTD_1, EXTPRO_1, PRE_POLY, MEMSTR_0,
      MEASURE6, COMPOS_0, XTUPLE_0, ORDINAL1, FINSEQ_6;
 requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, AMISTD_1;
 equalities STRUCT_0, EXTPRO_1, XBOOLE_0, FUNCOP_1, NAT_1, AMISTD_1, MEMSTR_0,
      CARD_1, ORDINAL1;
 expansions XBOOLE_0;
 theorems TARSKI, FINSEQ_4, FINSEQ_1, GRAPH_2, NAT_1, FUNCT_4, FUNCT_1,
      FUNCT_2, ZFMISC_1, CARD_1, FUNCOP_1, ORDINAL1, GRFUNC_1, FINSEQ_3, INT_1,
      REVROT_1, FUNCT_7, XBOOLE_0, MEMBERED, XREAL_1, XXREAL_0, FINSEQ_6,
      PARTFUN1, XXREAL_2, XREAL_0, NAT_D, PBOOLE, AMISTD_1,
      MEMSTR_0, CARD_3;
 schemes NAT_1, FUNCT_7, FINSEQ_2, FRAENKEL, DOMAIN_1, FINSEQ_4;

begin :: Ami-Struct

reserve x for set,
  D for non empty set,
  k, n for Element of NAT,
  z for Nat;
reserve N for with_zero set,
  S for
    IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
  i for Element of the InstructionsF of S,
  l, l1, l2, l3 for Element of NAT,
  s for State of S;
reserve ss for Element of product the_Values_of S;

begin :: Ordering of Instruction Locations

definition
  let N,S; let l1,l2 be Nat;
  pred l1 <= l2, S means
  ex f being non empty FinSequence of NAT st f/.1
= l1 & f/.len f = l2 & for n st 1 <= n & n < len f
 holds f/.(n+1) in SUCC(f/.n,S);
end;

theorem
 for N,S for l1,l2 being Nat holds
  l1 <= l2,S & l2 <= l3, S implies l1 <= l3, S
proof let N,S;  let l1,l2 be Nat;
  given f1 being non empty FinSequence of NAT such that
A1: f1/.1 = l1 and
A2: f1/.len f1 = l2 and
A3: for n st 1 <= n & n < len f1 holds f1/.(n+1) in SUCC(f1/.n,S);
  given f2 being non empty FinSequence of NAT such that
A4: f2/.1 = l2 and
A5: f2/.len f2 = l3 and
A6: for n st 1 <= n & n < len f2 holds f2/.(n+1) in SUCC(f2/.n,S);
  take f1^'f2;
  thus (f1^'f2)/.1 = l1 by A1,FINSEQ_6:155;
  now
    per cases;
    suppose
      f2 is trivial;
      then
A7:   ex x being Element of NAT st f2 = <*x*> by FINSEQ_6:107;
      then f1^'f2 = f1 by FINSEQ_6:158;
      hence (f1^'f2)/.len(f1^'f2) = l3 by A2,A4,A5,A7,FINSEQ_1:39;
    end;
    suppose
      f2 is not trivial;
      hence (f1^'f2)/.len(f1^'f2) = l3 by A5,FINSEQ_6:156;
    end;
  end;
  hence (f1^'f2)/.len(f1^'f2) = l3;
  let n such that
A8: 1 <= n and
A9: n < len(f1^'f2);
A10: len (f1^'f2) +1 = len f1 + len f2 by FINSEQ_6:139;
  per cases by XXREAL_0:1;
  suppose
A11: n < len f1;
    then n+1 <= len f1 by NAT_1:13;
    then
A12: (f1^'f2)/.(n+1) = f1/.(n+1) by FINSEQ_6:159,NAT_1:11;
    (f1^'f2)/.n = f1/.n by A8,A11,FINSEQ_6:159;
    hence thesis by A3,A8,A11,A12;
  end;
  suppose
A13: n = len f1;
    then
A14: (f1^'f2)/.n = f2/.1 by A2,A4,A8,FINSEQ_6:159;
    n+1 < len (f1^'f2) +1 by A9,XREAL_1:6;
    then
A15: 1 < len f2 by A10,A13,XREAL_1:6;
    then (f1^'f2)/.(n+1) = f2/.(1+1) by A13,FINSEQ_6:160;
    hence thesis by A6,A14,A15;
  end;
  suppose
A16: n > len f1;
    then consider m being Nat such that
A17: len f1 + m = n by NAT_1:10;
    reconsider m as Element of NAT by ORDINAL1:def 12;
A18: len f1 + m > len f1 + 0 by A16,A17;
    len f1 + m+1 < len f1 + len f2 by A9,A10,A17,XREAL_1:6;
    then len f1 + (m+1) < len f1 + len f2;
    then
A19: m+1 < len f2 by XREAL_1:6;
A20: (f1^'f2)/.(n+1) = (f1^'f2)/.(len f1 + (m+1)) by A17
      .= f2/.(m+1+1) by A19,FINSEQ_6:160,NAT_1:11;
    m <= m+1 by NAT_1:11;
    then m < len f2 by A19,XXREAL_0:2;
    then (f1^'f2)/.n = f2/.(m+1) by A17,A18,FINSEQ_6:160,NAT_1:14;
    hence thesis by A6,A19,A20,NAT_1:11;
  end;
end;

definition
  let N, S;
  attr S is InsLoc-antisymmetric means
  for l1, l2 st l1 <= l2, S & l2 <= l1, S holds
  l1 = l2;
end;

definition
  let N, S;
  attr S is weakly_standard means
  :Def3:
  ex f being sequence of NAT st f is
  bijective & for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
end;

theorem Th2:
  for f1, f2 being sequence of NAT st f1 is bijective & (for
m, n being Element of NAT holds m <= n iff f1.m <= f1.n,S) & f2 is bijective &
 (for m, n being Element of NAT holds m <= n iff f2.m <= f2.n, S) holds f1 = f2
proof
  let f1, f2 be sequence of NAT such that
A1: f1 is bijective and
A2: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n,S and
A3: f2 is bijective and
A4: for m, n being Element of NAT holds m <= n iff f2.m <= f2.n,S;
A5: dom f1 = NAT by FUNCT_2:def 1;
A6: dom f2 = NAT by FUNCT_2:def 1;
  defpred P[Nat] means f1.$1 <> f2.$1;
  assume f1 <> f2;
  then ex c being Element of NAT st P[c] by FUNCT_2:63;
  then
A7: ex c being Nat st P[c];
  consider d being Nat such that
A8: P[d] and
A9: for n being Nat st P[n] holds d <= n from NAT_1:sch 5(A7);
  reconsider d as Element of NAT by ORDINAL1:def 12;
A10: rng f1 = NAT by A1,FUNCT_2:def 3;
A11:  rng f2 = NAT by A3,FUNCT_2:def 3;
  consider d1 being object such that
A12: d1 in dom f1 and
A13: f2.d = f1.d1 by A10,FUNCT_1:def 3;
  reconsider d1 as Element of NAT by A12;
  consider d2 being object such that
A14: d2 in dom f2 and
A15: f1.d = f2.d2 by A11,FUNCT_1:def 3;
  reconsider d2 as Element of NAT by A14;
  per cases;
  suppose
A16: d1 <= d & d2 <= d;
    then f2.d2 <= f2.d, S by A4;
    then d <= d1 by A2,A15,A13;
    hence contradiction by A8,A13,A16,XXREAL_0:1;
  end;
  suppose
A17: d <= d1 & d2 <= d;
    f2.d2 = f1.d2
    proof
      assume not thesis;
      then d <= d2 by A9;
      hence contradiction by A8,A15,A17,XXREAL_0:1;
    end;
    hence contradiction by A1,A8,A15,A5,FUNCT_1:def 4;
  end;
  suppose
A18: d1 <= d & d <= d2;
    f1.d1 = f2.d1
    proof
      assume not thesis;
      then d <= d1 by A9;
      hence contradiction by A8,A13,A18,XXREAL_0:1;
    end;
    hence contradiction by A3,A8,A13,A6,FUNCT_1:def 4;
  end;
  suppose
A19: d <= d1 & d <= d2;
    then f2.d <= f2.d2,S by A4;
    then d1 <= d by A2,A15,A13;
    hence contradiction by A8,A13,A19,XXREAL_0:1;
  end;
end;

Lm1: k <= k, S
  proof
     reconsider l=k as Element of NAT;
     reconsider f = <*l*> as non empty FinSequence of NAT;
    take f;
    thus f/.1 = k by FINSEQ_4:16;
    hence thesis by FINSEQ_1:39;
  end;

theorem Th3:
  for f being sequence of NAT st f is bijective holds
  (for m, n being Element of NAT holds m <= n iff f.m <= f.n, S)
   iff for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) &
    for j being Element of NAT st f.j in SUCC(f.k,S) holds k <= j
proof
  let f be sequence of NAT;
  assume
A1: f is bijective;
  hereby
    assume
A2: for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
    let k be Element of NAT;
    k <= k+1 by NAT_1:11;
    then f.k <= f.(k+1), S by A2;
    then consider F being non empty FinSequence of NAT such that
A3: F/.1 = f.k and
A4: F/.len F = f.(k+1) and
A5: for n st 1 <= n & n < len F holds F/.(n+1) in SUCC(F/.n,S);
    set F1 = F -| f.(k+1);
    set x = (f.(k+1))..F;
A6: f.(k+1) in rng F by A4,FINSEQ_6:168;
    then
A7: len F1 = x-1 by FINSEQ_4:34;
    then
A8: len F1+1 = x;
A9: x in dom F by A6,FINSEQ_4:20;
    then
A10: F/.(len F1+1) = F.x by A7,PARTFUN1:def 6
      .= f.(k+1) by A6,FINSEQ_4:19;
    x <= len F by A9,FINSEQ_3:25;
    then
A11: len F1 < len F by A8,NAT_1:13;
    1 <= len F by NAT_1:14;
    then
A12: 1 in dom F by FINSEQ_3:25;
    then
A13: F/.1 = F.1 by PARTFUN1:def 6;
A14: F.x = f.(k+1) by A6,FINSEQ_4:19;
A15: dom f = NAT by FUNCT_2:def 1;
A16: f.k <> f.(k+1)
    proof
      assume not thesis;
      then 0+k = k+1 by A1,A15,FUNCT_1:def 4;
      hence contradiction;
    end;
    then
A17:   len F1 <> 0 by A3,A14,A12,A7,PARTFUN1:def 6;
    1 <= x by A9,FINSEQ_3:25;
    then 1 < x by A3,A16,A14,A13,XXREAL_0:1;
    then
A18: 1 <= len F1 by A8,NAT_1:13;
    reconsider F1 as non empty FinSequence of NAT by A17,A6,FINSEQ_4:41;
    rng f = NAT by A1,FUNCT_2:def 3;
    then consider m being object such that
A19: m in dom f and
A20: f.m = F/.len F1 by FUNCT_1:def 3;
    reconsider m as Element of NAT by A19;
A21: len F1 in dom F by A18,A11,FINSEQ_3:25;
A22: len F1 in dom F1 by A18,FINSEQ_3:25;
    then
A23: F1/.len F1 = F1.len F1 by PARTFUN1:def 6
      .= F.len F1 by A6,A22,FINSEQ_4:36
      .= F/.len F1 by A21,PARTFUN1:def 6;
A24: now
      (rng F1) misses {f.(k+1)} by A6,FINSEQ_4:38;
      then rng F1 /\ {f.(k+1)} = {};
      then
A25:  not f.(k+1) in rng F1 or not f.(k+1) in {f.(k+1)} by XBOOLE_0:def 4;
      assume
A26:  m = k+1;
A27:  len F1 in dom F1 by A18,FINSEQ_3:25;
      then F1/.len F1 = F1.len F1 by PARTFUN1:def 6;
      hence contradiction by A20,A23,A26,A25,A27,FUNCT_1:def 3,TARSKI:def 1;
    end;
    reconsider F2 = <*F/.len F1, F/.x*> as non empty FinSequence of NAT;
A28: len F2 = 2 by FINSEQ_1:44;
    then
A29: 2 in dom F2 by FINSEQ_3:25;
    then
A30: F2/.len F2 = F2.2 by A28,PARTFUN1:def 6
      .= F/.x by FINSEQ_1:44
      .= f.(k+1) by A14,A9,PARTFUN1:def 6;
A31: 1 in dom F2 by A28,FINSEQ_3:25;
A32: now
      let n;
      assume 1 <= n & n < len F2;
      then n <> 0 & n < 1+1 by FINSEQ_1:44;
      then n <> 0 & n <= 1 by NAT_1:13;
      then
A33:  n = 1 by NAT_1:25;
      then
A34:  F2/.n = F2.1 by A31,PARTFUN1:def 6
        .= F/.len F1 by FINSEQ_1:44;
      F2/.(n+1) = F2.2 by A29,A33,PARTFUN1:def 6
        .= F/.(len F1+1) by A7,FINSEQ_1:44;
      hence F2/.(n+1) in SUCC(F2/.n,S) by A5,A18,A11,A34;
    end;
A35: now
      let n;
      assume that
A36:  1 <= n and
A37:  n < len F1;
A38:  1 <= n+1 by A36,NAT_1:13;
A39:  n+1 <= len F1 by A37,NAT_1:13;
      then n+1 <= len F by A11,XXREAL_0:2;
      then
A40:  n+1 in dom F by A38,FINSEQ_3:25;
      n <= len F by A11,A37,XXREAL_0:2;
      then
A41:  n in dom F by A36,FINSEQ_3:25;
A42:  n in dom F1 by A36,A37,FINSEQ_3:25;
      then
A43:  F1/.n = F1.n by PARTFUN1:def 6
        .= F.n by A6,A42,FINSEQ_4:36
        .= F/.n by A41,PARTFUN1:def 6;
A44:  n < len F by A11,A37,XXREAL_0:2;
A45:  n+1 in dom F1 by A38,A39,FINSEQ_3:25;
      then F1/.(n+1) = F1.(n+1) by PARTFUN1:def 6
        .= F.(n+1) by A6,A45,FINSEQ_4:36
        .= F/.(n+1) by A40,PARTFUN1:def 6;
      hence F1/.(n+1) in SUCC(F1/.n,S) by A5,A36,A43,A44;
    end;
    F2/.1 = F2.1 by A31,PARTFUN1:def 6
      .= f.m by A20,FINSEQ_1:44;
    then f.m <= f.(k+1), S by A30,A32;
    then
A46: m <= k+1 by A2;
A47: 1 in dom F1 by A18,FINSEQ_3:25;
    then F1/.1 = F1.1 by PARTFUN1:def 6
      .= F.1 by A6,A47,FINSEQ_4:36
      .= f.k by A3,A12,PARTFUN1:def 6;
    then f.k <= f.m, S by A20,A23,A35;
    then k <= m by A2;
    then m = k or m = k+1 by A46,NAT_1:9;
    hence f.(k+1) in SUCC(f.k,S) by A5,A18,A11,A10,A20,A24;
    let j be Element of NAT;
    reconsider fk=f.k, fj=f.j as Element of NAT;
    reconsider F = <*fk, fj*> as non empty FinSequence of NAT;
A48: len F = 2 by FINSEQ_1:44;
    then
A49: 2 in dom F by FINSEQ_3:25;
A50: 1 in dom F by A48,FINSEQ_3:25;
    then
A51: F/.1 = F.1 by PARTFUN1:def 6
      .= f.k by FINSEQ_1:44;
    assume
A52: f.j in SUCC(f.k,S);
A53: now
      let n be Element of NAT;
      assume 1 <= n & n < len F;
      then n <> 0 & n < 1+1 by FINSEQ_1:44;
      then n <> 0 & n <= 1 by NAT_1:13;
      then
A54:  n = 1 by NAT_1:25;
      then
A55:  F/.n = F.1 by A50,PARTFUN1:def 6
        .= f.k by FINSEQ_1:44;
      F/.(n+1) = F.2 by A49,A54,PARTFUN1:def 6
        .= f.j by FINSEQ_1:44;
      hence F/.(n+1) in SUCC(F/.n,S) by A52,A55;
    end;
    F/.len F = F.2 by A48,A49,PARTFUN1:def 6
      .= f.j by FINSEQ_1:44;
    then f.k <= f.j, S by A51,A53;
    hence k <= j by A2;
  end;
  assume
A56: for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j
  being Element of NAT st f.j in SUCC(f.k,S) holds k <= j;
  let m, n be Element of NAT;
  hereby
    assume
A57: m <= n;
    per cases by A57,XXREAL_0:1;
    suppose
      m = n;
      hence f.m <= f.n, S by Lm1;
    end;
    suppose
A58:  m < n;
      thus f.m <= f.n, S
      proof
        reconsider f9=f as sequence of NAT;
        set mn = n -' m;
        deffunc F(Nat) = f9.(m+$1-'1);
        consider F being FinSequence of NAT such that
A59:    len F = mn+1 and
A60:    for j being Nat st j in dom F holds F.j = F(j) from FINSEQ_2:
        sch 1;
        reconsider F as non empty FinSequence of NAT by A59;
        take F;
A61:    1 <= mn+1 by NAT_1:11;
        then
A62:    1 in dom F by A59,FINSEQ_3:25;
        hence F/.1 = F.1 by PARTFUN1:def 6
          .= f.(m+1-'1) by A60,A62
          .= f.m by NAT_D:34;
        m+1 <= n by A58,INT_1:7;
        then 1 <= n-m by XREAL_1:19;
        then 0 <= n-m;
        then
A63:    mn = n - m by XREAL_0:def 2;
A64:    len F in dom F by A59,A61,FINSEQ_3:25;
        hence F/.len F = F.len F by PARTFUN1:def 6
          .= f.(m+(mn+1)-'1) by A59,A60,A64
          .= f.(m+mn+1-'1)
          .= f.n by A63,NAT_D:34;
        let p be Element of NAT;
        assume that
A65:    1 <= p and
A66:    p < len F;
A67:    p in dom F by A65,A66,FINSEQ_3:25;
        then
A68:    F/.p = F.p by PARTFUN1:def 6
          .= f.(m+p-'1) by A60,A67;
A69:    p <= m+p by NAT_1:11;
        1 <= p+1 & p+1 <= len F by A65,A66,NAT_1:13;
        then
A70:    p+1 in dom F by FINSEQ_3:25;
        then F/.(p+1) = F.(p+1) by PARTFUN1:def 6
          .= f.(m+(p+1)-'1) by A60,A70
          .= f.(m+p+1-'1)
          .= f.(m+p-'1+1) by A65,A69,NAT_D:38,XXREAL_0:2;
        hence thesis by A56,A68;
      end;
    end;
  end;
  assume f.m <= f.n, S;
  then consider F being non empty FinSequence of NAT such that
A71: F/.1 = f.m and
A72: F/.len F = f.n and
A73: for n being Element of NAT st 1 <= n & n < len F holds F/.(n+1) in
  SUCC(F/.n,S);
  defpred P[Nat] means
   1 <= $1 & $1 <= len F implies ex l being
  Element of NAT st F/.$1 = f.l & m <= l;
A74: now
    let k be Nat such that
A75: P[k];
    now
      assume that
      1 <= k+1 and
A76:  k+1 <= len F;
      per cases;
      suppose
        k = 0;
        hence ex l being Element of NAT st F/.(k+1) = f.l & m <= l by A71;
      end;
      suppose
A77:    k > 0;
        rng f = NAT by A1,FUNCT_2:def 3;
        then consider l1 being object such that
A78:    l1 in dom f and
A79:    f.l1 = F/.(k+1) by FUNCT_1:def 3;
        consider l being Element of NAT such that
A80:    F/.k = f.l and
A81:    m <= l by A75,A76,A77,NAT_1:13,14;
        reconsider l1 as Element of NAT by A78;
        reconsider kk=k as Element of NAT by ORDINAL1:def 12;
        k < len F by A76,NAT_1:13;
        then F/.(kk+1) in SUCC(F/.kk,S) by A73,A77,NAT_1:14;
        then l <= l1 by A56,A80,A79;
        hence
        ex l being Element of NAT st F/.(k+1) = f.l & m <= l by A81,A79,
XXREAL_0:2;
      end;
    end;
    hence P[k+1];
  end;
A82: 1 <= len F by NAT_1:14;
A83: P[0];
  for k being Nat holds P[k] from NAT_1:sch 2(A83, A74);
  then dom f = NAT & ex l being Element of NAT st F/.len F = f.l & m <= l by
A82,FUNCT_2:def 1;
  hence thesis by A1,A72,FUNCT_1:def 4;
end;

theorem Th4:
  S is weakly_standard iff ex f being sequence of NAT st f is
  bijective & for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j
  being Element of NAT st f.j in SUCC(f.k,S) holds k <= j
proof
  hereby
    assume S is weakly_standard;
    then consider f being sequence of NAT such that
A1: f is bijective and
A2: for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
    thus ex f being sequence of NAT st f is bijective & for k being
Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j being Element of NAT st f.j
    in SUCC(f.k,S) holds k <= j
    proof
      take f;
      thus f is bijective by A1;
      thus thesis by A1,A2,Th3;
    end;
  end;
  given f be sequence of NAT such that
A3: f is bijective and
A4: for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j being
  Element of NAT st f.j in SUCC(f.k,S) holds k <= j;
  take f;
  thus f is bijective by A3;
  thus thesis by A3,A4,Th3;
end;

set III = {[1,0,0],[0,0,0]};

begin :: Standard trivial computer

Lm2: for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds IC Exec(i,s) = IC s + 1

proof
  let i be Instruction of STC N, s be State of STC N;
  set M = STC N;
  assume
A1: InsCode i = 1;
A2: now
    assume i in {[0,0,0]};
    then i = [0,0,0] by TARSKI:def 1;
    hence contradiction by A1;
  end;
  the InstructionsF of M = III by AMISTD_1:def 7;
  then i = [1,0,0] or i = [0,0,0] by TARSKI:def 2;
  then
A3: i in {[1,0,0]} by A1,TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;
  then
A5: 0 in dom (0 .-->(In(s.0,NAT)+1));

  consider f be Function of product the_Values_of M, product
  the_Values_of M such that
A6: for s being Element of product the_Values_of M holds f.s = s+*(
  0 .--> (In(s.0,NAT)+1)) and

A7: the Execution of M = ([1,0,0] .--> f) +* ([0,0,0] .--> id product
  the_Values_of M) by AMISTD_1:def 7;
A8: for s being State of M holds f.s = s+*(0 .-->(In(s.0,NAT)+1))
 proof let s be State of M;
  reconsider s as Element of product the_Values_of M by CARD_3:107;
  f.s = s+*(0 .-->(In(s.0,NAT)+1)) by A6;
  hence thesis;
 end;
A9: IC M = 0 by AMISTD_1:def 7;
A10: s in product the_Values_of M by CARD_3:107;
   dom(the_Values_of M) = the carrier of M by PARTFUN1:def 2
     .= {0} by AMISTD_1:def 7;
    then
A11:  0 in dom(the_Values_of M) by TARSKI:def 1;
  Values IC M = NAT by MEMSTR_0:def 6;
  then reconsider k = s.0 as Element of NAT by A10,A11,CARD_3:9,A9;
  dom ([0,0,0] .--> id product the_Values_of M) = {[0,0,0]};
  then (the Execution of M).i = ([1,0,0] .--> f).i by A7,A2,FUNCT_4:11
    .= f by A3,FUNCOP_1:7;
  hence IC Exec(i,s) = (s+*(0 .-->(In(s.0,NAT)+1))).0 by A9,A8
    .= (0 .-->(In(k,NAT)+1)).0 by A5,FUNCT_4:13
    .= IC s + 1 by A9,A4,FUNCOP_1:7;
end;

Lm3: for l being Element of NAT, i being Element of the
InstructionsF of STC N st l = z & InsCode i = 1 holds NIC(i, l) = {z+1}
proof
  let l be Element of NAT, i be Element of the InstructionsF of STC N;
  assume that
A1: l = z and
A2: InsCode i = 1;
  set M = STC N;
  set F = { IC Exec(i,ss)
     where ss is Element of product the_Values_of STC N:
    IC ss = l };
  now
    reconsider f = NAT --> i
     as Instruction-Sequence of M;
    reconsider l9 = l as Element of Values IC M by MEMSTR_0:def 6;
    reconsider w = the l-started State of M
     as Element of product the_Values_of M by CARD_3:107;
    set u = (IC M).-->l9;
    let y be object;
    reconsider t = w+*u as Element of product the_Values_of STC N
     by CARD_3:107;
    hereby
      assume y in F;
      then ex s being Element of product the_Values_of STC N
      st y = IC Exec(i,s) & IC s = l;
      then y = z + 1 by A1,A2,Lm2;
      hence y in {z+1} by TARSKI:def 1;
    end;
    assume y in {z+1};
    then
A4: y = z+1 by TARSKI:def 1;
    IC M in dom u by TARSKI:def 1;
    then
A5: IC t = u.IC M by FUNCT_4:13
      .= z by A1,FUNCOP_1:72;
    then IC Exec(i,t) = z+1 by A2,Lm2;
    hence y in F by A1,A4,A5;
  end;
  hence thesis by TARSKI:2;
end;

registration
  let N be with_zero set;
  cluster STC N -> weakly_standard;
  coherence
  proof
    reconsider f = id NAT as sequence of NAT;
    set M = STC N;
    now
      let k be Element of NAT;
      reconsider fk = f.k as Element of NAT;
A1:   SUCC(fk,STC N) = {k,k+1} by AMISTD_1:8;
      thus f.(k+1) in SUCC(f.k,STC N) by A1,TARSKI:def 2;
      let j be Element of NAT;
      assume f.j in SUCC(f.k,STC N);
      then f.j = k or f.j = k+1 by A1,TARSKI:def 2;
      then j = k+1 or j = k;
      hence k <= j by NAT_1:11;
    end;
    hence thesis by Th4;
  end;
end;

registration
  let N be with_zero set;
  cluster weakly_standard halting
    for IC-Ins-separated non empty with_non-empty_values AMI-Struct
    over N;
  existence
  proof
    take STC N;
    thus thesis;
  end;
end;

reserve T for weakly_standard
 IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N, k be natural Number;
  func il.(S,k) -> Element of NAT means
  :Def4:
  ex f being
sequence of NAT st f is bijective & (for m, n being Element of NAT holds
  m <= n iff f.m <= f.n, S) & it = f.k;
  existence
  proof
    reconsider k as Element of NAT by ORDINAL1:def 12;
    consider f being sequence of NAT such that
A1: f is bijective & for m, n being Element of NAT holds m <= n iff f.
    m <= f.n, S by Def3;
      reconsider fk = f.k as Element of NAT;
    take fk;
    take f;
    thus thesis by A1;
  end;
  uniqueness by Th2;
end;

theorem Th5:
  for N,T
  for k1, k2 being Nat st il.(T,k1) = il.(T,k2) holds
  k1 = k2
proof let N,T;
  let k1, k2 be Nat;
  assume
A1: il.(T,k1) = il.(T,k2);
A2: k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12;
  consider f2 being sequence of NAT such that
A3: f2 is bijective & for m, n being Element of NAT holds m <= n iff f2.
  m <= f2. n, T and
A4: il.(T,k2) = f2.k2 by Def4;
  consider f1 being sequence of NAT such that
A5: f1 is bijective and
A6: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n, T and
A7: il.(T,k1) = f1.k1 by Def4;
A8: dom f1 = NAT by FUNCT_2:def 1;
  f1 = f2 by A5,A6,A3,Th2;
  hence thesis by A1,A2,A5,A7,A4,A8,FUNCT_1:def 4;
end;

theorem Th6:
  for l being Nat ex k being Nat st l = il.(T,k)
proof
  let l be Nat;
  consider f1 being sequence of NAT such that
A1: f1 is bijective and
A2: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n, T and
  il.(T,0) = f1.0 by Def4;
  l in NAT & rng f1 = NAT by A1,FUNCT_2:def 3,ORDINAL1:def 12;
  then consider k being object such that
A3: k in dom f1 and
A4: f1.k = l by FUNCT_1:def 3;
  reconsider k as Nat by A3;
  take k;
  reconsider l as Element of NAT by ORDINAL1:def 12;
   l = il.(T,k) by A1,A2,A4,Def4;
  hence thesis;
end;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, l be Nat;
  func locnum(l,S) -> Nat means
  :Def5:
  il.(S,it) = l;
  existence by Th6;
  uniqueness by Th5;
end;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, l be Nat;
  redefine func locnum(l,S) -> Element of NAT;
  coherence by ORDINAL1:def 12;
end;

theorem Th7:
  for l1, l2 being Element of NAT holds locnum(l1,T) =
  locnum(l2,T) implies l1 = l2
proof
  let l1, l2 be Element of NAT;
  assume
A1: locnum(l1,T) = locnum(l2,T);
  il.(T,locnum(l1,T)) = l1 by Def5;
  hence thesis by A1,Def5;
end;

theorem Th8:
  for N,T
  for k1, k2 being natural Number holds
  il.(T,k1) <= il.(T,k2), T iff k1 <= k2
proof let N,T;
  let k1, k2 be natural Number;
A1: k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12;
  consider f2 being sequence of NAT such that
A2: f2 is bijective & for m, n being Element of NAT holds m <= n iff f2.
  m <= f2. n, T and
A3: il.(T,k2) = f2.k2 by Def4;
  consider f1 being sequence of NAT such that
A4: f1 is bijective and
A5: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n, T and
A6: il.(T,k1) = f1.k1 by Def4;
  f1 = f2 by A4,A5,A2,Th2;
  hence thesis by A1,A5,A6,A3;
end;

theorem Th9:
  for N,T
  for l1, l2 being Element of NAT holds locnum(l1,T) <=
  locnum(l2,T) iff l1 <= l2, T
proof let N,T;
  let l1, l2 be Element of NAT;
  il.(T,locnum(l1,T)) = l1 & il.(T,locnum(l2,T)) = l2 by Def5;
  hence thesis by Th8;
end;

theorem Th10:
  for N,T holds T is InsLoc-antisymmetric
proof let N,T;
  let l1, l2 be Element of NAT;
  assume
A1: l1 <= l2, T & l2 <= l1, T;
  reconsider T as weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  reconsider l1, l2 as Element of NAT;
  locnum(l1,T) <= locnum(l2,T) & locnum(l2,T) <= locnum(l1,T) by A1,Th9;
  hence thesis by Th7,XXREAL_0:1;
end;

registration
  let N;
  cluster weakly_standard -> InsLoc-antisymmetric
   for IC-Ins-separated non
    empty with_non-empty_values AMI-Struct over N;
  coherence by Th10;
end;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, f be
  Element of NAT, k be Nat;
  func f +(k,S) -> Element of NAT equals
  il.(S,locnum(f,S) + k);
  coherence;
end;

theorem
  for f being Element of NAT holds f + (0,T) = f by Def5;

theorem
  for f, g being Element of NAT st f + (z,T) = g + (z,T)
   holds f = g
proof
  let f, g be Element of NAT;
  assume f + (z,T) = g + (z,T);
  then locnum(f,T) + z = locnum(g,T) + z by Th5;
  hence thesis by Th7;
end;

theorem
  for f being Element of NAT
   holds locnum(f,T) + z = locnum(f+(z,T),T) by Def5;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, f be
  Element of NAT;
  func NextLoc(f,S) -> Element of NAT equals
  f + (1,S);
  coherence;
end;

theorem
  for f being Element of NAT
   holds NextLoc(f,T) = il.(T,locnum(f,T)+ 1);

theorem Th15:
  for f being Element of NAT holds f <> NextLoc(f,T)
proof
  let f be Element of NAT;
  assume f = NextLoc(f,T);
  then locnum(f,T) = locnum(f,T) + 1 by Def5;
  hence thesis;
end;

theorem
  for f, g being Element of NAT st NextLoc(f,T) = NextLoc(g,T)
  holds f = g
proof
  let f, g be Element of NAT such that
A1: NextLoc(f,T) = NextLoc(g,T);
  set m = locnum(g,T);
  set k = locnum(f,T);
  k+0 = k+1-1
    .= m+1-1 by A1,Th5
    .= m+0;
  hence thesis by Th7;
end;

theorem Th17:
  il.(STC N, z) = z
proof
  set M = STC N;
  reconsider f2 = id NAT as sequence of NAT;
  consider f being sequence of NAT such that
A1: f is bijective & for m, n being Element of NAT holds m <= n iff f.m
  <= f.n, STC N and
A2: il.(M,z) = f.z by Def4;
  now
    let k be Element of NAT;
      reconsider fk = f2.k as Element of NAT;
A3: SUCC(fk,STC N) = {k,k+1} by AMISTD_1:8;
    thus f2.(k+1) in SUCC(f2.k,STC N) by A3,TARSKI:def 2;
    let j be Element of NAT;
    assume f2.j in SUCC(f2.k,STC N);
    then j = k or j = k+1 by A3,TARSKI:def 2;
    hence k <= j by NAT_1:11;
  end;
  then for m, n being Element of NAT holds m <= n iff f2.m <= f2.n, M by Th3;
  then z is Element of NAT & f = f2 by A1,Th2,ORDINAL1:def 12;
  hence thesis by A2;
end;

theorem
  for i being Instruction of STC N, s being State of STC N st InsCode i
  = 1 holds IC Exec(i,s) = NextLoc(IC s,STC N)
proof
  let i be Instruction of STC N, s be State of STC N;
  set M = STC N;
  set k = locnum(IC s,STC N);
  reconsider K = IC s as Element of NAT;
  assume InsCode i = 1;
  then
A1: IC Exec(i,s) = IC s + 1 by Lm2
    .= K+1;
  il.(M,k) = k & il.(M,k+1) = k+1 by Th17;
  hence thesis by A1,Def5;
end;

theorem
  for l being Element of NAT, i being Element of the
  InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {NextLoc(l,STC N)}
proof
  let l be Element of NAT, i be Element of the InstructionsF of
  STC N;
  assume
A1: InsCode i = 1;
  set M = STC N;
  consider k being Nat such that
A2: l = il.(M,k) by Th6;
  k = locnum(l,M) by A2,Def5;
  then NextLoc(l,STC N) = k+1 by Th17;
  hence thesis by A1,A2,Lm3,Th17;
end;

theorem
  for l being Element of NAT holds SUCC(l,STC N) = {l, NextLoc(l,STC N)}
proof
  let l be Element of NAT;
  set M = STC N;
  consider k being Nat such that
A1: l = il.(M,k) by Th6;
A2: k = locnum(l,M) by A1,Def5;
  thus SUCC(l,STC N) = {k,k+1} by A1,Th17,AMISTD_1:8
    .= {k,il.(M,k+1)} by Th17
    .= {l, NextLoc(l,STC N)} by A1,A2,Th17;
end;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, i be Instruction of
  S;
  attr i is sequential means
  for s being State of S holds Exec(i, s).IC S = NextLoc(IC s,S);
end;

theorem Th21:
  for S being weakly_standard IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N, il being Element of NAT,
  i being Instruction of S st i is sequential holds NIC(i,il)
   = {NextLoc(il,S)}
proof
  let S be weakly_standard IC-Ins-separated
   non empty
  with_non-empty_values AMI-Struct over N, il be Element of NAT, i be
  Instruction of S such that
A1: for s being State of S holds Exec(i, s).IC S = NextLoc(IC s,S);
  now
    let x be object;
A2: now
      reconsider il1 = il as Element of Values IC S by MEMSTR_0:def 6;
      set I = i;
      set t = the  State of S,
        P = the Instruction-Sequence of S;
      assume
A3:   x = NextLoc(il,S);
      reconsider u = t+*(IC S,il1) as
       Element of product the_Values_of S by CARD_3:107;
      il in NAT;
      then
A4:     il in dom P by PARTFUN1:def 2;
A5:   (P+*(il,i))/.il = (P+*(il,i)).il by PBOOLE:143
         .= i by A4,FUNCT_7:31;
      IC S in dom t by MEMSTR_0:2;
      then
A6:   IC u = il by FUNCT_7:31;
      then IC Following(P+*(il,i),u) = NextLoc(il,S) by A1,A5;
      hence x in {IC Exec(i,ss)
       where ss is Element of product the_Values_of S
        : IC ss = il} by A3,A6,A5;
    end;
    now
      assume x in {IC Exec(i,ss)
       where ss is Element of product the_Values_of S : IC ss = il};
      then ex s being Element of product the_Values_of S
       st x = IC Exec(i,s) & IC s = il;
      hence x = NextLoc(il,S) by A1;
    end;
    hence
    x in {NextLoc(il,S)} iff x in {IC Exec(i,ss)
       where ss is Element of product the_Values_of S
     : IC ss = il } by A2,TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th22:
  for S being weakly_standard IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N,
    i being Instruction of S st i is sequential
   holds i is non halting
proof
  let S be weakly_standard IC-Ins-separated
    non empty
  with_non-empty_values AMI-Struct over N, i be Instruction of S such that
A1: i is sequential;
  set s = the State of S;
  NIC(i,IC s) = {NextLoc(IC s,S)} by A1,Th21;
  then NIC(i,IC s) <> {IC s} by Th15,ZFMISC_1:3;
  hence thesis by AMISTD_1:2;
end;

registration
  let N;
  let S be weakly_standard IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N;
  cluster sequential -> non halting for Instruction of S;
  coherence by Th22;
  cluster halting -> non sequential for Instruction of S;
  coherence;
end;

begin :: Closedness of finite partial states

definition
  let N be with_zero set;
  let S be weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  let F be NAT-defined (the InstructionsF of S)-valued Function;
  attr F is para-closed means
  for s being State of S st IC s = il.(S,0)
   for k being Element of NAT holds IC Comput(F,s,k) in dom F;
end;

theorem Th23:
  for S being weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N,
   F being NAT-defined (the InstructionsF of S)-valued
 finite Function st F is really-closed & il.(S,0) in dom F holds F is
  para-closed
by AMISTD_1:14;

theorem Th24:
  for S being weakly_standard halting IC-Ins-separated
 non empty with_non-empty_values AMI-Struct over N holds il.(S,0) .-->
  halt S qua NAT-defined (the InstructionsF of S)-valued
   finite Function is really-closed
proof
  let S be weakly_standard halting IC-Ins-separated
    non empty
  with_non-empty_values AMI-Struct over N;
  reconsider F = il.(S,0) .--> halt S as
   NAT-defined (the InstructionsF of S)-valued finite Function;
  let l be Nat;
  assume
A1: l in dom(il.(S,0) .--> halt S);
A3: l = il.(S,0) by A1,TARSKI:def 1;
  F/.l = F.l by A1,PARTFUN1:def 6
    .= halt S by A3,FUNCOP_1:72;
  hence thesis by A3,AMISTD_1:2;
end;

definition
  let N be with_zero set;
  let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
  N;
  let F be (the InstructionsF of S)-valued NAT-defined finite Function;
  attr F is lower means
  :Def10:
  for l being Element of NAT st l in
  dom F holds for m being Element of NAT st m <= l, S
   holds m in dom F;
end;

registration
  let N be with_zero set,
  S be IC-Ins-separated non
  empty with_non-empty_values AMI-Struct over N;
  cluster empty -> lower
    for finite (the InstructionsF of S)-valued NAT-defined Function;
  coherence;
end;

theorem Th25:
  for i being Element of the InstructionsF of T
   holds il.(T,0) .--> i is lower
proof
  let i be Element of the InstructionsF of T;
  set F = il.(T,0).--> i;
  let l be Element of NAT such that
A1: l in dom F;
  let m be Element of NAT such that
A2: m <= l, T;
  consider k being Nat such that
A3: m = il.(T,k) by Th6;
A4: l = il.(T,0) by A1,TARSKI:def 1;
  then 0 <= k & k <= 0 by A2,A3,Th8;
  hence thesis by A1,A4,A3,XXREAL_0:1;
end;

registration
  let N be with_zero set;
  let S be weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  cluster lower 1-element for NAT-defined
     (the InstructionsF of S)-valued finite Function;
  existence
  proof
    set i = the Instruction of S;
    take il.(S,0).--> i;
    thus thesis by Th25;
  end;
end;

theorem Th26:
  for F being lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
   holds il.(T,0) in dom F
proof
  let F be lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function;
  consider l being object such that
A1: l in dom F by XBOOLE_0:def 1;
  reconsider l as Element of NAT by A1;
  consider f being sequence of NAT such that
A2: f is bijective and
A3: for m, n being Element of NAT holds m <= n iff f.m <= f.n, T and
A4: il.(T,0) = f.0 by Def4;
  rng f = NAT by A2,FUNCT_2:def 3;
  then consider x being object such that
A5: x in dom f and
A6: l = f.x by FUNCT_1:def 3;
  reconsider x as Element of NAT by A5;
  f.0 <= f.x, T by A3;
  hence thesis by A1,A4,A6,Def10;
end;

theorem Th27:
  for P being lower
  NAT-defined (the InstructionsF of T)-valued finite Function
   holds z < card P iff il.(T,z) in dom P
proof
  let P be lower NAT-defined (the InstructionsF of T)-valued finite Function;
  deffunc F(Element of NAT) = il.(T,$1);
  defpred P[Element of NAT] means F($1) in dom P;
  set A = { k : P[k]};
A1: A is Subset of NAT from DOMAIN_1:sch 7;
A2: now
    let a, b be Nat;
    assume a in A;
    then
A3: ex l being Element of NAT st l = a & il.(T,l) in dom P;
A4: b in NAT by ORDINAL1:def 12;
    assume b < a;
    then il.(T,b) <= il.(T,a), T by Th8;
    then il.(T,b) in dom P by A3,Def10;
    hence b in A by A4;
  end;
A5: now
    let x be set;
    assume x in dom P;
    then reconsider l=x as Element of NAT;
    consider n being Nat such that
A6: l = il.(T,n) by Th6;
    reconsider n as Element of NAT by ORDINAL1:def 12;
    take n;
    thus x = F(n) by A6;
  end;
  reconsider A as Cardinal by A1,A2,FUNCT_7:20;
  set A1 = {k : F(k) in dom P};
A7: z is Element of NAT by ORDINAL1:def 12;
A8: for k1, k2 being Element of NAT st F(k1) = F(k2) holds k1 = k2 by Th5;
A9: dom P, A1 are_equipotent from FUNCT_7:sch 3(A5,A8);
  hereby
    assume z < card P;
    then card Segm z in card Segm card P by NAT_1:41;
    then z in card dom P by CARD_1:62;
    then z in card A by A9,CARD_1:5;
    then ex d being Element of NAT st d = z & il.(T,d) in dom P;
    hence il.(T,z) in dom P;
  end;
  assume il.(T,z) in dom P;
  then z in card A by A7;
  then z in card dom P by A9,CARD_1:5;
  then card Segm z in card Segm card P by CARD_1:62;
  hence thesis by NAT_1:41;
end;

definition
  let N be with_zero set;
  let S be weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  let F be non empty
   NAT-defined (the InstructionsF of S)-valued finite Function;
  func LastLoc F -> Element of NAT means
  :Def11:
  ex M being finite non empty natural-membered set
   st M = { locnum(l,S) where l is
  Element of NAT : l in dom F } & it = il.(S, max M);
  existence
  proof
    deffunc F(Element of NAT) = locnum($1,S);
    set M = { F(l) where l is Element of NAT : l in dom F };
    set l = the Element of dom F;
    reconsider l as Element of NAT;
A1: locnum(l,S) in M;
A2: M c= NAT
    proof
      let k be object;
      assume k in M;
      then
      ex l being Element of NAT st k = locnum(l,S) & l in dom F;
      hence thesis;
    end;
A3: dom F is finite;
    M is finite from FRAENKEL:sch 21(A3);
    then reconsider M as finite non empty Subset of NAT by A1,A2;
    take il.(S, max M), M;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th28:
  for F being non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
   holds LastLoc F in dom F
proof
  let F be non empty
    NAT-defined (the InstructionsF of T)-valued finite Function;
  consider M being finite non empty natural-membered set such that
A1: M = { locnum(l,T) where l is Element of NAT : l in dom F } and
A2: LastLoc F = il.(T, max M) by Def11;
  max M in M by XXREAL_2:def 8;
  then
  ex l being Element of NAT st max M = locnum(l,T) & l in dom F
  by A1;
  hence thesis by A2,Def5;
end;

theorem
  for F, G being non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
    st F c= G
  holds LastLoc F <= LastLoc G, T
proof
  let F, G be non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
  such that
A1: F c= G;
  consider N being finite non empty natural-membered set such that
A2: N = { locnum(l,T) where l is Element of NAT : l in dom G } and
A3: LastLoc G = il.(T, max N) by Def11;
  consider M being finite non empty natural-membered set such that
A4: M = { locnum(l,T) where l is Element of NAT : l in dom F } and
A5: LastLoc F = il.(T, max M) by Def11;
  reconsider MM = M, NN = N as non empty finite Subset of REAL by MEMBERED:3;
  M c= N
  proof
    let a be object;
    assume a in M;
    then
A6: ex l being Element of NAT st a = locnum(l,T) & l in dom F by A4;
    dom F c= dom G by A1,GRFUNC_1:2;
    hence thesis by A2,A6;
  end;
  then max MM <= max NN by XXREAL_2:59;
  hence thesis by A5,A3,Th8;
end;

theorem Th30:
  for F being non empty
  NAT-defined (the InstructionsF of T)-valued finite Function,
      l being
  Element of NAT st l in dom F holds l <= LastLoc F, T
proof
  let F be non empty
  NAT-defined (the InstructionsF of T)-valued finite Function,
  l be Element of NAT
   such that
A1: l in dom F;
  consider M being finite non empty natural-membered set such that
A2: M = { locnum(w,T) where w is Element of NAT : w in dom F } and
A3: LastLoc F = il.(T, max M) by Def11;
  locnum(l,T) in M by A1,A2;
  then
A4: locnum(l,T) <= max M by XXREAL_2:def 8;
  max M is Nat by TARSKI:1;
  then locnum(LastLoc F,T) = max M by A3,Def5;
  hence thesis by A4,Th9;
end;

theorem
  for F being lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function,
  G being non empty NAT-defined
   NAT-defined (the InstructionsF of T)-valued finite Function
    holds F c= G & LastLoc F = LastLoc G
  implies F = G
proof
  let F be lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function,
     G be non empty
     NAT-defined (the InstructionsF of T)-valued finite Function
      such that
A1: F c= G and
A2: LastLoc F = LastLoc G;
  dom F = dom G
  proof
    thus dom F c= dom G by A1,GRFUNC_1:2;
    let x be object;
    assume
A3: x in dom G;
    reconsider x as Element of NAT by A3;
A4: LastLoc F in dom F by Th28;
    x <= LastLoc F, T by A2,A3,Th30;
    hence thesis by A4,Def10;
  end;
  hence thesis by A1,GRFUNC_1:3;
end;

theorem Th32:
  for F being lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
  holds LastLoc F = il.(T, card F -' 1)
proof
  let F be lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function;
  consider k being Nat such that
A1: LastLoc F = il.(T,k) by Th6;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  LastLoc F in dom F by Th28;
  then k < card F by A1,Th27;
  then
A2: k <= card F -' 1 by NAT_D:49;
  per cases by A2,XXREAL_0:1;
  suppose
    k < card F -' 1;
    then k+1 < card F -' 1 + 1 by XREAL_1:6;
    then k+1 < card F by NAT_1:14,XREAL_1:235;
    then il.(T,k+1) in dom F by Th27;
    then il.(T,k+1) <= LastLoc F, T by Th30;
    then
A3: k+1 <= k by A1,Th8;
    k <= k+1 by NAT_1:11;
    then k+0 = k+1 by A3,XXREAL_0:1;
    hence thesis;
  end;
  suppose
    k = card F -' 1;
    hence thesis by A1;
  end;
end;

registration
  let N be with_zero set,
  S be weakly_standard
  IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
  cluster really-closed lower non empty -> para-closed for NAT-defined
    (the InstructionsF of S)-valued finite Function;
  coherence
  by Th26,Th23;
end;

Lm4: now
  let N;
  let S be weakly_standard halting IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  set F = il.(S,0) .--> halt S;
A1: card dom F = 1 by CARD_1:30;
  F is lower NAT-defined (the InstructionsF of S)-valued finite Function
      by Th25;
  then
A2: LastLoc F = il.(S,card F -' 1) by Th32
    .= il.(S,card dom F -' 1) by CARD_1:62
    .= il.(S,0) by A1,XREAL_1:232;
  hence F.(LastLoc F) = halt S by FUNCOP_1:72;
  let l be Element of NAT such that
  F.l = halt S;
  assume l in dom F;
  hence l = LastLoc F by A2,TARSKI:def 1;
end;

definition
  let N be with_zero set,
  S be weakly_standard halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F
  be non empty NAT-defined (the InstructionsF of S)-valued finite Function;
  attr F is halt-ending means
  :Def12:
  F.(LastLoc F) = halt S;
  attr F is unique-halt means
  :Def13:
  for f being Element of NAT st
  F.f = halt S & f in dom F holds f = LastLoc F;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  cluster halt-ending unique-halt trivial
   for lower non empty
    NAT-defined (the InstructionsF of S)-valued finite Function;
  existence
  proof
    reconsider F = il.(S,0) .--> halt S as lower non empty
     NAT-defined (the InstructionsF of S)-valued finite Function
    by Th25;
    take F;
    thus F.(LastLoc F) = halt S by Lm4;
    thus for f being Element of NAT st F.f = halt S & f in dom F
    holds f = LastLoc F by Lm4;
    thus thesis;
  end;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated
    non empty
  with_non-empty_values AMI-Struct over N;
  cluster trivial really-closed lower non empty
  for NAT-defined (the InstructionsF of S)-valued finite Function;
  existence
  proof
    reconsider F = il.(S,0) .--> halt S as lower non empty
     NAT-defined (the InstructionsF of S)-valued finite Function
     by Th25;
    take F;
    thus thesis by Th24;
  end;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated
    non empty
  with_non-empty_values AMI-Struct over N;
  cluster halt-ending unique-halt trivial really-closed
  for lower non empty
   NAT-defined (the InstructionsF of S)-valued finite Function;
  existence
  proof
    reconsider F = il.(S,0) .--> halt S as lower non empty
     NAT-defined (the InstructionsF of S)-valued finite Function
     by Th25;
    take F;
    thus F.(LastLoc F) = halt S by Lm4;
    thus for f being Element of NAT st F.f = halt S & f in dom F
    holds f = LastLoc F by Lm4;
    thus thesis by Th24;
  end;
end;

definition
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  mode pre-Macro of S is halt-ending unique-halt
   lower non empty
   NAT-defined (the InstructionsF of S)-valued finite Function;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N;
  cluster really-closed for pre-Macro of S;
  existence
  proof
    reconsider F = il.(S,0) .--> halt S as lower non empty
     NAT-defined (the InstructionsF of S)-valued finite Function
     by Th25;
    F.(LastLoc F) = halt S & for l being Element of NAT st F.l
    = halt S & l in dom F holds l = LastLoc F by Lm4;
    then reconsider F as pre-Macro of S by Def12,Def13;
    take F;
    thus thesis by Th24;
  end;
end;

theorem
  for N being with_zero set,
      S being IC-Ins-separated
       non empty with_non-empty_values AMI-Struct over N,
  l1, l2 being Element of NAT st SUCC(l1,S) = NAT
   holds l1 <= l2, S
proof
  let N be with_zero set,
  S be IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N, l1, l2 be Element of NAT
  such that
A1: SUCC(l1,S) = NAT;
  defpred P[set,set] means ($1 = 1 implies $2 = l1) & ($1 = 2 implies $2 = l2);
A2: for n being Nat st n in Seg 2 ex d being Element of NAT st P[n,d]
  proof
    let n be Nat;
    assume
A3: n in Seg 2;
    per cases by A3,FINSEQ_1:2,TARSKI:def 2;
    suppose
A4:   n = 1;
      reconsider l1 as Element of NAT;
      take l1;
      thus thesis by A4;
    end;
    suppose
A5:   n = 2;
      reconsider l2 as Element of NAT;
      take l2;
      thus thesis by A5;
    end;
  end;
  consider f being FinSequence of NAT such that
A6: len f = 2 and
A7: for n being Nat st n in Seg 2 holds P[n,f/.n] from FINSEQ_4:sch 1(A2);
A8: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
  then
A9: f/.1 = l1 by A7;
  reconsider f as non empty FinSequence of NAT by A6;
  take f;
  2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
  hence f/.1 = l1 & f/.len f = l2 by A6,A7,A8;
  let n be Element of NAT;
  assume
A10: 1 <= n;
  assume n < len f;
  then n < 1+1 by A6;
  then n <= 1 by NAT_1:13;
  then n = 1 by A10,XXREAL_0:1;
  hence thesis by A1,A9;
end;

:: from SCMRING4, 2008.03.13, A.T.

reserve i, j, k for Nat,
  n for Element of NAT,
  N for with_zero set,
  S for weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N,
  l for Element of NAT,
  f for FinPartState of S;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, loc be
  Element of NAT, k be Nat;
  func loc -' (k,S) -> Element of NAT equals
  il.(S, (locnum(loc,S)) -' k);
  coherence;
end;

theorem
  l -' (0,S) = l
by NAT_D:40,Def5;

theorem
  l + (k,S) -' (k,S) = l
proof
  thus l + (k,S) -' (k,S) = il.(S,locnum(l,S) + k -' k) by Def5
    .= il.(S,locnum(l,S)) by NAT_D:34
    .= l by Def5;
end;