:: Replacement of Subtrees in a Tree
::  by Oleg Okhotnikov
::
:: Received October 1, 1995
:: Copyright (c) 1995-2012 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 TREES_1, FINSEQ_1, NUMBERS, SUBSET_1, ORDINAL4, XBOOLE_0, TARSKI,
      RELAT_1, XXREAL_0, ARYTM_3, TREES_2, FUNCT_1, TREES_A;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, ORDINAL1, NAT_1,
      RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2;
 constructors XXREAL_0, NAT_1, MEMBERED, TREES_2, RELSET_1, FINSEQ_2;
 registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_1, TREES_2;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, TREES_1, TREES_2, RELAT_1;
 theorems TARSKI, FUNCT_1, FINSEQ_1, TREES_1, TREES_2, XBOOLE_0, XBOOLE_1,
      RELAT_1;
 schemes TREES_2;

begin

reserve T, T1 for Tree,
  P for AntiChain_of_Prefixes of T,
  p1 for FinSequence,
  p, q, r, s, p9 for FinSequence of NAT,
  x, Z for set,
  t for Element of T,
  k, n for Element of NAT;

theorem Th1:
  for p,q,r,s being FinSequence st p^q = s^r holds p,s are_c=-comparable
proof
  let p,q,r,s be FinSequence;
  assume
A1: p^q = s^r;
  then  p is_a_prefix_of s^r & s is_a_prefix_of p^q by TREES_1:1;
  hence thesis by A1,TREES_2:1;
end;

definition
  let T,T1;
  let P such that
A1: P<>{};
  func tree(T,P,T1) -> Tree means
  :Def1:
  q in it iff (q in T & for p st p in P holds not p is_a_proper_prefix_of q)
  or ex p,r st p in P & r in T1 & q = p^r;
  existence
  proof
    reconsider P9 = P as Subset of T by TREES_1:def 11;
 now
      let x;
      assume
A1:   x in P9;
      then reconsider x9 = x as FinSequence by TREES_1:def 10;
      reconsider x9 as Element of T by A1;
   now
        let p such that
A2:     p in P;
        per cases;
        suppose
       p <> x9;
then        not p,x9 are_c=-comparable by A1,A2,TREES_1:def 10;
          hence not p is_a_proper_prefix_of x9 by XBOOLE_1:104;
        end;
        suppose
       p = x9;
          hence not p is_a_proper_prefix_of x9;
        end;
      end;
      hence x in {t : for p st p in P holds not p is_a_proper_prefix_of t};
    end;
then  P c= {t : for p st p in P holds not p is_a_proper_prefix_of t}
    by TARSKI:def 3;
    then reconsider Y = {t : for p st p in P holds not p is_a_proper_prefix_of
    t} as non empty set by A1,XBOOLE_1:3;
    consider Z such that
A3: Z = {p^s where p is Element of T, s is Element of T1 : p in P};
    reconsider X = Y \/ Z as non empty set;
A4: x in {t : for p st p in P holds not p is_a_proper_prefix_of t} implies
    x is FinSequence of NAT & x in NAT* & x in T
    proof
      assume x in {t : for p st p in P holds not p is_a_proper_prefix_of t};
      then A5:  ex
 t st x = t & for p st p in P holds not p is_a_proper_prefix_of t;
      hence x is FinSequence of NAT;
      thus thesis by A5,FINSEQ_1:def 11;
    end;
 X is Tree-like
    proof
      thus X c= NAT*
      proof
        let x;
        assume x in X;
        then A6:    x
 in {t : for p st p in P holds not p is_a_proper_prefix_of t } or
        x in {p^s where p is Element of T, s is Element of T1 : p in P}
        by A3,XBOOLE_0:def 3;
    now
          assume x
 in {p^s where p is Element of T, s is Element of T1 : p in
          P };
then       ex p being Element of T st ex s being Element of T1 st
          x = p^s & p in P;
          hence x is FinSequence of NAT;
        end;
        hence thesis by A4,A6,FINSEQ_1:def 11;
      end;
      thus for q st q in X holds ProperPrefixes q c= X
      proof
        let q such that
A7:    q in X;
A8:    now
          assume
A9:      q in {t : for p st p in P holds not p is_a_proper_prefix_of t};
then       ex t st q = t &
          for p st p in P holds not p is_a_proper_prefix_of t;
then A10:      ProperPrefixes q c= T by TREES_1:def 3;
          thus ProperPrefixes q c= X
          proof
            let x;
            assume
A11:        x in ProperPrefixes q;
            then consider p1 such that
A12:        x = p1 and
A13:        p1 is_a_proper_prefix_of q by TREES_1:def 2;
            reconsider p1 as Element of T by A10,A11,A12;
        for p st p in P holds not p is_a_proper_prefix_of p1
            proof
              let p such that
A14:          p in P;
              ex t st q = t & for p st p in P holds not p
              is_a_proper_prefix_of t by A9;
              hence thesis by A13,A14,XBOOLE_1:56;
            end;
then         x in { s1 where s1 is Element of T : for p st p in P holds
            not p is_a_proper_prefix_of s1 } by A12;
            hence thesis by XBOOLE_0:def 3;
          end;
        end;
    now
          assume q in Z;
          then consider p being Element of T, s being Element of T1 such that
A15:      q = p^s and
A16:      p in P by A3;
          thus ProperPrefixes q c= X
          proof
            let x;
            assume
A17:        x in ProperPrefixes q;
            then reconsider r = x as FinSequence by TREES_1:11;
        r is_a_proper_prefix_of p^s by A15,A17,TREES_1:12;
then         r is_a_prefix_of p^s by XBOOLE_0:def 8;
            then consider r1 being FinSequence such that
A18:        p^s = r^r1 by TREES_1:1;
A19:        now
              assume len p <= len r;
              then consider r2 being FinSequence such that
A20:          p^r2 = r by A18,FINSEQ_1:47;
          p^s = p^(r2^r1) by A18,A20,FINSEQ_1:32;
then           s = r2^r1 by FINSEQ_1:33;
then           s|(dom r2) = r2 by FINSEQ_1:21;
then A21:          s|Seg(len r2) = r2 by FINSEQ_1:def 3;
              then reconsider r2 as FinSequence of NAT by FINSEQ_1:18;
          r2 is_a_prefix_of s by A21,TREES_1:def 1;
              then reconsider r2 as Element of T1 by TREES_1:20;
          r = p^r2 by A20;
then           r in { w^v where w is Element of T,
              v is Element of T1 : w in P } by A16;
              hence r in X by A3,XBOOLE_0:def 3;
            end;
        now
              assume len r <= len p;
then           ex r2 being FinSequence st r^r2 = p by A18,FINSEQ_1:47;
then           p|(dom r) = r by FINSEQ_1:21;
then A22:          p|Seg(len r) = r by FINSEQ_1:def 3;
              then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:18;
A23:          r3 is_a_prefix_of p by A22,TREES_1:def 1;
              then reconsider r3 as Element of T by TREES_1:20;
          for p9 st p9 in P holds not p9 is_a_proper_prefix_of r3
              proof
                let p9;
                assume
A24:            p9 in P;
                assume
A25:            p9 is_a_proper_prefix_of r3;
then             p9 is_a_prefix_of r3 by XBOOLE_0:def 8;
then             p9 is_a_prefix_of p by A23,XBOOLE_1:1;
then A26:            p,p9 are_c=-comparable by XBOOLE_0:def 9;
                per cases;
                suppose
              p<>p9;
                  hence contradiction by A16,A24,A26,TREES_1:def 10;
                end;
                suppose
              p=p9;
                  hence contradiction by A23,A25,XBOOLE_0:def 8;
                end;
              end;
then           r3 in { t : for p9 st p9 in P holds
              not p9 is_a_proper_prefix_of t };
              hence r in X by XBOOLE_0:def 3;
            end;
            hence thesis by A19;
          end;
        end;
        hence thesis by A7,A8,XBOOLE_0:def 3;
      end;
      let q,k,n such that
A27:  q^<*k*> in X and
A28:  n <= k;
A29:  now
        assume
A30:    q^<*k*> in { t : for p st p in P holds not p is_a_proper_prefix_of t };
then     ex s being Element of T st
        q^<*k*> = s & for p st p in P holds not p is_a_proper_prefix_of s;
        then reconsider u = q^<*n*> as Element of T by A28,TREES_1:def 3;
    now
          let p such that
A31:      p in P;
          assume p is_a_proper_prefix_of u;
          then
A32:      p is_a_prefix_of q by TREES_1:9;
          ex s being Element of T st q^<*k*> = s & for p st p in
          P holds not p is_a_proper_prefix_of s by A30;
          hence contradiction by A31,A32,TREES_1:8;
        end;
then     q^<*n*> in {t : for p st p in P holds not p
        is_a_proper_prefix_of t};
        hence q^<*n*> in X by XBOOLE_0:def 3;
      end;
  now
        assume q^<*k*> in Z;
        then consider p being Element of T, s being Element of T1 such that
A33:    q^<*k*> = p^s and
A34:    p in P by A3;
A35:    now
          assume len q <= len p;
          then consider r being FinSequence such that
A36:      q^r = p by A33,FINSEQ_1:47;
      q^<*k*> = q^(r^s) by A33,A36,FINSEQ_1:32;
then A37:      <*k*> = r^s by FINSEQ_1:33;
A38:      now
            assume
A39:        r = <*k*>;
            then reconsider s9 = q^<*n*> as Element of T by A28,A36,
TREES_1:def 3;
        now
              let p9 such that
A40:          p9 in P;
              assume
A41:          p9 is_a_proper_prefix_of s9;
then A42:          p9 is_a_prefix_of s9 by XBOOLE_0:def 8;
A43:          len p = len q + len <*k*> by A36,A39,FINSEQ_1:22
                .= len q + 1 by FINSEQ_1:40
                .= len q + len <*n*> by FINSEQ_1:40
                .= len s9 by FINSEQ_1:22;
              per cases;
              suppose
            p9 = p;
                hence contradiction by A41,A42,A43,TREES_1:2;
              end;
              suppose
A44:            p9 <> p;
                            q
 is_a_prefix_of p & p9 is_a_prefix_of q by A36,A41,TREES_1:1,9;
then             p9 is_a_prefix_of p by XBOOLE_1:1;
then             p,p9 are_c=-comparable by XBOOLE_0:def 9;
                hence contradiction by A34,A40,A44,TREES_1:def 10;
              end;
            end;
            hence q^<*n*> in { t : for p st p in P holds
            not p is_a_proper_prefix_of t };
          end;
      now
            assume that
A45:        s = <*k*> and
A46:        r = {};
       s = <*>NAT^s by FINSEQ_1:34;
then        <*>NAT^<*n*> in T1 by A28,A45,TREES_1:def 3;
            then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;
       q^<*n*> = p^t by A36,A46,FINSEQ_1:34;
            hence q^<*n*> in Z by A3,A34;
          end;
          hence q^<*n*> in X by A37,A38,FINSEQ_1:88,XBOOLE_0:def 3;
        end;
   now
          assume len p <= len q;
          then consider r being FinSequence such that
A47:     p^r = q by A33,FINSEQ_1:47;
     p^(r^<*k*>) = p^s by A33,A47,FINSEQ_1:32;
then A48:     r^<*k*> = s by FINSEQ_1:33;
then      s|dom r = r by FINSEQ_1:21;
then      s|Seg len r = r by FINSEQ_1:def 3;
          then reconsider r as FinSequence of NAT by FINSEQ_1:18;
          reconsider t = r^<*n*> as Element of T1 by A28,A48,TREES_1:def 3;
     q^<*n*> = p^t by A47,FINSEQ_1:32;
then      q^<*n*> in { p9^v where p9 is Element of T,
          v is Element of T1 : p9 in P } by A34;
          hence q^<*n*> in X by A3,XBOOLE_0:def 3;
        end;
        hence q^<*n*> in X by A35;
      end;
      hence q^<*n*> in X by A27,A29,XBOOLE_0:def 3;
    end;
    then reconsider X as Tree;
    take X;
    let q;
    thus q in X implies
    (q in T & for p st p in P holds not p is_a_proper_prefix_of q)
    or ex p,r st p in P & r in T1 & q = p^r
    proof
      assume
A49: q in X;
A50: now
        assume q in Y;
then    ex s being Element of T st q = s &
        for p st p in P holds not p is_a_proper_prefix_of s;
        hence thesis;
      end;
 now
        assume q in Z;
then    ex p being Element of T st ex s being Element of T1 st
        q = p^s & p in P by A3;
        hence ex p,r st p in P & r in T1 & q = p^r;
      end;
      hence thesis by A49,A50,XBOOLE_0:def 3;
    end;
    assume
A51: (q in T & for p st p in P holds not p is_a_proper_prefix_of q)
    or ex p,r st p in P & r in T1 & q = p^r;
A52: (q in T & for p st p in P holds not p is_a_proper_prefix_of q) implies
    q in {t : for p st p in P holds not p is_a_proper_prefix_of t};
 now
      given p,r such that
A53: p in P & r in T1 & q = p^r;
 P c= T by TREES_1:def 11;
      hence q in Z by A3,A53;
    end;
    hence thesis by A51,A52,XBOOLE_0:def 3;
  end;
  uniqueness
  proof
    let S1,S2 be Tree such that
A54: q in S1 iff (q in T & for p st p in
    P holds not p is_a_proper_prefix_of q)
    or ex p,r st p in P & r in T1 & q = p^r and
A55: q in S2 iff (q in T & for p st p in
    P holds not p is_a_proper_prefix_of q)
    or ex p,r st p in P & r in T1 & q = p^r;
    let x be FinSequence of NAT;
    thus x in S1 implies x in S2
    proof
      assume
A56: x in S1;
      reconsider q = x as FinSequence of NAT;
 (q in T & for p st p in P holds not p is_a_proper_prefix_of q)
      or ex p,r st p in P & r in T1 & q = p^r by A54,A56;
      hence thesis by A55;
    end;
    assume
A57: x in S2;
    reconsider q = x as FinSequence of NAT;
 (q in T & for p st p in P holds not p is_a_proper_prefix_of q)
    or ex p,r st p in P & r in T1 & q = p^r by A55,A57;
    hence thesis by A54;
  end;
end;

theorem Th2:
  P <> {} implies tree(T,P,T1) = {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1}
  \/ { p^s where p is Element of T, s is Element of T1 : p in P }
proof
  assume
A1: P <> {};
  thus tree(T,P,T1) c=
  {t : for p st p in P holds not p is_a_proper_prefix_of t} \/
  { p^s where p is Element of T, s is Element of T1 : p in P }
  proof
    let x be set;
    assume
A2: x in tree(T,P,T1);
    then reconsider q = x as FinSequence of NAT by TREES_1:19;
A3: now
      given p,r such that
A4:   p in P & r in T1 & q = p^r;
   P c= T by TREES_1:def 11;
      hence x in { p9^s where p9 is Element of T,
      s is Element of T1 : p9 in P } by A4;
    end;
     q in T & (for p st p in P holds not p is_a_proper_prefix_of q) implies
    x in { t : for p st p in P holds not p is_a_proper_prefix_of t };
    hence thesis by A1,A2,A3,Def1,XBOOLE_0:def 3;
  end;
  let x be set such that
A5: x in { t : for p st p in P holds not p is_a_proper_prefix_of t } \/
  { p^s where p is Element of T, s is Element of T1 : p in P };
A6: now
    assume x in { p^s where p is Element of T, s is Element of T1 : p in P };
then  ex p being Element of T st
    ex s being Element of T1 st x = p^s & p in P;
    hence thesis by Def1;
  end;
 now
    assume x in { t : for p st p in P holds not p is_a_proper_prefix_of t };
then  ex t st x = t & for p st p in P holds not p is_a_proper_prefix_of t;
    hence thesis by A1,Def1;
  end;
  hence thesis by A5,A6,XBOOLE_0:def 3;
end;

theorem Th3:
  {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1} c=
  {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1}
proof
  let x be set;
  assume x in {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1};
  then consider t9 being Element of T such that
A1: x = t9 and
A2: for p st p in P holds not p is_a_prefix_of t9;
 now
    let p;
    assume p in P;
then  not p is_a_prefix_of t9 by A2;
    hence not p is_a_proper_prefix_of t9 by XBOOLE_0:def 8;
  end;
  hence thesis by A1;
end;

theorem Th4:
  P c= {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1}
proof
  let x be set;
  assume
A1: x in P;
 ex t1 being Element of T st x = t1 &
  for p st p in P holds not p is_a_proper_prefix_of t1
  proof
 P c= T by TREES_1:def 11;
    then consider t9 being Element of T such that
A2: t9 = x by A1;
 now
      let p such that
A3:   p in P;
      per cases;
      suppose
     t9 = p;
        hence not p is_a_proper_prefix_of t9;
      end;
      suppose
     t9 <> p;
then      not t9, p are_c=-comparable by A1,A2,A3,TREES_1:def 10;
        hence not p is_a_proper_prefix_of t9 by XBOOLE_1:104;
      end;
    end;
    hence thesis by A2;
  end;
  hence thesis;
end;

theorem Th5:
  {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1} \
  {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1} = P
proof
 now
    let x be set;
    assume
A1: x in {t1 where t1 is Element of T :
    for p st p in P holds not p is_a_proper_prefix_of t1} \
    {t1 where t1 is Element of T :
    for p st p in P holds not p is_a_prefix_of t1};
then A2: x in {t1 where t1 is Element of T : for p st p in P holds not p
    is_a_proper_prefix_of t1};
A3: not x in {t1 where t1 is Element of T : for p st p in P holds not p
    is_a_prefix_of t1} by A1,XBOOLE_0:def 5;
    assume
A4: not x in P;
 ex t1 being Element of T st x = t1 &
    for p st p in P holds not p is_a_prefix_of t1
    proof
      consider t9 being Element of T such that
A5:   x = t9 and
A6:   for p st p in P holds not p is_a_proper_prefix_of t9 by A2;
   now
        let p;
        assume
A7:    p in P;
then A8:    not p is_a_proper_prefix_of t9 by A6;
        per cases by A8,XBOOLE_0:def 8;
        suppose
      not p is_a_prefix_of t9;
          hence not p is_a_prefix_of t9;
        end;
        suppose
      p = t9;
          hence not p is_a_prefix_of t9 by A4,A5,A7;
        end;
      end;
      hence thesis by A5;
    end;
    hence contradiction by A3;
  end;
  hence {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1} \
  {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1} c= P by TARSKI:def 3;
  let x be set;
  assume
A9: x in P;
A10: P c= {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1} by Th4;
 not x in {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1}
  proof
    assume x in {t1 where t1 is Element of T :
    for p st p in P holds not p is_a_prefix_of t1};
then  ex t9 being Element of T st x = t9 & for p st p in P
    holds not p is_a_prefix_of t9;
    hence contradiction by A9;
  end;
  hence thesis by A9,A10,XBOOLE_0:def 5;
end;

theorem Th6:
  for T, T1, P holds
  P c= { p^s where p is Element of T, s is Element of T1 : p in P }
proof
  let T, T1, P;
 now
    let x be set;
    assume
A1: x in P;
 P c= T by TREES_1:def 11;
    then consider q being Element of T such that
A2: q = x by A1;
 <*> NAT in T1 by TREES_1:22;
    then consider s9 being Element of T1 such that
A3: s9 = <*> NAT;
 q = q^s9 by A3,FINSEQ_1:34;
    thus
    then x in { p^s where p is Element of T, s is Element of T1 : p in P }
    by A1,A2;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th7:
  P <> {} implies tree(T,P,T1) = {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1}
  \/ { p^s where p is Element of T, s is Element of T1 : p in P }
proof
  assume
A1: P <> {};
then A2: tree(T,P,T1) = {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_proper_prefix_of t1}
  \/ { p^s where p is Element of T, s is Element of T1 : p in P } by Th2;
  thus tree(T,P,T1) c= {t1 where t1 is Element of T :
  for p st p in P holds not p is_a_prefix_of t1}
  \/ { p^s where p is Element of T, s is Element of T1 : p in P }
  proof
    let x be set;
    assume x in tree(T,P,T1);
then A3: x in {t1 where t1 is Element of T :
    for p st p in P holds not p is_a_proper_prefix_of t1}
    \/ { p^s where p is Element of T, s is Element of T1 : p in P } by A1,Th2;
 now per cases;
      suppose
A4:     x in P;
     P c= { p^s where p is Element of T, s is Element of T1 : p in P }
        by Th6;
        hence x in {t1 where t1 is Element of T :
        for p st p in P holds not p is_a_prefix_of t1}
        or x in { p^s where p is Element of T, s is Element of T1 : p in P }
        by A4;
      end;
      suppose
A5:     not x in P;
     now per cases by A3,XBOOLE_0:def 3;
          suppose
A6:        x in {t1 where t1 is Element of T :
            for p st p in P holds not p is_a_proper_prefix_of t1};
        x in {t1 where t1 is Element of T :
            for p st p in P holds not p is_a_prefix_of t1}
            proof
              assume
A7:          not x in {t1 where t1 is Element of T :
              for p st p in P holds not p is_a_prefix_of t1};
          {t1 where t1 is Element of T :
              for p st p in P holds not p is_a_proper_prefix_of t1} \
              {t1 where t1 is Element of T :
              for p st p in P holds not p is_a_prefix_of t1} = P by Th5;
              hence contradiction by A5,A6,A7,XBOOLE_0:def 5;
            end;
            hence x in {t1 where t1 is Element of T :
            for p st p in P holds not p is_a_prefix_of t1} or
            x in { p^s where p is Element of T, s is Element of T1 : p in P };
          end;
          suppose
                    x
 in { p^s where p is Element of T, s is Element of T1 : p in P };
            hence x in {t1 where t1 is Element of T :
            for p st p in P holds not p is_a_prefix_of t1} or
            x in { p^s where p is Element of T, s is Element of T1 : p in P };
          end;
        end;
        hence x in {t1 where t1 is Element of T :
        for p st p in P holds not p is_a_prefix_of t1}
        or x in { p^s where p is Element of T, s is Element of T1 : p in P };
      end;
    end;
    hence thesis by XBOOLE_0:def 3;
  end;
  thus thesis by A2,Th3,XBOOLE_1:9;
end;

theorem
  p in P implies T1 = tree(T,P,T1)|p
proof
  assume
A1: p in P;
 ex q,r st q in P & r in T1 & p = q^r
  proof
    consider q such that
A2: q = p;
    consider r such that
A3: r = <*> NAT;
A4: r in T1 by A3,TREES_1:22;
 p = q^r by A2,A3,FINSEQ_1:34;
    hence thesis by A1,A2,A4;
  end;
then A5: p in tree(T,P,T1) by Def1;
  let x be FinSequence of NAT;
  thus x in T1 implies x in tree(T,P,T1)|p
  proof
    assume x in T1;
then  p^x in tree(T,P,T1) by A1,Def1;
    hence thesis by A5,TREES_1:def 6;
  end;
  thus x in tree(T,P,T1)|p implies x in T1
  proof
    assume x in tree(T,P,T1)|p;
then A6: p^x in tree(T,P,T1) by A5,TREES_1:def 6;
A7: now
      assume that p^x in T and
A8:  for r st r in P holds not r is_a_proper_prefix_of p^x;
A9:  not p is_a_proper_prefix_of p^x by A1,A8;
  p is_a_prefix_of p^x by TREES_1:1;
then   p^x = p by A9,XBOOLE_0:def 8
        .= p^<*>NAT by FINSEQ_1:34;
then   x = {} by FINSEQ_1:33;
      hence thesis by TREES_1:22;
    end;
 now
      given s,r such that
A10:  s in P and
A11:  r in T1 and
A12:  p^x = s^r;
  now
        assume s <> p;
then     not s,p are_c=-comparable by A1,A10,TREES_1:def 10;
        hence contradiction by A12,Th1;
      end;
      hence thesis by A11,A12,FINSEQ_1:33;
    end;
    hence thesis by A1,A6,A7,Def1;
  end;
end;

registration
  let T;
  cluster non empty for AntiChain_of_Prefixes of T;
  existence
  proof
    set w = the Element of T;
    consider X being set such that
A1: X = {w};
A2: X is AntiChain_of_Prefixes-like by A1,TREES_1:36;
 X c= T
    proof
      let x be set;
      assume x in X;
then    x = w by A1,TARSKI:def 1;
      hence thesis;
    end;
    then reconsider X as AntiChain_of_Prefixes of T by A2,TREES_1:def 11;
    take X;
    thus thesis by A1;
  end;
end;

definition
  let T;
  let t be Element of T;
  redefine func {t} -> AntiChain_of_Prefixes of T;
  correctness by TREES_1:39;
end;

theorem Th9:
  tree(T,{t},T1) = T with-replacement (t,T1)
proof
  let p;
  thus p in tree(T,{t},T1) implies p in T with-replacement (t,T1)
  proof
    assume
A1: p in tree(T,{t},T1);
A2: now
      assume
A3:   p in T & for s st s in {t} holds not s is_a_proper_prefix_of p;
   t in {t} by TARSKI:def 1;
      hence p in T & not t is_a_proper_prefix_of p by A3;
    end;
 now
      given s such that
A4:   ex r st s in {t} & r in T1 & p = s^r;
   s = t by A4,TARSKI:def 1;
      hence ex r st r in T1 & p = t^r by A4;
    end;
    hence thesis by A1,A2,Def1,TREES_1:def 9;
  end;
  assume
A5: p in T with-replacement (t,T1);
A6: p in T & not t is_a_proper_prefix_of p implies
  p in T & for s st s in {t} holds not s is_a_proper_prefix_of p
  by TARSKI:def 1;
 now
    assume
A7: ex r st r in T1 & p = t^r;
    thus ex s,r st s in {t} & r in T1 & p = s^r
    proof
      take t;
  t in {t} by TARSKI:def 1;
      hence thesis by A7;
    end;
  end;
  hence thesis by A5,A6,Def1,TREES_1:def 9;
end;

reserve T,T1 for DecoratedTree,
  P for AntiChain_of_Prefixes of dom T,
  t for Element of dom T,
  p1, p2, r1, r2 for FinSequence of NAT;

definition
  let T,P,T1;
  assume
A1: P<>{};
  func tree(T,P,T1) -> DecoratedTree means
  :Def2:
  dom it = tree(dom T, P, dom T1) & for q st q in tree(dom T, P, dom T1) holds
  (for p st p in P holds not p is_a_prefix_of q & it.q = T.q)
  or ex p,r st p in P & r in dom T1 & q = p^r & it.q = T1.r;
  existence
  proof
    defpred X[FinSequence,set] means
    (for p st p in P holds not p is_a_prefix_of $1 & $2 = T.$1) or
    ex p,r st p in P & r in dom T1 & $1 = p^r & $2 = T1.r;
A2: for q st q in tree(dom T,P,dom T1) ex x st X[q,x]
    proof
      let q;
      assume q in tree(dom T, P, dom T1);
then A3:   q in {t where t is Element of dom T :
      for p st p in P holds not p is_a_prefix_of t}
      \/ { p^s where p is Element of dom T,
      s is Element of dom T1 : p in P } by A1,Th7;
A4:   now
        assume q in {t where t is Element of dom T :
        for p st p in P holds not p is_a_prefix_of t};
        then consider t such that
A5:     q = t & for p st p in P holds not p is_a_prefix_of t;
        take x = T.t;
     for p st p in P holds not p is_a_prefix_of q & x = T.q by A5;
        hence thesis;
      end;
   now
        assume q in { p^s where p is Element of dom T,
        s is Element of dom T1 : p in P };
        then consider p being Element of dom T, s being Element of dom T1
        such that
A6:    q = p^s & p in P;
        take x = T1.s;
    (for p st p in P holds not p is_a_prefix_of q & x = T.q) or
        ex p,r st p in P & r in dom T1 & q = p^r & x = T1.r by A6;
        hence thesis;
      end;
      hence thesis by A3,A4,XBOOLE_0:def 3;
    end;
    thus ex T0 being DecoratedTree st dom T0 = tree(dom T, P, dom T1) &
    for p st p in tree(dom T, P, dom T1) holds X[p,T0.p]
    from TREES_2:sch 6(A2);
  end;
  uniqueness
  proof
    let D1,D2 be DecoratedTree such that
A7: dom D1 = tree(dom T,P,dom T1) and
A8: for q st q in tree(dom T,P,dom T1) holds
    (for p st p in P holds not p is_a_prefix_of q & D1.q = T.q) or
    ex p,r st p in P & r in dom T1 & q = p^r & D1.q = T1.r and
A9: dom D2 = tree(dom T,P,dom T1) and
A10: for q st q in tree(dom T,P,dom T1) holds
    (for p st p in P holds not p is_a_prefix_of q & D2.q = T.q) or
    ex p,r st p in P & r in dom T1 & q = p^r & D2.q = T1.r;
 now
      let q;
      assume that
A11:  q in dom D1 and
A12:  D1.q <> D2.q;
      thus contradiction
      proof
        per cases by A7,A8,A11;
        suppose
A13:      for p st p in P holds not p is_a_prefix_of q & D1.q = T.q;
      now
            per cases by A7,A10,A11;
            suppose
A14:          for p st p in P holds not p is_a_prefix_of q & D2.q = T.q;
              consider x being set such that
A15:          x in P by A1,XBOOLE_0:def 1;
          P c= dom T by TREES_1:def 11;
              then reconsider x as Element of dom T by A15;
A16:          ex p9 st p9 = x;
then           D1.q = T.q by A13,A15;
              hence contradiction by A12,A14,A15,A16;
            end;
            suppose
                        ex
 p,r st p in P & r in dom T1 & q = p^r & D2.q = T1.r;
              then consider p2,r2 such that
A17:          p2 in P and r2 in dom T1 and
A18:          q = p2^r2 and D2.q = T1.r2;
          not p2 is_a_prefix_of q by A13,A17;
              hence contradiction by A18,TREES_1:1;
            end;
          end;
          hence contradiction;
        end;
        suppose
      ex p,r st p in P & r in dom T1 & q = p^r & D1.q = T1.r;
          then consider p1,r1 such that
A19:      p1 in P and r1 in dom T1 and
A20:      q = p1^r1 and
A21:      D1.q = T1.r1;
      now
            per cases by A7,A10,A11;
            suppose
                        for
 p st p in P holds not p is_a_prefix_of q & D2.q = T.q;
then           not p1 is_a_prefix_of q by A19;
              hence contradiction by A20,TREES_1:1;
            end;
            suppose
                        ex
 p,r st p in P & r in dom T1 & q = p^r & D2.q = T1.r;
              then consider p2,r2 such that
A22:          p2 in P and r2 in dom T1 and
A23:          q = p2^r2 and
A24:          D2.q = T1.r2;
          now
                assume
A25:            p1 <> p2;
            p1,p2 are_c=-comparable by A20,A23,Th1;
                hence contradiction by A19,A22,A25,TREES_1:def 10;
              end;
              hence contradiction by A12,A20,A21,A23,A24,FINSEQ_1:33;
            end;
          end;
          hence contradiction;
        end;
      end;
    end;
    hence thesis by A7,A9,TREES_2:31;
  end;
end;

theorem Th10:
  P<>{} implies for q st q in dom tree(T,P,T1) holds
  (for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q)
  or ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r
proof
  assume
A1: P<>{};
  let q;
  assume q in dom tree(T,P,T1);
then  q in tree(dom T,P,dom T1) by A1,Def2;
  hence thesis by Def2;
end;

theorem Th11:
  p in dom T implies for q st q in dom (T with-replacement (p,T1)) holds
  not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q
  or ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r
proof
  assume
A1: p in dom T;
  let q;
  assume q in dom (T with-replacement (p,T1));
then  q in dom T with-replacement (p,dom T1) by A1,TREES_2:def 11;
  hence thesis by A1,TREES_2:def 11;
end;

theorem Th12:
  P<>{} implies for q st q in dom tree(T,P,T1) &
  q in {t1 where t1 is Element of dom T :
  for p st p in P holds not p is_a_prefix_of t1} holds tree(T,P,T1).q = T.q
proof
  assume
A1: P<>{};
  let q;
  assume that
A2: q in dom tree(T,P,T1) and
A3: q in {t1 where t1 is Element of dom T : for p st p in P holds not p
  is_a_prefix_of t1};
A4: ex t9 being Element of dom T st t9 = q & for p st p in P
  holds not p is_a_prefix_of t9 by A3;
  per cases by A2,Th10;
  suppose
A5: for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
    consider x being set such that
A6: x in P by A1,XBOOLE_0:def 1;
 P c= dom T by TREES_1:def 11;
    then reconsider x as Element of dom T by A6;
 ex p9 st p9 = x;
    hence thesis by A5,A6;
  end;
  suppose
     ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r;
    then consider p,r such that
A7: p in P and r in dom T1 and
A8: q = p^r and tree(T,P,T1).q = T1.r;
 not p is_a_prefix_of q by A4,A7;
    hence thesis by A8,TREES_1:1;
  end;
end;

theorem Th13:
  p in dom T implies for q st q in dom (T with-replacement (p,T1)) &
  q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1}
  holds T with-replacement (p,T1).q = T.q
proof
  assume
A1: p in dom T;
  let q;
  assume that
A2: q in dom (T with-replacement (p,T1)) and
A3: q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1};
  per cases by A1,A2,Th11;
  suppose
 not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
    hence thesis;
  end;
  suppose
    A4: ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r;
 ex t9 being Element of dom T st q = t9 & not p is_a_prefix_of t9 by A3;
    hence thesis by A4,TREES_1:1;
  end;
end;

theorem Th14:
  for q st q in dom tree(T,P,T1) &
  q in {p^s where p is Element of dom T, s is Element of dom T1 : p in P}
  holds ex p9 being Element of dom T, r being Element of dom T1 st
  q = p9^r & p9 in P & tree(T,P,T1).q = T1.r
proof
  let q;
  assume that
A1: q in dom tree(T,P,T1) and
A2: q in {p^s where p is Element of dom T, s is Element of dom T1 : p in P};
  per cases by A1,Th10;
  suppose
A3: for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
    consider p9 being Element of dom T, r being Element of dom T1 such that
A4: q= p9^r and
A5: p9 in P by A2;
 now
      assume tree(T,P,T1).q <> T1.r;
   not p9 is_a_prefix_of q by A3,A5;
      hence contradiction by A4,TREES_1:1;
    end;
    hence thesis by A4,A5;
  end;
  suppose
     ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r;
    then consider p,r such that
A6: p in P and
A7: r in dom T1 and
A8: q = p^r and
A9: tree(T,P,T1).q = T1.r;
    consider p9 being Element of dom T, r9 being Element of dom T1 such that
A10: q = p9^r9 and
A11: p9 in P by A2;
 now
      assume
A12:  p <> p9;
  p,p9 are_c=-comparable by A8,A10,Th1;
      hence contradiction by A6,A11,A12,TREES_1:def 10;
    end;
    hence thesis by A6,A7,A8,A9;
  end;
end;

theorem Th15:
  p in dom T implies for q st q in dom (T with-replacement (p,T1)) &
  q in {p^s where s is Element of dom T1 : s = s}
  holds ex r being Element of dom T1 st
  q = p^r & T with-replacement (p,T1).q = T1.r
proof
  assume
A1: p in dom T;
  let q;
  assume that
A2: q in dom (T with-replacement (p,T1)) and
A3: q in {p^s where s is Element of dom T1 : s = s};
  per cases by A1,A2,Th11;
  suppose
A4: not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
 ex r being Element of dom T1 st q = p^r & r = r by A3;
    hence thesis by A4,TREES_1:1;
  end;
  suppose
     ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r;
    hence thesis;
  end;
end;

theorem
  tree(T,{t},T1) = T with-replacement (t,T1)
proof
A1: dom tree(T,{t},T1) = tree(dom T,{t},dom T1) by Def2
    .= dom T with-replacement (t,dom T1) by Th9
    .= dom (T with-replacement (t,T1)) by TREES_2:def 11;
 for q st q in dom tree(T,{t},T1) holds tree(T,{t},T1).q =
  T with-replacement (t,T1).q
  proof
    let q;
    assume
A2: q in dom tree(T,{t},T1);
then A3: q in tree(dom T,{t},dom T1) by Def2;
A4: tree(dom T,{t},dom T1) = {t1 where t1 is Element of dom T :
    for p st p in {t} holds not p is_a_prefix_of t1} \/
    { p^s where p is Element of dom T, s is Element of dom T1 : p in {t} }
    by Th7;
    per cases by A3,A4,XBOOLE_0:def 3;
    suppose
A5:   q in {t1 where t1 is Element of dom T :
      for p st p in {t} holds not p is_a_prefix_of t1};
      then consider t9 being Element of dom T such that
A6:   q = t9 and
A7:   for p st p in {t} holds not p is_a_prefix_of t9;
      consider p such that
A8:   p = t;
  p in {t} by A8,TARSKI:def 1;
then A9:  not p is_a_prefix_of t9 by A7;
  q in dom (T with-replacement (t,T1)) &
      q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1}
      implies T with-replacement (t,T1).q = T.q by A8,Th13;
      hence thesis by A1,A2,A5,A6,A9,Th12;
    end;
    suppose
A10:  q in { p9^s where p9 is Element of dom T,
      s is Element of dom T1 : p9 in {t} };
      then consider p being Element of dom T, r being Element of dom T1
      such that
A11:  q = p^r and
A12:  p in {t};
A13:  q in { p^s where s is Element of dom T1 : s = s } by A11;
      consider p1 being Element of dom T, r1 being Element of dom T1 such that
A14:  q = p1^r1 and
A15:  p1 in {t} and
A16:  tree(T,{t},T1).q = T1.r1 by A2,A10,Th14;
A17:  p1 = t by A15,TARSKI:def 1;
A18:  p = t by A12,TARSKI:def 1;
then   ex r2 being Element of dom T1 st q = p^r2 & (T
      with-replacement (p,T1)).q = T1.r2 by A1,A2,A13,Th15;
      hence thesis by A14,A16,A17,A18,FINSEQ_1:33;
    end;
  end;
  hence thesis by A1,TREES_2:31;
end;

reserve D for non empty set,
  T,T1 for DecoratedTree of D,
  P for AntiChain_of_Prefixes of dom T;

definition
  let D,T,P,T1;
  assume
A1: P<>{};
  func tree(T,P,T1) -> DecoratedTree of D equals
  tree(T,P,T1);
  coherence
  proof
    set T2 = tree(T,P,T1);
 T2 is D-valued
    proof
      let y be set;
      assume y in rng T2;
      then consider x being set such that
A2:   x in dom T2 and
A3:   y = T2.x by FUNCT_1:def 3;
   x is Element of dom T2 by A2;
      then reconsider q = x as FinSequence of NAT;
   dom T2 = tree(dom T,P,dom T1) by A1,Def2;
then A4:   dom T2 = {t1 where t1 is Element of dom T :
      for p st p in P holds not p is_a_prefix_of t1}
      \/ { p^s where p is Element of dom T,
      s is Element of dom T1 : p in P } by A1,Th7;
      per cases by A2,A4,XBOOLE_0:def 3;
      suppose
A5:     q in {t1 where t1 is Element of dom T :
        for p st p in P holds not p is_a_prefix_of t1};
then A6:    tree(T,P,T1).q = T.q by A1,A2,Th12;
    now
      ex t9 being Element of dom T st q = t9 & for p st p in P
          holds not p is_a_prefix_of t9 by A5;
          hence q in dom T;
        end;
then A7:    y in rng T by A3,A6,FUNCT_1:def 3;
    rng T c= D by RELAT_1:def 19;
        hence thesis by A7;
      end;
      suppose
    q in { p^s where p is Element of dom T,
        s is Element of dom T1 : p in P };
then     ex p being Element of dom T,r being Element of dom T1 st
        q = p^r & p in P & tree(T,P,T1).q = T1.r by A2,Th14;
        hence thesis by A3;
      end;
    end;
    hence thesis;
  end;
end;