The Mizar article:

A Tree of Execution of a Macroinstruction

by
Artur Kornilowicz

Received December 10, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: AMISTD_3
[ MML identifier index ]


environ

 vocabulary AMISTD_3, AMI_1, TREES_2, GOBOARD5, AMI_3, RELAT_1, FINSET_1,
      FUNCT_1, AMISTD_1, SQUARE_1, WAYBEL_0, BOOLE, ORDINAL1, FINSEQ_1, CARD_1,
      CARD_3, ORDINAL2, ARYTM, PARTFUN1, TREES_1, TARSKI, WELLORD1, WELLORD2,
      AMISTD_2, FRECHET, FINSEQ_2, CAT_1, FUNCOP_1, MEMBERED;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1, NUMBERS,
      ORDINAL1, ORDINAL2, MEMBERED, XREAL_0, CQC_SIM1, NAT_1, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, WELLORD1, WELLORD2, FUNCOP_1, CQC_LANG, FINSEQ_1,
      FINSEQ_2, TREES_1, TREES_2, STRUCT_0, AMI_1, AMI_3, AMI_5, AMISTD_1,
      AMISTD_2;
 constructors AMISTD_2, CQC_SIM1, WELLORD1, ORDERS_2, AMI_5, PRE_CIRC,
      POLYNOM1, WELLORD2;
 clusters AMI_1, AMISTD_1, FINSET_1, RELSET_1, TREES_2, ARYTM_3, FINSEQ_6,
      FUNCT_7, HEYTING2, NECKLACE, CARD_5, WAYBEL12, RELAT_1, FUNCOP_1,
      FINSEQ_5, SCMFSA_4, XREAL_0, CARD_1, ORDINAL1, MEMBERED, FINSEQ_1,
      PRELAMB;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, ORDINAL1, WELLORD1, WELLORD2, FUNCT_1, TREES_1;
 theorems ORDINAL2, AMI_3, CQC_SIM1, AMISTD_1, GRFUNC_1, NAT_1, ORDINAL1,
      CARD_1, TREES_2, SUBSET_1, FUNCT_2, TREES_1, FINSEQ_1, FUNCT_1, PARTFUN1,
      XBOOLE_1, RELAT_1, FINSEQ_3, FINSEQ_5, AXIOMS, TARSKI, QC_LANG4, CARD_5,
      FINSEQ_2, XBOOLE_0, AMI_5, AMISTD_2, CQC_LANG, CARD_2, WELLORD2,
      ENUMSET1, WELLORD1, ZFMISC_1, AMI_1, TOLER_1, ORDERS_2, CARD_4, FINSET_1,
      FUNCOP_1, RELSET_1, MEMBERED;
 schemes FRAENKEL, TREES_2, FUNCT_2, NAT_1, HILBERT2, ORDINAL2;

begin

:: Preliminaries

reserve x, y, X for set,
        m, n for natural number,
        O for Ordinal,
        R, S for Relation;

definition
  let D be set, f be PartFunc of D,NAT, n be set;
  cluster f.n -> natural;
coherence
proof
  per cases;
  suppose n in dom f;
  then reconsider a = f.n as Nat by PARTFUN1:27;
  a is natural;
  hence thesis;
  suppose not n in dom f;
  hence thesis by FUNCT_1:def 4;
end;
end;

definition
  let R be empty Relation, X be set;
  cluster R|X -> empty;
coherence
proof
  dom R misses X by XBOOLE_1:65;
  hence thesis by RELAT_1:95;
end;
end;

theorem Th1:
  dom R = {x} & rng R = {y} implies R = x .--> y
proof
  assume that
A1:  dom R = {x} and
A2:  rng R = {y};
   set g = x .--> y;
A3: g = {[x,y]} by AMI_1:19;
  for a, b being set holds [a,b] in R iff [a,b] in g
  proof
    let a, b be set;
    hereby
      assume [a,b] in R;
      then a in dom R & b in rng R by RELAT_1:20;
      then a = x & b = y by A1,A2,TARSKI:def 1;
      hence [a,b] in g by A3,TARSKI:def 1;
    end;
    assume [a,b] in g;
    then [a,b] = [x,y] by A3,TARSKI:def 1;
    then
A4: a = x & b = y by ZFMISC_1:33;
    then a in dom R by A1,TARSKI:def 1;
    then consider z being set such that
A5:   [a,z] in R by RELAT_1:def 4;
    z in rng R by A5,RELAT_1:20;
    hence [a,b] in R by A5,A2,A4,TARSKI:def 1;
  end;
  hence thesis by RELAT_1:def 2;
end;

theorem Th2:
  field {[x,x]} = {x}
proof
  thus field {[x,x]} = {x,x} by RELAT_1:32
    .= {x} by ENUMSET1:69;
end;

definition
  let X be infinite set, a be set;
  cluster X --> a -> infinite;
coherence
proof
  assume X --> a is finite;
  then reconsider f = X --> a as finite Relation;
  dom f is finite;
  hence thesis by FUNCOP_1:19;
end;
end;

definition
  cluster infinite Function;
existence
proof
  take NAT --> 0;
  thus thesis;
end;
end;

definition
  let R be finite Relation;
  cluster field R -> finite;
coherence
proof
   field R = dom R \/ rng R by RELAT_1:def 6;
   hence thesis;
end;
end;

theorem Th3:
  field R is finite implies R is finite
proof
  assume field R is finite;
  then reconsider A = field R as finite set;
  R c= [:A,A:] by ORDERS_2:82;
  hence thesis by FINSET_1:13;
end;

definition
  let R be infinite Relation;
  cluster field R -> infinite;
coherence by Th3;
end;

theorem
  dom R is finite & rng R is finite implies R is finite
proof
  assume dom R is finite & rng R is finite;
  then dom R \/ rng R is finite by FINSET_1:14;
  then field R is finite by RELAT_1:def 6;
  hence thesis by Th3;
end;

definition
  cluster RelIncl {} -> empty;
coherence
proof
  for Y,Z being set st Y in {} & Z in {} holds [Y,Z] in {} iff Y c= Z;
  hence thesis by TOLER_1:1,WELLORD2:def 1;
end;
end;

definition
  let X be non empty set;
  cluster RelIncl X -> non empty;
coherence
proof
  consider a being Element of X;
  [a,a] in RelIncl X by WELLORD2:def 1;
  hence thesis;
end;
end;

theorem Th5:
  RelIncl {x} = {[x,x]}
proof
A1: field {[x,x]} = {x} by Th2;
  for Y,Z being set st Y in {x} & Z in {x} holds [Y,Z] in {[x,x]} iff Y c= Z
  proof
    let Y,Z be set;
    assume Y in {x} & Z in {x};
    then
A2: Y = x & Z = x by TARSKI:def 1;
    hence [Y,Z] in {[x,x]} implies Y c= Z;
    thus thesis by A2,TARSKI:def 1;
  end;
  hence thesis by A1,WELLORD2:def 1;
end;

theorem Th6:
  RelIncl X c= [:X,X:]
proof
  set R = RelIncl X;
  let x be set;
  assume
A1: x in R;
  then consider a, b being set such that
A2: x = [a,b] by RELAT_1:def 1;
  a in field R & b in field R by A1,A2,RELAT_1:30;
  then a in X & b in X by WELLORD2:def 1;
  hence thesis by A2,ZFMISC_1:106;
end;

definition
  let X be finite set;
  cluster RelIncl X -> finite;
coherence
proof
  RelIncl X c= [:X,X:] by Th6;
  hence thesis by FINSET_1:13;
end;
end;

theorem Th7:
  RelIncl X is finite implies X is finite
proof
  set R = RelIncl X;
  assume R is finite;
  then reconsider A = R as finite Relation;
  field A is finite;
  hence thesis by WELLORD2:def 1;
end;

definition
  let X be infinite set;
  cluster RelIncl X -> infinite;
coherence by Th7;
end;

theorem
  R,S are_isomorphic & R is well-ordering implies S is well-ordering
proof
  assume R,S are_isomorphic;
  then ex F being Function st F is_isomorphism_of R,S by WELLORD1:def 8;
  hence thesis by WELLORD1:54;
end;

theorem Th9:
  R,S are_isomorphic & R is finite implies S is finite
proof
  given F being Function such that
A1: F is_isomorphism_of R,S;
  assume R is finite;
  then reconsider R as finite Relation;
  field R is finite;
  then dom F is finite by A1,WELLORD1:def 7;
  then rng F is finite by FINSET_1:26;
  then field S is finite by A1,WELLORD1:def 7;
  hence S is finite by Th3;
end;

theorem Th10:
  x .--> y is_isomorphism_of {[x,x]},{[y,y]}
proof
  set F = x .--> y;
  set R = {[x,x]};
  set S = {[y,y]};
A1: field R = {x} by Th2;
  hence dom F = field R by CQC_LANG:5;
  field S = {y} by Th2;
  hence rng F = field S by CQC_LANG:5;
  thus F is one-to-one;
  let a,b be set;
  hereby
    assume [a,b] in R;
    then [a,b] = [x,x] by TARSKI:def 1;
    then
A2: a = x & b = x by ZFMISC_1:33;
    hence a in field R & b in field R by A1,TARSKI:def 1;
    F.x = y by CQC_LANG:6;
    hence [F.a,F.b] in S by A2,TARSKI:def 1;
  end;
  assume a in field R & b in field R;
  then a = x & b = x by A1,TARSKI:def 1;
  hence thesis by TARSKI:def 1;
end;

theorem
  {[x,x]}, {[y,y]} are_isomorphic
proof
  take f = x .--> y;
  thus f is_isomorphism_of {[x,x]},{[y,y]} by Th10;
end;

definition
  cluster order_type_of {} -> empty;
coherence
proof
  {},RelIncl {} are_isomorphic by WELLORD1:48;
  hence thesis by ORDERS_2:21,WELLORD2:def 2;
end;
end;

theorem
  order_type_of RelIncl O = O
proof
A1: RelIncl O is well-ordering by WELLORD2:7;
  RelIncl O,RelIncl O are_isomorphic by WELLORD1:48;
  hence thesis by A1,WELLORD2:def 2;
end;

Lm1:
  for X being finite set st X c= O holds order_type_of RelIncl X is finite
proof
  let X be finite set;
  assume X c= O;
  then RelIncl X is well-ordering by WELLORD2:9;
  then
  RelIncl X,RelIncl order_type_of RelIncl X are_isomorphic by WELLORD2:def 2;
  then RelIncl order_type_of RelIncl X is finite by Th9;
  hence thesis by Th7;
end;

theorem Th13:
  for X being finite set st X c= O holds order_type_of RelIncl X = card X
proof
  let X be finite set;
  assume
A1: X c= O;
  then
A2: card X = Card order_type_of RelIncl X by CARD_5:16;
  order_type_of RelIncl X is finite by A1,Lm1;
  then order_type_of RelIncl X in omega by CARD_4:7;
  hence thesis by A2,CARD_1:66;
end;

theorem Th14:
  {x} c= O implies order_type_of RelIncl {x} = 1
proof
  card {x} = 1 by CARD_2:60;
  hence thesis by Th13;
end;

theorem Th15:
  {x} c= O implies
  canonical_isomorphism_of (RelIncl order_type_of RelIncl {x}, RelIncl {x})
    = 0 .--> x
proof
  set X = {x};
  set R = RelIncl X;
  set C = canonical_isomorphism_of (RelIncl order_type_of R,R);
  assume
A1: X c= O;
  then R is well-ordering by WELLORD2:9;
  then R, RelIncl order_type_of R are_isomorphic by WELLORD2:def 2;
  then
A2:RelIncl order_type_of R, R are_isomorphic by WELLORD1:50;
  RelIncl order_type_of R is well-ordering by WELLORD2:9;
  then
A3:C is_isomorphism_of RelIncl order_type_of R, R by A2,WELLORD1:def 9;
A4:RelIncl {0} = {[0,0]} by Th5;
A5:order_type_of R = {0} by A1,Th14,CARD_5:1;
  then
A6:dom canonical_isomorphism_of(RelIncl {0}, R) = field RelIncl {0}
    by A3,WELLORD1:def 7
    .= {0} by A4,Th2;
  rng canonical_isomorphism_of(RelIncl {0}, R) = field R
    by A5,A3,WELLORD1:def 7
    .= X by WELLORD2:def 1;
  hence thesis by A5,A6,Th1;
end;

definition
  let O be Ordinal,
      X be Subset of O,
      n be set;
  cluster canonical_isomorphism_of
              (RelIncl order_type_of RelIncl X,RelIncl X).n
          -> ordinal;
coherence
proof
  consider phi being Ordinal-Sequence such that
A1:phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X, RelIncl X) &
   phi is increasing & dom phi = order_type_of RelIncl X and
A2:rng phi = X by CARD_5:14;
  per cases;
  suppose n in dom phi;
  then phi.n in rng phi by FUNCT_1:def 5;
  hence thesis by A1,A2,ORDINAL1:23;
  suppose not n in dom phi;
  hence thesis by A1,FUNCT_1:def 4;
end;
end;

definition
  let X be natural-membered set,
      n be set;
  cluster canonical_isomorphism_of
              (RelIncl order_type_of RelIncl X,RelIncl X).n
          -> natural;
coherence
proof
  X c= NAT
  proof
    let x be set;
    assume x in X;
    then x is natural by MEMBERED:def 5;
    hence thesis by ORDINAL2:def 21;
  end;
  then reconsider X as Subset of NAT;
  consider phi being Ordinal-Sequence such that
A1:phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X, RelIncl X) &
   phi is increasing & dom phi = order_type_of RelIncl X and
A2:rng phi = X by CARD_5:14;
  per cases;
  suppose
A3: n in dom phi;
  then
A4:phi.n in rng phi by FUNCT_1:def 5;
  reconsider a = phi.n as Element of X by A2,A3,FUNCT_1:def 5;
  a is Nat by A2,A4;
  hence thesis by A1;
  suppose not n in dom phi;
  hence thesis by A1,FUNCT_1:def 4;
end;
end;

:: Trees

theorem Th16:
  n |-> x = m |-> x implies n = m
proof
  len(n |-> x) = n & len(m |-> x) = m by FINSEQ_2:69;
  hence thesis;
end;

theorem Th17:
  for T being Tree, t being Element of T holds t|Seg n in T
proof
  let T be Tree,
      t be Element of T;
  t|Seg n is_a_prefix_of t by RELAT_1:88;
  hence thesis by TREES_1:45;
end;

theorem Th18:
  for T1, T2 being Tree st
    for n being Nat holds T1-level n = T2-level n holds
  T1 = T2
proof
  let T1, T2 be Tree such that
A1: for n being Nat holds T1-level n = T2-level n;
  for p being FinSequence of NAT holds p in T1 iff p in T2
  proof
    let p be FinSequence of NAT;
A2: T1 = union { T1-level n where n is Nat: not contradiction } by TREES_2:16;
A3: T2 = union { T2-level n where n is Nat: not contradiction } by TREES_2:16;
    hereby
      assume p in T1;
      then consider Y being set such that
A4:     p in Y and
A5:     Y in { T1-level n where n is Nat: not contradiction }
          by A2,TARSKI:def 4;
      consider n being Nat such that
A6:     Y = T1-level n by A5;
      Y = T2-level n by A1,A6;
      hence p in T2 by A4;
    end;
    assume p in T2;
    then consider Y being set such that
A7:   p in Y and
A8:   Y in { T2-level n where n is Nat: not contradiction }
        by A3,TARSKI:def 4;
    consider n being Nat such that
A9:   Y = T2-level n by A8;
    Y = T1-level n by A1,A9;
    hence p in T1 by A7;
  end;
  hence T1 = T2 by TREES_2:7;
end;

definition
  func TrivialInfiniteTree equals :Def1:
  { k |-> 0 where k is Nat: not contradiction };
coherence;
end;

definition
  cluster TrivialInfiniteTree -> non empty Tree-like;
coherence
proof
  set X = TrivialInfiniteTree;
  0 |-> 0 in X by Def1;
  hence X is non empty;
  thus X c= NAT*
  proof
    let x be set;
    assume x in X;
    then ex k being Nat st x = k |-> 0 by Def1;
    then x is FinSequence of NAT by FINSEQ_2:77;
    hence thesis by FINSEQ_1:def 11;
  end;
  thus for p being FinSequence of NAT st p in X holds ProperPrefixes p c= X
  proof
    let p be FinSequence of NAT;
    assume p in X;
    then consider m being Nat such that
A1:   p = m |-> 0 by Def1;
    let x be set;
    assume
A2:   x in ProperPrefixes p;
    then reconsider x as FinSequence by TREES_1:35;
A3: len x = len (len x |-> 0) by FINSEQ_2:69;
    for k being Nat st 1 <= k & k <= len x holds x.k = (len x |-> 0).k
    proof
      let k be Nat;
      assume 1 <= k & k <= len x;
      then
A4:   k in dom x by FINSEQ_3:27;
      then
A5:   k in Seg len x by FINSEQ_1:def 3;
      len x < len p by A2,TREES_1:37;
      then Seg len x c= Seg len p by FINSEQ_1:7;
      then k in Seg len p by A5;
      then
A6:   k in Seg m by A1,FINSEQ_2:69;
      x is_a_proper_prefix_of p by A2,TREES_1:36;
      then
A7:   x c= p by XBOOLE_0:def 8;
      thus (len x |-> 0).k = 0 by A5,FINSEQ_2:70
         .= p.k by A1,A6,FINSEQ_2:70
         .= x.k by A4,A7,GRFUNC_1:8;
    end;
    then x = len x |-> 0 by A3,FINSEQ_1:18;
    hence thesis by Def1;
  end;
  let p be FinSequence of NAT,
      m, n be Nat;
  assume p^<*m*> in X;
  then consider k being Nat such that
A8: p^<*m*> = k |-> 0 by Def1;
  assume
A9:  n <= m;
A10: len (p^<*m*>) = len p + 1 by FINSEQ_2:19;
A11: len (p^<*m*>) = k by A8,FINSEQ_2:69;
A12: (p^<*m*>).len (p^<*m*>) = m by A10,FINSEQ_1:59;
  0 = k or 0 < k by NAT_1:18;
  then 0+1 <= k by A8,NAT_1:38,FINSEQ_2:72;
  then k in Seg k by FINSEQ_1:3;
  then
A13: m = 0 by A12,A8,A11,FINSEQ_2:70;
A14: len (p^<*n*>) = len (len (p^<*n*>) |-> 0) by FINSEQ_2:69;
  for z being Nat st 1 <= z & z <= len (p^<*n*>) holds
    (len (p^<*n*>) |-> 0).z = (p^<*n*>).z
  proof
    let z be Nat;
    assume that
A15:   1 <= z and
A16:   z <= len (p^<*n*>);
    z in dom (p^<*n*>) by A15,A16,FINSEQ_3:27;
    then
A17: z in Seg len (p^<*n*>) by FINSEQ_1:def 3;
    len (p^<*n*>) = len p + 1 by FINSEQ_2:19;
    then
A18: z in Seg k by A15,A16,A11,A10,FINSEQ_1:3;
    thus (len (p^<*n*>) |-> 0).z = 0 by A17,FINSEQ_2:70
      .= (p^<*m*>).z by A8,A18,FINSEQ_2:70
      .= (p^<*n*>).z by A13,A9,NAT_1:19;
  end;
  then len (p^<*n*>) |-> 0 = p^<*n*> by A14,FINSEQ_1:18;
  hence p^<*n*> in X by Def1;
end;
end;

theorem Th19:
  NAT,TrivialInfiniteTree are_equipotent
proof
  defpred P[Nat,set] means $2 = $1 |-> 0;
A1: for x being Element of NAT
     ex y being Element of TrivialInfiniteTree st P[x,y]
  proof
    let x be Element of NAT;
    x |-> 0 in TrivialInfiniteTree by Def1;
    then reconsider y = x |-> 0 as Element of TrivialInfiniteTree;
    take y;
    thus thesis;
  end;
  consider f being Function of NAT,TrivialInfiniteTree such that
A2:   for x being Element of NAT holds P[x,f.x] from FuncExD(A1);
  take f;
  thus f is one-to-one
  proof
    let x,y be set;
    assume
A3:   x in dom f & y in dom f;
    assume
A4:   f.x = f.y;
    reconsider x, y as Nat by A3,FUNCT_2:def 1;
    P[x,f.x] & P[y,f.y] by A2;
    hence thesis by A4,Th16;
  end;
  thus
A5: dom f = NAT by FUNCT_2:def 1;
  thus rng f c= TrivialInfiniteTree by RELSET_1:12;
  let a be set;
  assume a in TrivialInfiniteTree;
  then consider k being Nat such that
A6:  a = k |-> 0 by Def1;
  k in dom f & f.k = a by A2,A6,A5;
  hence thesis by FUNCT_1:def 5;
end;

definition
  cluster TrivialInfiniteTree -> infinite;
coherence by Th19,CARD_1:68;
end;

theorem Th20:
  for n being Nat holds TrivialInfiniteTree-level n = { n |-> 0 }
proof
  let n be Nat;
  set T = TrivialInfiniteTree;
  set L = { w where w is Element of T: len w = n };
  set f = n |-> 0;
  {f} = L
  proof
    hereby
      let a be set;
      assume a in {f};
      then
A1:   a = f by TARSKI:def 1;
A2:   f in T by Def1;
      len f = n by FINSEQ_2:69;
      hence a in L by A1,A2;
    end;
    let a be set;
    assume a in L;
    then consider w being Element of T such that
A3:   a = w & len w = n;
    w in T;
    then ex k being Nat st w = k |-> 0 by Def1;
    then a = f by A3,FINSEQ_2:69;
    hence a in {f} by TARSKI:def 1;
  end;
  hence thesis by TREES_2:def 6;
end;

:: First Location

reserve
  N for with_non-empty_elements set,
  S for standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over N)),
  L, l1 for Instruction-Location of S,
  J for Instruction of S,
  F for Subset of the Instruction-Locations of S;

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 FinPartState of S such that
A1:   F is non empty and
A2:   F is programmed;
  func FirstLoc F -> Instruction-Location of S means :Def2:
  ex M being non empty Subset of NAT st
     M = { locnum l where l is Element of the Instruction-Locations of S
                        : l in dom F } &
     it = il.(S, min M);
existence
proof
  deffunc G(Element of the Instruction-Locations of S) = locnum $1;
  reconsider F as non empty programmed FinPartState of S by A1,A2;
  set M = { G(l) where l is Element of the Instruction-Locations of S
          : l in dom F };
A3: dom F is finite;
A4: M is finite from FraenkelFin(A3);
    consider l being Element of dom F;
    l in dom F & dom F c= the Instruction-Locations of S by AMI_3:def 13;
    then reconsider l as Element of the Instruction-Locations of S;
A5: locnum l in M;
    M c= NAT
    proof
      let k be set;
      assume k in M;
      then ex l being Element of the Instruction-Locations of S st
        k = locnum l & l in dom F;
      hence k in NAT;
    end;
  then reconsider M as finite non empty Subset of NAT by A4,A5;
  take il.(S, min M), M;
  thus thesis;
end;
uniqueness;
end;

theorem Th21:
  for F being non empty programmed FinPartState of S holds
   FirstLoc F in dom F
proof
    let F be non empty programmed FinPartState of S;
    consider M being non empty Subset of NAT such that
A1:    M = { locnum l where l is Element of the Instruction-Locations of S
                          : l in dom F } and
A2:    FirstLoc F = il.(S,min M) by Def2;
    min M in M by CQC_SIM1:def 8;
    then ex l being Element of the Instruction-Locations of S st
      min M = locnum l & l in dom F by A1;
    hence FirstLoc F in dom F by A2,AMISTD_1:def 13;
  end;

theorem
  for F, G being non empty programmed FinPartState of S st F c= G holds
   FirstLoc G <= FirstLoc F
proof
    let F, G be non empty programmed FinPartState of S such that
A1:   F c= G;
    consider M being non empty Subset of NAT such that
A2:    M = { locnum l where l is Element of the Instruction-Locations of S
                          : l in dom F } and
A3:    FirstLoc F = il.(S,min M) by Def2;
    consider N being non empty Subset of NAT such that
A4:    N = { locnum l where l is Element of the Instruction-Locations of S
                          : l in dom G } and
A5:    FirstLoc G = il.(S,min N) by Def2;
    M c= N
    proof
      let a be set;
      assume a in M;
      then
A6:   ex l being Element of the Instruction-Locations of S st
       a = locnum l & l in dom F by A2;
      dom F c= dom G by A1,GRFUNC_1:8;
      hence a in N by A4,A6;
    end;
    then min N <= min M by CQC_SIM1:19;
    hence thesis by A3,A5,AMISTD_1:28;
  end;

theorem Th23:
  for F being non empty programmed FinPartState of S st l1 in dom F holds
   FirstLoc F <= l1
proof
    let F be non empty programmed FinPartState of S such that
A1:   l1 in dom F;
    consider M being non empty Subset of NAT such that
A2:    M = { locnum w where w is Element of the Instruction-Locations of S
                          : w in dom F } and
A3:    FirstLoc F = il.(S,min M) by Def2;
A4: locnum FirstLoc F = min M by A3,AMISTD_1:def 13;
    locnum l1 in M by A1,A2;
    then min M <= locnum l1 by CQC_SIM1:def 8;
    hence FirstLoc F <= l1 by A4,AMISTD_1:29;
  end;

theorem
  for F being lower non empty programmed FinPartState of S holds
   FirstLoc F = il.(S,0)
proof
    let F be lower non empty programmed FinPartState of S;
    consider M being non empty Subset of NAT such that
      M = { locnum l where l is Element of the Instruction-Locations of S
                          : l in dom F } and
A1:    FirstLoc F = il.(S,min M) by Def2;
A2: FirstLoc F in dom F by Th21;
   0 <= min M by NAT_1:18;
   then
A3:il.(S,0) <= il.(S,min M) by AMISTD_1:28;
   then il.(S,0) in dom F by A2,A1,AMISTD_1:def 20;
   then FirstLoc F <= il.(S,0) by Th23;
   hence thesis by A3,A1,AMISTD_1:def 9;
  end;

:: LocNums

definition
 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 Subset of the Instruction-Locations of S;
 func LocNums F -> Subset of NAT equals :Def3:
  {locnum l where l is Instruction-Location of S : l in F};
coherence
proof
  set A = {locnum l where l is Instruction-Location of S : l in F};
  A c= NAT
  proof
    let a be set;
    assume a in A;
    then ex l being Instruction-Location of S st a = locnum l & l in F;
    hence thesis;
  end;
  hence thesis;
end;
end;

theorem Th25:
  locnum l1 in LocNums F iff l1 in F
proof
A1:LocNums F =
  {locnum l where l is Instruction-Location of S : l in F} by Def3;
  hereby
    assume locnum l1 in LocNums F;
    then ex l being Instruction-Location of S st locnum l1 = locnum l &
      l in F by A1;
    hence l1 in F by AMISTD_1:27;
  end;
  thus thesis by A1;
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)),
     F be empty Subset of the Instruction-Locations of S;
 cluster LocNums F -> empty;
coherence
proof
A1:LocNums F =
  {locnum l where l is Instruction-Location of S : l in F} by Def3;
  assume LocNums F is non empty;
  then consider x being set such that
A2:  x in LocNums F by XBOOLE_0:def 1;
  ex l being Instruction-Location of S st x = locnum l & l in F by A1,A2;
  hence thesis;
end;
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)),
     F be non empty Subset of the Instruction-Locations of S;
 cluster LocNums F -> non empty;
coherence
proof
  ex l being Instruction-Location of S st l in F by SUBSET_1:10;
  hence thesis by Th25;
end;
end;

theorem Th26:
  F = {il.(S,n)} implies LocNums F = {n}
proof
  assume
A1: F = {il.(S,n)};
A2: il.(S,n) in {il.(S,n)} by TARSKI:def 1;
A3: locnum il.(S,n) = n by AMISTD_1:def 13;
A4: LocNums F = {locnum l where l is Instruction-Location of S : l in F}
     by Def3;
  hereby
    let x be set;
    assume x in LocNums F;
    then consider l being Instruction-Location of S such that
A5:   x = locnum l and
A6:   l in F by A4;
    l = il.(S,n) by A1,A6,TARSKI:def 1;
    then x = n by A5,AMISTD_1:def 13;
    hence x in {n} by TARSKI:def 1;
  end;
  let x be set;
  assume x in {n};
  then x = n by TARSKI:def 1;
  hence thesis by A1,A2,A3,Th25;
end;

theorem Th27:
  F, LocNums F are_equipotent
proof
A1:LocNums F = {locnum l where l is Instruction-Location of S : l in F}
   by Def3;
  per cases;
  suppose F is empty;
  then reconsider F as empty Subset of the Instruction-Locations of S;
  LocNums F is empty;
  hence thesis;
  suppose
A2: F is non empty;
  LocNums F,F are_equipotent
  proof
  defpred P[Nat,set] means $2 = il.(S,$1);
A3: for x being set st x in LocNums F ex y being set st y in F & P[x,y]
  proof
    let x be set;
    assume x in LocNums F;
    then consider l being Instruction-Location of S such that
A4:    x = locnum l & l in F by A1;
    take l;
    thus thesis by A4,AMISTD_1:def 13;
  end;
  consider f being Function of LocNums F,F such that
A5:   for x being set st x in LocNums F holds P[x,f.x] from FuncEx1(A3);
  take f;
  thus f is one-to-one
  proof
    let x,y be set;
    assume that
A6:   x in dom f and
A7:   y in dom f and
A8:   f.x = f.y;
A9: dom f = LocNums F by A2,FUNCT_2:def 1;
    then
A10: ex l1 being Instruction-Location of S st x = locnum l1 & l1 in F by A6,A1;
A11: ex l2 being Instruction-Location of S st y = locnum l2 & l2 in F
     by A7,A1,A9;
    P[x,f.x] & P[y,f.y] by A5,A6,A7,A9;
    hence thesis by A8,A10,A11,AMISTD_1:25;
  end;
  thus
A12: dom f = LocNums F by A2,FUNCT_2:def 1;
  thus rng f c= F by RELSET_1:12;
  let a be set;
  assume
A13: a in F;
  then reconsider l = a as Instruction-Location of S;
A14:locnum l in dom f by A12,A13,A1;
  then P[locnum l,f.locnum l] by A5,A12;
  then f.locnum l = a by AMISTD_1:def 13;
  hence thesis by A14,FUNCT_1:def 5;
  end;
  hence thesis;
end;

theorem Th28:
  Card F c= order_type_of RelIncl LocNums F
proof
  set X = LocNums F;
A1: Card X = Card order_type_of RelIncl X by CARD_5:16;
  F,X are_equipotent by Th27;
  then Card F = Card X by CARD_1:21;
  hence thesis by A1,CARD_1:24;
end;

theorem Th29:
  S is realistic & J is halting implies LocNums NIC(J,L) = {locnum L}
proof
  assume S is realistic & J is halting;
  then NIC(J,L) = {L} by AMISTD_1:15
               .= {il.(S,locnum L)} by AMISTD_1:def 13;
  hence thesis by Th26;
end;

theorem
  S is realistic & J is sequential implies
   LocNums NIC(J,L) = {locnum NextLoc L}
proof
  assume S is realistic & J is sequential;
  then NIC(J,L) = {NextLoc L} by AMISTD_1:41
            .= {il.(S,locnum NextLoc L)} by AMISTD_1:def 13;
  hence thesis by Th26;
end;

:: LocSeq

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be Subset of the Instruction-Locations of S;
  deffunc F(set) = il.(S, canonical_isomorphism_of
        (RelIncl order_type_of RelIncl LocNums M,RelIncl LocNums M).$1);
  set Z = the Instruction-Locations of S;
  func LocSeq M -> T-Sequence of the Instruction-Locations of S means :Def4:
   dom it = Card M &
   for m being set st m in Card M holds
    it.m = il.(S, canonical_isomorphism_of
                  (RelIncl order_type_of RelIncl LocNums M,
                   RelIncl LocNums M).m);
existence
proof
  consider f being T-Sequence such that
A1:  dom f = Card M and
A2:  for A being Ordinal st A in Card M holds f.A = F(A) from TS_Lambda;
  take f;
  thus f is T-Sequence of Z
  proof
    let y be set;
    assume y in rng f;
    then consider x being set such that
A3:  x in dom f and
A4:  y = f.x by FUNCT_1:def 5;
    x is Ordinal by A3,ORDINAL1:23;
    then f.x = F(x) by A1,A2,A3;
    hence y in Z by A4;
  end;
  thus dom f = Card M by A1;
  let m be set;
  assume
A5: m in Card M;
  then m is Ordinal by ORDINAL1:23;
  hence thesis by A2,A5;
end;
uniqueness
proof
  let f, g be T-Sequence of Z such that
A6: dom f = Card M and
A7: for m being set st m in Card M holds f.m = F(m) and
A8: dom g = Card M and
A9: for m being set st m in Card M holds g.m = F(m);
  for x being set st x in dom f holds f.x = g.x
  proof
    let x be set such that
A10:   x in dom f;
    thus f.x = F(x) by A6,A7,A10
      .= g.x by A6,A9,A10;
  end;
  hence thesis by A6,A8,FUNCT_1:9;
end;
end;

theorem
  F = {il.(S,n)} implies LocSeq F = 0 .--> il.(S,n)
proof
  assume
A1: F = {il.(S,n)};
  then
A2:LocNums F = {n} by Th26;
  {n} c= omega
  proof
    let a be set;
    assume a in {n};
    then a = n by TARSKI:def 1;
    hence thesis by ORDINAL2:def 21;
  end;
  then
A3:canonical_isomorphism_of(RelIncl order_type_of RelIncl {n}, RelIncl {n}).0
   = (0 .--> n).0 by Th15
  .= n by CQC_LANG:6;
A4: dom LocSeq F = Card F by Def4;
A5: Card F = {0} by A1,CARD_1:50,CARD_2:20,CARD_5:1;
A6: dom (0 .--> il.(S,n)) = {0} by CQC_LANG:5;
  for a being set st a in dom LocSeq F holds (LocSeq F).a = (0 .--> il.(S,n)).a
  proof
    let a be set;
    assume
A7:   a in dom LocSeq F;
    then
A8: a = 0 by A4,A5,TARSKI:def 1;
    thus (LocSeq F).a = il.(S, canonical_isomorphism_of
                  (RelIncl order_type_of RelIncl LocNums F,
                   RelIncl LocNums F).a) by A4,A7,Def4
       .= (0 .--> il.(S,n)).a by A8,CQC_LANG:6,A3,A2;
  end;
  hence LocSeq F = 0 .--> il.(S,n) by A4,A5,A6,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)),
      M be Subset of the Instruction-Locations of S;
  cluster LocSeq M -> one-to-one;
coherence
proof
  set f = LocSeq M;
  set X = LocNums M;
  set C = canonical_isomorphism_of (RelIncl order_type_of RelIncl X,RelIncl X);
  let x1,x2 be set such that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f.x1 = f.x2;
A4: dom f = Card M by Def4;
  then
A5: f.x1 = il.(S,C.x1) by A1,Def4;
  f.x2 = il.(S,C.x2) by A2,A4,Def4;
  then
A6:C.x1 = C.x2 by A3,A5,AMISTD_1:25;
  consider phi being Ordinal-Sequence such that
A7:phi = C
   and
A8: phi is increasing and
A9: dom phi = order_type_of RelIncl X and rng phi = X by CARD_5:14;
A10:phi is one-to-one by A8,CARD_5:20;
  Card M c= order_type_of RelIncl X by Th28;
  hence x1 = x2 by A7,A6,A10,A1,A2,A4,A9,FUNCT_1:def 8;
end;
end;

:: Tree of Execution

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be FinPartState of S;
  func ExecTree(M) -> DecoratedTree of the Instruction-Locations of S means
:Def5:
  it.{} = FirstLoc(M) &
  for t being Element of dom it holds
    succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,it.t),it.t) } &
     for m being Nat st m in Card NIC(pi(M,it.t),it.t) holds
      it.(t^<*m*>) = (LocSeq NIC(pi(M,it.t),it.t)).m;
existence
proof
set D = the Instruction-Locations of S;
  defpred P[Instruction-Location of S,Nat,set] means
  ($2 in dom LocSeq NIC(pi(M,$1),$1) implies
   $3 = (LocSeq NIC(pi(M,$1),$1)).$2) &
  (not $2 in dom LocSeq NIC(pi(M,$1),$1) implies $3 = il.(S,0));
A1: for x being Element of D, y being Element of NAT
      ex z being Element of D st P[x,y,z]
    proof
      let x be Element of D, y be Element of NAT;
      set z = (LocSeq NIC(pi(M,x),x)).y;
      per cases;
      suppose
A2:     y in dom LocSeq NIC(pi(M,x),x);
      then
A3:   z in rng LocSeq NIC(pi(M,x),x) by FUNCT_1:def 5;
      take z;
      rng LocSeq NIC(pi(M,x),x) c= D by ORDINAL1:def 8;
      then z in D by A3;
      hence thesis by A2;
      suppose
A4:     not y in dom LocSeq NIC(pi(M,x),x);
      take il.(S,0);
      thus thesis by A4;
    end;
  consider f be Function of [:D,NAT:],D such that
A5: for l being Instruction-Location of S, n being Nat holds
     P[l,n,f.[l,n]] from FuncEx2D(A1);
  deffunc F(Instruction-Location of S) = Card NIC(pi(M,$1),$1);
A6: for d being Element of D,
        k1, k2 being Nat st k1 <= k2 & k2 in F(d) holds k1 in F(d)
   proof
     let d be Element of D,
         k1, k2 be Nat such that
A7:    k1 <= k2 and
A8:    k2 in F(d);
     k1 c= k2 by A7,CARD_1:56;
     hence thesis by A8,ORDINAL1:22;
   end;
  consider T being DecoratedTree of D such that
A9:T.{} = FirstLoc(M) and
A10:for t being Element of dom T holds
    succ t = { t^<*k*> where k is Nat: k in F(T.t)} &
     for n being Nat, x being set st x = T.t & n in F(x) holds
      T.(t^<*n*>) = f.[x,n] from DTreeStructEx(A6);
  take T;
  thus T.{} = FirstLoc(M) by A9;
  let t be Element of dom T;
  thus succ t = { t^<*k*> where k is Nat: k in F(T.t)} by A10;
  let m be Nat;
  assume
A11: m in Card NIC(pi(M,T.t),T.t);
A12: dom LocSeq NIC(pi(M,T.t),T.t) = Card NIC(pi(M,T.t),T.t) by Def4;
  thus T.(t^<*m*>) = f.[T.t,m] by A10,A11
    .= (LocSeq NIC(pi(M,T.t),T.t)).m by A5,A11,A12;
end;
uniqueness
proof
  let T1,T2 be DecoratedTree of the Instruction-Locations of S such that
A13: T1.{} = FirstLoc(M) and
A14: for t being Element of dom T1 holds
     succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t),T1.t)} &
     for m being Nat st m in Card NIC(pi(M,T1.t),T1.t) holds
      T1.(t^<*m*>) = (LocSeq NIC(pi(M,T1.t),T1.t)).m and
A15: T2.{} = FirstLoc(M) and
A16: for t being Element of dom T2 holds
     succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,T2.t),T2.t)} &
     for m being Nat st m in Card NIC(pi(M,T2.t),T2.t) holds
      T2.(t^<*m*>) = (LocSeq NIC(pi(M,T2.t),T2.t)).m;
   defpred P[Nat] means dom T1-level $1 = dom T2-level $1;
A17:P[0]
   proof
     thus dom T1-level 0 = {{}} by QC_LANG4:17
       .= dom T2-level 0 by QC_LANG4:17;
   end;
A18:for n being Nat st P[n] holds P[n+1]
   proof
     let n be Nat such that
A19:    P[n];
     set U1 = { succ w where w is Element of dom T1 : len w = n };
     set U2 = { succ w where w is Element of dom T2 : len w = n };
A20:  dom T1-level (n+1) = union U1 by QC_LANG4:18;
A21:  dom T1-level n = {v where v is Element of dom T1: len v = n}
       by TREES_2:def 6;
A22:  dom T2-level n = {v where v is Element of dom T2: len v = n}
       by TREES_2:def 6;
     union U1 = union U2
     proof
       hereby
         let a be set;
         assume a in union U1;
         then consider A being set such that
A23:        a in A and
A24:        A in U1 by TARSKI:def 4;
         consider w being Element of dom T1 such that
A25:        A = succ w and
A26:        len w = n by A24;
         w in dom T1-level n by A26,A21;
         then consider v being Element of dom T2 such that
A27:        w = v and
A28:        len v = n by A22,A19;
A29:      succ v = {v^<*k*> where k is Nat: k in Card NIC(pi(M,T2.v),T2.v)}
           by A16;
A30:      succ w = {w^<*k*> where k is Nat: k in Card NIC(pi(M,T1.w),T1.w)}
           by A14;
         defpred R[Nat] means
          $1 <= len w & w|Seg $1 in dom T1 & v|Seg $1 in dom T2 implies
           T1.(w|Seg $1) = T2.(w|Seg $1);
A31:      R[0]
         proof
           assume 0 <= len w;
           assume w|Seg 0 in dom T1;
           assume v|Seg 0 in dom T2;
           w|{} = {} by RELAT_1:110;
           hence T1.(w|Seg 0) = T2.(w|Seg 0) by A15,A13,FINSEQ_1:4;
         end;
A32:   for n being Nat st R[n] holds R[n+1]
   proof
    let n be Nat;
    assume that
A33:   R[n] and
A34:   n+1 <= len w and
A35:   w|Seg (n+1) in dom T1 and
A36:   v|Seg (n+1) in dom T2;
    set t1 = w|Seg n;
A37: n <= n+1 by NAT_1:29;
    then
A38: Seg n c= Seg(n+1) by FINSEQ_1:7;
    then
    w|Seg n = w|Seg(n+1)|Seg n by RELAT_1:103;
    then
A39: w|Seg n is_a_prefix_of w|Seg(n+1) by TREES_1:def 1;
    v|Seg n = v|Seg(n+1)|Seg n by A38,RELAT_1:103;
    then
A40: v|Seg n is_a_prefix_of v|Seg(n+1) by TREES_1:def 1;
A41: (w|Seg(n+1)).len(w|Seg(n+1)) is Nat by ORDINAL2:def 21;
A42: 1 <= n+1 by NAT_1:29;
    then
A43: n+1 in dom w by A34,FINSEQ_3:27;
A44: len(w|Seg(n+1)) = n+1 by A34,FINSEQ_1:21;
    then len(w|Seg(n+1)) in Seg(n+1) by A42,FINSEQ_1:3;
    then w.(n+1) = (w|Seg(n+1)).len(w|Seg(n+1)) by A44,FUNCT_1:72;
    then
A45: w|Seg(n+1) = t1^<*(w|Seg(n+1)).len (w|Seg(n+1))*> by A43,FINSEQ_5:11;
    reconsider t1 as Element of dom T1 by A39,A35,TREES_1:45;
    reconsider t2 = t1 as Element of dom T2 by A27,A40,A36,TREES_1:45;
A46: succ t1 = { t1^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t1),T1.t1)}
      by A14;
    t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> in succ t1 by A45,A41,A35,TREES_2:14;
    then consider k being Nat such that
A47:   t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> = t1^<*k*> and
A48:   k in Card NIC(pi(M,T1.t1),T1.t1) by A46;
A49:   k = (w|Seg(n+1)).len(w|Seg(n+1)) by A47,FINSEQ_2:20;
A50: (w|Seg(n+1)).len(w|Seg(n+1)) in Card NIC(pi(M,T2.t2),T2.t2)
      by A48,A47,A40,A33,A36,A37,A34,AXIOMS:22,TREES_1:45,FINSEQ_2:20;
    thus T1.(w|Seg(n+1)) =
         (LocSeq NIC(pi(M,T1.t1),T1.t1)).((w|Seg(n+1)).len (w|Seg(n+1)))
                by A14,A48,A49,A45
             .= T2.(w|Seg(n+1))
             by A16,A45,A50,A41,A40,A33,A36,A37,A34,AXIOMS:22,TREES_1:45;
  end;
A51:      for n being Nat holds R[n] from Ind(A31,A32);
         w = w|Seg len w by FINSEQ_3:55;
         then
A52:      T1.w = T2.w by A51,A27;
         succ v in U2 by A28;
         hence a in union U2 by A52,A27,A29,A30,A23,A25,TARSKI:def 4;
       end;
         let a be set;
         assume a in union U2;
         then consider A being set such that
A53:        a in A and
A54:        A in U2 by TARSKI:def 4;
         consider w being Element of dom T2 such that
A55:        A = succ w and
A56:        len w = n by A54;
         w in dom T2-level n by A56,A22;
         then consider v being Element of dom T1 such that
A57:        w = v and
A58:        len v = n by A21,A19;
A59:      succ v = {v^<*k*> where k is Nat: k in Card NIC(pi(M,T1.v),T1.v)}
           by A14;
A60:      succ w = {w^<*k*> where k is Nat: k in Card NIC(pi(M,T2.w),T2.w)}
           by A16;
         defpred R[Nat] means
          $1 <= len w & w|Seg $1 in dom T1 & v|Seg $1 in dom T2 implies
           T1.(w|Seg $1) = T2.(w|Seg $1);
A61:      R[0]
         proof
           assume 0 <= len w;
           assume w|Seg 0 in dom T1;
           assume v|Seg 0 in dom T2;
           w|{} = {} by RELAT_1:110;
           hence T1.(w|Seg 0) = T2.(w|Seg 0) by A15,A13,FINSEQ_1:4;
         end;
A62:   for n being Nat st R[n] holds R[n+1]
   proof
    let n be Nat;
    assume that
A63:   R[n] and
A64:   n+1 <= len w and
A65:   w|Seg (n+1) in dom T1 and
A66:   v|Seg (n+1) in dom T2;
    set t1 = w|Seg n;
A67: n <= n+1 by NAT_1:29;
    then
A68: Seg n c= Seg(n+1) by FINSEQ_1:7;
    then
    w|Seg n = w|Seg(n+1)|Seg n by RELAT_1:103;
    then
A69: w|Seg n is_a_prefix_of w|Seg(n+1) by TREES_1:def 1;
    v|Seg n = v|Seg(n+1)|Seg n by A68,RELAT_1:103;
    then
A70: v|Seg n is_a_prefix_of v|Seg(n+1) by TREES_1:def 1;
A71: (w|Seg(n+1)).len(w|Seg(n+1)) is Nat by ORDINAL2:def 21;
A72: 1 <= n+1 by NAT_1:29;
    then
A73: n+1 in dom w by A64,FINSEQ_3:27;
A74: len(w|Seg(n+1)) = n+1 by A64,FINSEQ_1:21;
    then len(w|Seg(n+1)) in Seg(n+1) by A72,FINSEQ_1:3;
    then w.(n+1) = (w|Seg(n+1)).len(w|Seg(n+1)) by A74,FUNCT_1:72;
    then
A75: w|Seg(n+1) = t1^<*(w|Seg(n+1)).len (w|Seg(n+1))*> by A73,FINSEQ_5:11;
    reconsider t1 as Element of dom T1 by A69,A65,TREES_1:45;
    reconsider t2 = t1 as Element of dom T2 by A57,A70,A66,TREES_1:45;
A76: succ t1 = { t1^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t1),T1.t1)}
      by A14;
    t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> in succ t1 by A75,A71,A65,TREES_2:14;
    then consider k being Nat such that
A77:   t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> = t1^<*k*> and
A78:   k in Card NIC(pi(M,T1.t1),T1.t1) by A76;
A79: k = (w|Seg(n+1)).len(w|Seg(n+1)) by A77,FINSEQ_2:20;
A80: (w|Seg(n+1)).len(w|Seg(n+1)) in Card NIC(pi(M,T2.t2),T2.t2)
      by A78,A77,A70,A63,A66,A67,A64,AXIOMS:22,TREES_1:45,FINSEQ_2:20;
    thus T1.(w|Seg(n+1)) =
       (LocSeq NIC(pi(M,T1.t1),T1.t1)).((w|Seg(n+1)).len(w|Seg(n+1)))
                by A14,A78,A79,A75
             .= T2.(w|Seg(n+1))
             by A75,A16,A80,A71,A70,A63,A66,A67,A64,AXIOMS:22,TREES_1:45;
  end;
A81:      for n being Nat holds R[n] from Ind(A61,A62);
         w = w|Seg len w by FINSEQ_3:55;
         then
A82:      T1.w = T2.w by A81,A57;
         succ v in U1 by A58;
         hence a in union U1 by A82,A57,A59,A60,A53,A55,TARSKI:def 4;
     end;
     hence thesis by A20,QC_LANG4:18;
   end;
A83: for n being Nat holds P[n] from Ind(A17,A18);
   then
A84:dom T1 = dom T2 by Th18;
  for p being FinSequence of NAT st p in dom T1 holds T1.p = T2.p
  proof
    let p be FinSequence of NAT;
    assume
A85:   p in dom T1;
defpred P[Nat] means
 $1 <= len p & p|Seg $1 in dom T1 implies T1.(p|Seg $1) = T2.(p|Seg $1);
A86: P[0]
  proof
    assume 0 <= len p;
    assume p|Seg 0 in dom T1;
    p|{} = {} by RELAT_1:110;
    hence T1.(p|Seg 0) = T2.(p|Seg 0) by A15,A13,FINSEQ_1:4;
  end;
A87: for n being Nat st P[n] holds P[n+1]
  proof
    let n be Nat;
    assume that
A88:   P[n] and
A89:   n+1 <= len p and
A90:   p|Seg (n+1) in dom T1;
    set t1 = p|Seg n;
A91: n <= n+1 by NAT_1:29;
    then Seg n c= Seg(n+1) by FINSEQ_1:7;
    then p|Seg n = p|Seg(n+1)|Seg n by RELAT_1:103;
    then
A92: p|Seg n is_a_prefix_of p|Seg(n+1) by TREES_1:def 1;
A93: (p|Seg(n+1)).len(p|Seg(n+1)) is Nat by ORDINAL2:def 21;
A94: 1 <= n+1 by NAT_1:29;
    then
A95: n+1 in dom p by A89,FINSEQ_3:27;
A96: len(p|Seg(n+1)) = n+1 by A89,FINSEQ_1:21;
    then len(p|Seg(n+1)) in Seg(n+1) by A94,FINSEQ_1:3;
    then p.(n+1) = (p|Seg(n+1)).len(p|Seg(n+1)) by A96,FUNCT_1:72;
    then
A97: p|Seg(n+1) = t1^<*(p|Seg(n+1)).len (p|Seg(n+1))*> by A95,FINSEQ_5:11;
    reconsider t1 as Element of dom T1 by A92,A90,TREES_1:45;
    reconsider t2 = t1 as Element of dom T2 by A83,Th18;
A98: succ t1 = { t1^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t1),T1.t1)}
      by A14;
    t1^<*(p|Seg(n+1)).len (p|Seg(n+1))*> in succ t1 by A97,A93,A90,TREES_2:14;
    then consider k being Nat such that
A99:   t1^<*(p|Seg(n+1)).len (p|Seg(n+1))*> = t1^<*k*> and
A100:   k in Card NIC(pi(M,T1.t1),T1.t1) by A98;
A101: k = (p|Seg(n+1)).len (p|Seg(n+1)) by A99,FINSEQ_2:20;
A102: (p|Seg(n+1)).len (p|Seg(n+1)) in Card NIC(pi(M,T2.t2),T2.t2)
      by A100,A99,A88,A91,A89,AXIOMS:22,FINSEQ_2:20;
    thus T1.(p|Seg (n+1)) =
     (LocSeq NIC(pi(M,T1.t1),T1.t1)).((p|Seg(n+1)).len (p|Seg(n+1)))
                by A14,A100,A101,A97
       .= T2.(p|Seg (n+1)) by A97,A16,A102,A93,A88,A91,A89,AXIOMS:22;
  end;
A103:  for n being Nat holds P[n] from Ind(A86,A87);
  p|Seg len p = p by FINSEQ_3:55;
  hence thesis by A103,A85;
  end;
  hence T1 = T2 by A84,TREES_2:33;
end;
end;

theorem
  for S being standard halting realistic
        (IC-Ins-separated definite (non empty non void AMI-Struct over N))
  holds
  ExecTree Stop S = TrivialInfiniteTree --> il.(S,0)
proof
  let S be standard halting realistic
        (IC-Ins-separated definite (non empty non void AMI-Struct over N));
  set D = TrivialInfiniteTree;
  set M = Stop S;
  set E = ExecTree M;
A1: M = il.(S,0) .--> halt S by AMISTD_2:def 13;
  then
A2: dom M = {il.(S,0)} by CQC_LANG:5;
A3: M.il.(S,0) = halt S by A1,CQC_LANG:6;
A4: E.{} = FirstLoc(M) by Def5;
A5: for t being Element of dom E holds Card NIC(halt S,E.t) = {0}
    proof
      let t be Element of dom E;
      NIC(halt S,E.t) = {E.t} by AMISTD_1:15;
      hence thesis by CARD_1:50,CARD_2:20,CARD_5:1;
    end;
    defpred R[set] means E.$1 in dom M;
A6: R[<*>NAT] by A4,Th21;
A7: for f being Element of dom E st R[f]
      for a being Nat st f^<*a*> in dom E holds R[f^<*a*>]
    proof
      let f be Element of dom E such that
A8:     R[f];
      let a be Nat such that
A9:     f^<*a*> in dom E;
A10:   Card NIC(halt S,E.f) = {0} by A5;
A11:   succ f = { f^<*k*> where k is Nat: k in Card NIC(pi(M,E.f),E.f) }
        by Def5;
A12:   E.f = il.(S,0) by A8,A2,TARSKI:def 1;
      then
A13:   locnum (E.f) = 0 by AMISTD_1:def 13;
A14:   pi(M,E.f) = M.(E.f) by A8,AMI_5:def 5;
      then
A15:   0 in Card NIC(pi(M,E.f),E.f) by A10,A12,A3,TARSKI:def 1;
A16:   succ f = { f^<*0*> }
      proof
        hereby
          let s be set;
          assume s in succ f;
          then consider k being Nat such that
A17:         s = f^<*k*> and
A18:       k in Card NIC(pi(M,E.f),E.f) by A11;
          k = 0 by A3,A18,A12,A10,A14,TARSKI:def 1;
          hence s in { f^<*0*> } by A17,TARSKI:def 1;
        end;
        let s be set;
        assume s in { f^<*0*> };
        then s = f^<*0*> by TARSKI:def 1;
        hence s in succ f by A11,A15;
      end;
      f^<*a*> in succ f by A9,TREES_2:14;
      then
A19:   f^<*a*> = f^<*0*> by A16,TARSKI:def 1;
      LocNums NIC(halt S,E.f) = {0} by A13,Th29;
      then canonical_isomorphism_of
         (RelIncl order_type_of RelIncl LocNums NIC(pi(M,E.f),E.f),
          RelIncl LocNums NIC(pi(M,E.f),E.f)) = 0 .--> locnum (E.f)
               by A12,A3,A14,A13,Th15;
      then
A20:   canonical_isomorphism_of
        (RelIncl order_type_of RelIncl LocNums NIC(pi(M,E.f),E.f),
           RelIncl LocNums NIC(pi(M,E.f),E.f)).0 = locnum (E.f) by CQC_LANG:6
       .= 0 by A12,AMISTD_1:def 13;
      E.(f^<*a*>) = (LocSeq NIC(pi(M,E.f),E.f)).0 by A15,A19,Def5
                 .= il.(S,0) by A20,A15,Def4;
      hence R[f^<*a*>] by A2,TARSKI:def 1;
    end;
A21: for f being Element of dom E holds R[f] from InTreeInd(A6,A7);
  defpred X[Nat] means dom E-level $1 = D-level $1;
A22: X[0]
   proof
     thus dom E-level 0 = {{}} by QC_LANG4:17
       .= D-level 0 by QC_LANG4:17;
   end;
A23: for n being Nat st X[n] holds X[n+1]
  proof
    let n be Nat;
    assume
A24:   X[n];
    set f0 = n |-> 0;
    set f1 = (n+1) |-> 0;
A25: dom E-level (n+1) = {w where w is Element of dom E: len w = n+1}
       by TREES_2:def 6;
A26: len f1 = n+1 by FINSEQ_2:69;
    dom E-level (n+1) = {f1}
    proof
      hereby
        let a be set;
        assume a in dom E-level (n+1);
        then consider t1 being Element of dom E such that
A27:       a = t1 and
A28:       len t1 = n+1 by A25;
        reconsider t0 = t1|Seg n as Element of dom E by Th17;
A29:     dom E-level n = {w where w is Element of dom E: len w = n}
          by TREES_2:def 6;
A30:     succ t0 = { t0^<*k*> where k is Nat: k in Card NIC(pi(M,E.t0),E.t0) }
          by Def5;
A31:     Card NIC(halt S,E.t0) = {0} by A5;
A32:     E.t0 in dom M by A21;
        then
A33:     E.t0 = il.(S,0) by A2,TARSKI:def 1;
A34:     pi(M,E.t0) = M.(E.t0) by A32,AMI_5:def 5;
        then
A35:     0 in Card NIC(pi(M,E.t0),E.t0) by A31,A33,A3,TARSKI:def 1;
A36:     t1.(n+1) is Nat by ORDINAL2:def 21;
A37:     dom E-level n = {f0} by A24,Th20;
        n <= n+1 by NAT_1:29;
        then Seg n c= Seg(n+1) by FINSEQ_1:7;
        then Seg n c= dom t1 by A28,FINSEQ_1:def 3;
        then dom t0 = Seg n by RELAT_1:91;
        then len t0 = n by FINSEQ_1:def 3;
        then
A38:    t0 in dom E-level n by A29;
        t1 = t0^<*t1.(n+1)*> by A28,FINSEQ_3:61;
        then
A39:     t0^<*t1.(n+1)*> in succ t0 by A36,TREES_2:14;
        succ t0 = { t0^<*0*> }
        proof
          hereby
            let s be set;
            assume s in succ t0;
            then consider k being Nat such that
A40:           s = t0^<*k*> and
A41:           k in Card NIC(pi(M,E.t0),E.t0) by A30;
            k = 0 by A34,A3,A41,A33,A31,TARSKI:def 1;
            hence s in { t0^<*0*> } by A40,TARSKI:def 1;
          end;
          let s be set;
          assume s in { t0^<*0*> };
          then s = t0^<*0*> by TARSKI:def 1;
          hence s in succ t0 by A30,A35;
        end;
        then
A42:    t0^<*t1.(n+1)*> = t0^<*0*> by A39,TARSKI:def 1;
        for k being Nat st 1 <= k & k <= len t1 holds t1.k = f1.k
        proof
          let k be Nat such that
A43:        1 <= k & k <= len t1;
A44:      k in Seg(n+1) by A28,A43,FINSEQ_1:3;
          now
            per cases by A44,FINSEQ_2:8;
            suppose
A45:          k in Seg n;
            hence t1.k = t0.k by FUNCT_1:72
               .= f0.k by A38,A37,TARSKI:def 1
               .= 0 by A45,FINSEQ_2:70;
            suppose k = n+1;
            hence t1.k = 0 by A42,FINSEQ_2:20;
          end;
          hence t1.k = f1.k by A44,FINSEQ_2:70;
        end;
        then t1 = f1 by A28,A26,FINSEQ_1:18;
        hence a in {f1} by A27,TARSKI:def 1;
      end;
      let a be set;
      assume a in {f1};
      then
A46:   a = f1 by TARSKI:def 1;
      defpred P[Nat] means $1 |-> 0 in dom E;
      0 |-> 0 = {} by FINSEQ_2:72;
      then
A47:   P[0] by TREES_1:47;
A48:   for n being Nat st P[n] holds P[n+1]
      proof
        let n be Nat;
        assume P[n];
        then reconsider t = n |-> 0 as Element of dom E;
A49:     succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,E.t),E.t) }
          by Def5;
A50:     Card NIC(halt S,E.t) = {0} by A5;
A51:     E.t in dom M by A21;
        then
A52:     E.t = il.(S,0) by A2,TARSKI:def 1;
        pi(M,E.t) = M.(E.t) by A51,AMI_5:def 5;
        then 0 in Card NIC(pi(M,E.t),E.t) by A50,A52,A3,TARSKI:def 1;
        then t^<*0*> in succ t by A49;
        then t^<*0*> in dom E;
        hence thesis by FINSEQ_2:74;
      end;
      for n being Nat holds P[n] from Ind(A47,A48);
      then f1 is Element of dom E;
      hence a in dom E-level (n+1) by A25,A26,A46;
    end;
    hence thesis by Th20;
  end;
  for x being Nat holds X[x] from Ind(A22,A23);
  then
A53: dom E = D by Th18;
  for x being set st x in dom E holds E.x = il.(S,0)
  proof
    let x be set;
    assume x in dom E;
    then reconsider x as Element of dom E;
    E.x in dom M by A21;
    then E.x in {il.(S,0)} by A1,CQC_LANG:5;
    hence thesis by TARSKI:def 1;
  end;
  hence thesis by A53,FUNCOP_1:17;
end;

Back to top