The Mizar article:

Replacement of Subtrees in a Tree

by
Oleg Okhotnikov

Received October 1, 1995

Copyright (c) 1995 Association of Mizar Users

MML identifier: TREES_A
[ MML identifier index ]


environ

 vocabulary TREES_1, FINSEQ_1, ZFMISC_1, BOOLE, TREES_3, RELAT_1, TREES_2,
      FUNCT_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1,
      FUNCT_1, FINSEQ_1, TREES_1, TREES_2;
 constructors NAT_1, TREES_2, XREAL_0, MEMBERED;
 clusters SUBSET_1, TREES_2, RELSET_1, ARYTM_3, XBOOLE_0, MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, TREES_1, TREES_2;
 theorems TARSKI, FUNCT_1, FINSEQ_1, RLVECT_1, TREES_1, TREES_2, XBOOLE_0,
      XBOOLE_1;
 schemes TREES_2;

begin

reserve T, T1 for Tree,
        P for AntiChain_of_Prefixes of T,
        p1 for FinSequence,
        p, q, r, s, p' for FinSequence of NAT,
        x, Z for set,
        t for Element of T,
        k, n for 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 A2: p is_a_prefix_of s^r by TREES_1:8;
    s is_a_prefix_of p^q by A1,TREES_1:8;
  hence p,s are_c=-comparable by A1,A2,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 P' = P as Subset of T by TREES_1:def 14;
      now let x; assume A2: x in P';
      then reconsider x' = x as FinSequence by TREES_1:def 13;
      reconsider x' as Element of T by A2;
        now let p such that A3: p in P;
        per cases;
          suppose p <> x';
          then not p,x' are_c=-comparable by A2,A3,TREES_1:def 13;
          hence not p is_a_proper_prefix_of x' by XBOOLE_1:104;
          suppose p = x';
          hence not p is_a_proper_prefix_of x';
      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 A4:
      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;
A5:   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 A6:      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 A6,FINSEQ_1:def 11;
       end;
      X is Tree-like
      proof
        thus X c= NAT*
          proof let x; assume x in X;
then A7:          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 A4,XBOOLE_0:def 2;
              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 A5,A7,FINSEQ_1:def 11;
          end;
        thus for q st q in X holds ProperPrefixes q c= X
          proof let q such that A8: q in X;
A9:          now assume
              A10: 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 A11:       ProperPrefixes q c= T by TREES_1:def 5;
              thus ProperPrefixes q c= X
                proof let x; assume
A12:               x in ProperPrefixes q;
                  then consider p1 such that
A13:               x = p1 & p1 is_a_proper_prefix_of q by TREES_1:def 4;
                  reconsider p1 as Element of T by A11,A12,A13;
                    for p st p in P holds not p is_a_proper_prefix_of p1
                    proof let p such that A14: p in P;
                      consider t such that A15: q = t & for p st p in P holds
                        not p is_a_proper_prefix_of t by A10;
                        q = t & not p is_a_proper_prefix_of t by A14,A15;
                      hence not p is_a_proper_prefix_of p1 by A13,TREES_1:27;
                    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 A13;
                  hence thesis by XBOOLE_0:def 2;
                end;
            end;
              now assume q in Z;
              then consider p being Element of T, s being Element of T1 such
that
A16:              q = p^s & p in P by A4;
              thus ProperPrefixes q c= X
                proof let x; assume
A17:                x in ProperPrefixes q;
                  then reconsider r = x as FinSequence by TREES_1:35;
                    r is_a_proper_prefix_of p^s by A16,A17,TREES_1:36;
                  then r is_a_prefix_of p^s & r <> p^s by XBOOLE_0:def 8;
                  then consider r1 being FinSequence such that
A18:                  p^s = r^r1 by TREES_1:8;
A19:               now assume len p <= len r;
                    then consider r2 being FinSequence such that
A20:                 p^r2 = r by A18,FINSEQ_1:64;
                      p^s = p^(r2^r1) by A18,A20,FINSEQ_1:45;
                    then s = r2^r1 by FINSEQ_1:46;
                    then s|(dom r2) = r2 by RLVECT_1:105;
then A21:                 s|Seg(len r2) = r2 by FINSEQ_1:def 3;
                    then reconsider r2 as FinSequence of NAT by FINSEQ_1:23;
                      r2 is_a_prefix_of s & s in T1 by A21,TREES_1:def 1;
                    then reconsider r2 as Element of T1 by TREES_1:45;
                      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 A4,XBOOLE_0:def 2;
                  end;
                    now assume len r <= len p;
                    then ex r2 being FinSequence st
                      r^r2 = p by A18,FINSEQ_1:64;
                    then p|(dom r) = r by RLVECT_1:105;
then A22:            p|Seg(len r) = r by FINSEQ_1:def 3;
                    then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:23
;
A23:                r3 is_a_prefix_of p by A22,TREES_1:def 1;
                    then reconsider r3 as Element of T by TREES_1:45;
                  for p' st p' in P holds not p' is_a_proper_prefix_of r3
                      proof let p'; assume A24: p' in P;
                        assume A25: p' is_a_proper_prefix_of r3;
                        then p' is_a_prefix_of r3 by XBOOLE_0:def 8;
                        then p' is_a_prefix_of p by A23,XBOOLE_1:1;
then A26:                   p,p' are_c=-comparable by XBOOLE_0:def 9;
                        per cases;
                          suppose p<>p';
                          hence contradiction by A16,A24,A26,TREES_1:def 13;
                          suppose p=p';
                          hence contradiction by A23,A25,TREES_1:28;
                      end;
                    then r3 in { t : for p' st p' in P holds
                      not p' is_a_proper_prefix_of t };
                    hence r in X by XBOOLE_0:def 2;
                  end;
                  hence thesis by A19;
                end;
            end;
            hence thesis by A8,A9,XBOOLE_0:def 2;
          end;
        let q,k,n such that
A27:        q^<*k*> in X & n <= k;
A28:      now assume A29: 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 A27,TREES_1:def 5;
            now let p such that A30: p in P; assume p is_a_proper_prefix_of u;
            then A31: p is_a_prefix_of q by TREES_1:32;
            consider s being Element of T such that A32:
              q^<*k*> = s & for p st p in P holds
                 not p is_a_proper_prefix_of s by A29;
              not p is_a_proper_prefix_of s by A30,A32;
            hence contradiction by A31,A32,TREES_1:31;
          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 2;
        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 & p in P by A4;
A34:        now assume len q <= len p;
            then consider r being FinSequence such that
A35:         q^r = p by A33,FINSEQ_1:64;
              q^<*k*> = q^(r^s) by A33,A35,FINSEQ_1:45;
then A36:            <*k*> = r^s by FINSEQ_1:46;
A37:         now assume
A38:           r = <*k*>;
              then reconsider s' = q^<*n*> as Element of T by A27,A35,TREES_1:
def 5;
                now let p' such that A39: p' in P;
                assume A40: p' is_a_proper_prefix_of s';
then A41:             p' is_a_prefix_of s' & p' <> s' by XBOOLE_0:def 8;
A42:             len p = len q + len <*k*> by A35,A38,FINSEQ_1:35
                     .= len q + 1 by FINSEQ_1:57
                     .= len q + len <*n*> by FINSEQ_1:57
                     .= len s' by FINSEQ_1:35;
                per cases;
                  suppose p' = p;
                  hence contradiction by A41,A42,TREES_1:15;
                  suppose A43: p' <> p;
A44:               q is_a_prefix_of p by A35,TREES_1:8;
                    p' is_a_prefix_of q by A40,TREES_1:32;
                  then p' is_a_prefix_of p by A44,XBOOLE_1:1;
                  then p,p' are_c=-comparable by XBOOLE_0:def 9;
                  hence contradiction by A33,A39,A43,TREES_1:def 13;
              end;
              hence q^<*n*> in { t : for p st p in P holds
                not p is_a_proper_prefix_of t };
            end;
              now assume
A45:           s = <*k*> & r = {};
                s = <*>NAT^s & s in T1 & {} = <*> NAT
                by FINSEQ_1:47;
              then <*>NAT^<*n*> in T1 by A27,A45,TREES_1:def 5;
              then reconsider t = <*n*> as Element of T1 by FINSEQ_1:47;
                q^<*n*> = p^t by A35,A45,FINSEQ_1:47; hence q^<*n*> in
 Z by A4,A33;
            end;
            hence q^<*n*> in X by A36,A37,TREES_1:6,XBOOLE_0:def 2;
          end;
            now assume len p <= len q;
            then consider r being FinSequence such that
A46:         p^r = q by A33,FINSEQ_1:64;
              p^(r^<*k*>) = p^s by A33,A46,FINSEQ_1:45;
then A47:         r^<*k*> = s & s in T1 by FINSEQ_1:46;
            then s|dom r = r by RLVECT_1:105;
            then s|Seg len r = r by FINSEQ_1:def 3;
            then reconsider r as FinSequence of NAT by FINSEQ_1:23;
            reconsider t = r^<*n*> as Element of T1 by A27,A47,TREES_1:def 5;
              q^<*n*> = p^t by A46,FINSEQ_1:45;
            then q^<*n*> in { p'^v where p' is Element of T,
              v is Element of T1 : p' in P } by A33;
            hence q^<*n*> in X by A4,XBOOLE_0:def 2;
          end;
          hence q^<*n*> in X by A34;
        end;
        hence q^<*n*> in X by A27,A28,XBOOLE_0:def 2;
      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 A48: q in X;
A49:      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 A4;
          hence ex p,r st p in P & r in T1 & q = p^r;
        end;
        hence thesis by A48,A49,XBOOLE_0:def 2;
      end;
    assume
A50:    (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;
A51:  (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
A52:    p in P & r in T1 & q = p^r; P c= T by TREES_1:def 14;
      hence q in Z by A4,A52;
    end;
    hence thesis by A50,A51,XBOOLE_0:def 2;
  end;
uniqueness
   proof let S1,S2 be Tree such that
A53:  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
A54:  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
A55:      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 A53,A55;
       hence thesis by A54;
      end;
    assume
A56:    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 A54,A56;
    hence thesis by A53;
   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:44;
A3:    now given p,r such that
A4:      p in P & r in T1 & q = p^r; P c= T by TREES_1:def 14;
        hence x in { p'^s where p' is Element of T,
          s is Element of T1 : p' 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 2;
    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 2;
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 t' being Element of T such that A1: x = t' &
    for p st p in P holds not p is_a_prefix_of t';
    now let p; assume p in P; then not p is_a_prefix_of t' by A1;
    hence not p is_a_proper_prefix_of t' by XBOOLE_0:def 8;
  end;
  hence x in {t1 where t1 is Element of T :
     for p st p in P holds not p is_a_proper_prefix_of t1} 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 14;
      then consider t' being Element of T such that A2: t' = x by A1;
        now let p such that A3: p in P;
        per cases;
          suppose t' = p;
          hence not p is_a_proper_prefix_of t';
          suppose t' <> p;
            then not t', p are_c=-comparable by A1,A2,A3,TREES_1:def 13;
          hence not p is_a_proper_prefix_of t' by XBOOLE_1:104;
      end;
      hence thesis by A2;
    end;
  hence x in {t1 where t1 is Element of T :
    for p st p in P holds not p is_a_proper_prefix_of t1};
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
      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 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} &
      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 XBOOLE_0:def 4;
    assume A2: 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 t' being Element of T such that A3: x = t' &
          for p st p in P holds not p is_a_proper_prefix_of t' by A1;
          now let p; assume A4: p in P;
          then A5: not p is_a_proper_prefix_of t' by A3;
          per cases by A5,XBOOLE_0:def 8;
            suppose not p is_a_prefix_of t';
            hence not p is_a_prefix_of t';
            suppose p = t';
            hence not p is_a_prefix_of t' by A2,A3,A4;
        end;
        hence thesis by A3;
      end;
    hence contradiction by A1;
  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 A6: x in P;
  A7: 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 consider t' being Element of T such that A8: x = t' &
        for p st p in P holds not p is_a_prefix_of t';
      thus contradiction by A6,A8;
    end;
  hence 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} by A6,A7,XBOOLE_0:def 4;
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 14;
    then consider q being Element of T such that A2: q = x by A1; <*> NAT in
T1 by TREES_1:47;
    then consider s' being Element of T1 such that A3: s' = <*> NAT;
      q = q^s' by A3,FINSEQ_1:47;
    hence x in { p^s where p is Element of T, s is Element of T1 : p in P }
      by A1,A2;
  end;
  hence P c= { p^s where p is Element of T, s is Element of T1 : p in P }
    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;
        suppose A5: not x in P;
          now per cases by A3,XBOOLE_0:def 2;
          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 4;
              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 };
          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;
        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;
      hence x in {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 }
          by XBOOLE_0:def 2;
    end;
    {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} by Th3;
  hence {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 }
      c= tree(T,P,T1) by A2,XBOOLE_1:9;
end;

canceled;

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:47; p = q^r by A2,A3,FINSEQ_1:47;
      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 9;
    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 9;
A7:    now assume
        p^x in T & for r st r in P holds not r is_a_proper_prefix_of p^x;
        then A8: not p is_a_proper_prefix_of p^x by A1;
          p is_a_prefix_of p^x by TREES_1:8;
        then p^x = p by A8,XBOOLE_0:def 8 .= p^<*>NAT by FINSEQ_1:47;
        then x = {} by FINSEQ_1:46;
        hence x in T1 by TREES_1:47;
      end;
        now given s,r such that
A9:      s in P & r in T1 & p^x = s^r;
          now assume s <> p;
          then not s,p are_c=-comparable by A1,A9,TREES_1:def 13;
          hence contradiction by A9,Th1;
        end;
        hence x in T1 by A9,FINSEQ_1:46;
      end;
      hence thesis by A1,A6,A7,Def1;
    end;
end;

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

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

theorem Th10:
  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 p in T with-replacement (t,T1) by A1,A2,Def1,TREES_1:def 12;
    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 p in tree(T,{t},T1) by A5,A6,Def1,TREES_1:def 12;
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 2;
      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 DTreeEx(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
A11:    q in dom D1 & D1.q <> D2.q;
      thus contradiction
        proof
          per cases by A7,A8,A11;
            suppose A12: 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 A13: for p st p in P holds
                    not p is_a_prefix_of q & D2.q = T.q;
                  consider x being set such that A14: x in P by A1,XBOOLE_0:def
1;
                    P c= dom T by TREES_1:def 14;
                  then reconsider x as Element of dom T by A14;
                  consider p' such that A15: p' = x;
                 D1.q = T.q by A12,A14,A15;
                hence contradiction by A11,A13,A14,A15;
                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
A16:                  p2 in P & r2 in dom T1 & q = p2^r2 & D2.q = T1.r2;
                    not p2 is_a_prefix_of q by A12,A16;
                hence contradiction by A16,TREES_1:8;
            end;
            hence contradiction;
            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
A17:              p1 in P & r1 in dom T1 & q = p1^r1 & 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 A17;
                hence contradiction by A17,TREES_1:8;
                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
A18:                  p2 in P & r2 in dom T1 & q = p2^r2 & D2.q = T1.r2;
                    now assume A19: p1 <> p2;
                      p1,p2 are_c=-comparable by A17,A18,Th1;
                    hence contradiction by A17,A18,A19,TREES_1:def 13;
                  end;
                hence contradiction by A11,A17,A18,FINSEQ_1:46;
            end;
            hence contradiction;
        end;
    end;
    hence thesis by A7,A9,TREES_2:33;
  end;
end;

canceled 2;

theorem Th13:
  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 Th14:
  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 12;
  hence thesis by A1,TREES_2:def 12;
end;

theorem Th15:
  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 A2: 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};
  then consider t' being Element of dom T such that A3: t' = q &
    for p st p in P holds not p is_a_prefix_of t';
  per cases by A2,Th13;
    suppose
A4:    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 A5: x in P by A1,XBOOLE_0:def 1;
        P c= dom T by TREES_1:def 14;
      then reconsider x as Element of dom T by A5;
      consider p' such that A6: p' = x;
    thus tree(T,P,T1).q = T.q by A4,A5,A6;
    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 & r in dom T1 & q = p^r &
        tree(T,P,T1).q = T1.r;
      not p is_a_prefix_of q by A3,A7;
      hence tree(T,P,T1).q = T.q by A7,TREES_1:8;
end;

theorem Th16:
  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 A2: 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};
  per cases by A1,A2,Th14;
    suppose not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
    hence T with-replacement (p,T1).q = T.q;
    suppose ex r st r in dom T1 & q = p^r &
      T with-replacement (p,T1).q = T1.r;
      then consider r such that
      A3: r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r;
      consider t' being Element of dom T such that A4: q = t' &
        not p is_a_prefix_of t' by A2;
    thus T with-replacement (p,T1).q = T.q by A3,A4,TREES_1:8;
end;

theorem Th17:
  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 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
proof let q; assume A1: 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};
  per cases by A1,Th13;
    suppose
A2:    for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
      consider p' being Element of dom T, r being Element of dom T1
        such that A3: q= p'^r & p' in P by A1;
        now assume tree(T,P,T1).q <> T1.r;
          not p' is_a_prefix_of q by A2,A3;
        hence contradiction by A3,TREES_1:8;
      end;
    hence 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 A3;
    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
A4:      p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r;
      consider p' being Element of dom T, r' being Element of dom T1
        such that A5: q = p'^r' & p' in P by A1;
        now assume A6: p <> p';
          p,p' are_c=-comparable by A4,A5,Th1;
        hence contradiction by A4,A5,A6,TREES_1:def 13;
      end;
    hence 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 A4;
end;

theorem Th18:
  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 A2: q in dom (T with-replacement (p,T1)) &
    q in {p^s where s is Element of dom T1 : s = s};
  per cases by A1,A2,Th14;
    suppose A3: not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
      consider r being Element of dom T1 such that A4: q = p^r & r = r by A2;
    thus ex r being Element of dom T1 st q = p^r &
     T with-replacement (p,T1).q = T1.r by A3,A4,TREES_1:8;
    suppose ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r
;
    hence ex r being Element of dom T1 st q = p^r &
      T with-replacement (p,T1).q = T1.r;
end;

theorem
    tree(T,{t},T1) = T with-replacement (t,T1)
proof
A1:dom tree(T,{t},T1) = dom (T with-replacement (t,T1))
    proof
        dom tree(T,{t},T1) = tree(dom T,{t},dom T1) by Def2
                      .= dom T with-replacement (t,dom T1) by Th10
                      .= dom (T with-replacement (t,T1)) by TREES_2:def 12;
      hence thesis;
    end;
    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 2;
      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 t' being Element of dom T such that A6: q = t' &
          for p st p in {t} holds not p is_a_prefix_of t';
        consider p such that A7: p = t; p in {t} by A7,TARSKI:def 1;
        then A8: not p is_a_prefix_of t' by A6;
          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 A7,Th16;
      hence tree(T,{t},T1).q = T with-replacement (t,T1).q by A1,A2,A5,A6,A8,
Th15;
      suppose A9: q in { p'^s where p' is Element of dom T,
          s is Element of dom T1 : p' in {t} };
        then consider p being Element of dom T, r being Element of dom T1
          such that A10: q = p^r & p in {t};
A11:    q in { p^s where s is Element of dom T1 : s = s } by A10;
      consider p1 being Element of dom T, r1 being Element of dom T1
        such that A12: q = p1^r1 & p1 in {t} & tree(T,{t},T1).q = T1.r1 by A2,
A9,Th17;
A13:   p1 = t & p = t by A10,A12,TARSKI:def 1;
      then consider r2 being Element of dom T1
        such that A14: q = p^r2 & (T with-replacement (p,T1)).q = T1.r2
         by A1,A2,A11,Th18;
      thus tree(T,{t},T1).q = T with-replacement (t,T1).q by A12,A13,A14,
FINSEQ_1:46;
    end;
  hence tree(T,{t},T1) = T with-replacement (t,T1) by A1,TREES_2:33;
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
    consider T2 being DecoratedTree such that A2: T2 = tree(T,P,T1);
      T2 is ParametrizedSubset of D
      proof
        thus rng T2 c= D
          proof let y be set; assume y in rng T2;
            then consider x being set such that
A3:            x in dom T2 & y = T2.x by FUNCT_1:def 5;
                x is Element of dom T2 by A3;
            then reconsider q = x as FinSequence of NAT;
              dom T2 = tree(dom T,P,dom T1) by A1,A2,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 A3,A4,XBOOLE_0:def 2;
              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,A3,Th15;
                  now
                  consider t' being Element of dom T such that A7: q = t' &
                    for p st p in P holds not p is_a_prefix_of t' by A5;
                  thus q in dom T by A7;
                end;
then A8:              y in rng T by A2,A3,A6,FUNCT_1:def 5;
                  rng T c= D by TREES_2:def 9;
              hence y in D by A8;
              suppose 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,r being Element of dom
T1
                  such that A9: q = p^r & p in P &
                  tree(T,P,T1).q = T1.r by A2,A3,Th17;
              thus y in D by A2,A3,A9;
          end;
      end;
    hence thesis by A2;
  end;
end;


Back to top