trees_a.miz



    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 Nat;

    theorem :: TREES_A:1

    

     Th1: for p,q,r,s be 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;

      :: TREES_A:def1

      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 be object;

          assume

           A2: x in P9;

          then

          reconsider x9 = x as FinSequence by TREES_1:def 10;

          reconsider x9 as Element of T by A2;

          now

            let p such that

             A3: p in P;

            per cases ;

              suppose p <> x9;

              then not (p,x9) are_c=-comparable by A2, A3, TREES_1:def 10;

              hence not p is_a_proper_prefix_of x9;

            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 };

        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 be Element of T, s be 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 be object;

            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 be Element of T, s be Element of T1 : p in P } by A4, XBOOLE_0:def 3;

            now

              assume x in { (p ^ s) where p be Element of T, s be Element of T1 : p in P };

              then ex p be Element of T st ex s be 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 3;

              thus ( ProperPrefixes q) c= X

              proof

                let x be object;

                assume

                 A12: x in ( ProperPrefixes q);

                then

                consider p1 such that

                 A13: x = p1 and

                 A14: p1 is_a_proper_prefix_of q by TREES_1:def 2;

                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

                   A15: p in P;

                  ex t st q = t & for p st p in P holds not p is_a_proper_prefix_of t by A10;

                  hence thesis by A14, A15, XBOOLE_1: 56;

                end;

                then x in { s1 where s1 be 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 3;

              end;

            end;

            now

              assume q in Z;

              then

              consider p be Element of T, s be Element of T1 such that

               A16: q = (p ^ s) and

               A17: p in P by A4;

              thus ( ProperPrefixes q) c= X

              proof

                let x be object;

                assume

                 A18: x in ( ProperPrefixes q);

                then

                reconsider r = x as FinSequence by TREES_1: 11;

                r is_a_proper_prefix_of (p ^ s) by A16, A18, TREES_1: 12;

                then r is_a_prefix_of (p ^ s);

                then

                consider r1 be FinSequence such that

                 A19: (p ^ s) = (r ^ r1) by TREES_1: 1;

                 A20:

                now

                  assume ( len p) <= ( len r);

                  then

                  consider r2 be FinSequence such that

                   A21: (p ^ r2) = r by A19, FINSEQ_1: 47;

                  (p ^ s) = (p ^ (r2 ^ r1)) by A19, A21, FINSEQ_1: 32;

                  then s = (r2 ^ r1) by FINSEQ_1: 33;

                  then (s | ( dom r2)) = r2 by FINSEQ_1: 21;

                  then

                   A22: (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 A22;

                  then

                  reconsider r2 as Element of T1 by TREES_1: 20;

                  r = (p ^ r2) by A21;

                  then r in { (w ^ v) where w be Element of T, v be Element of T1 : w in P } by A17;

                  hence r in X by A4, XBOOLE_0:def 3;

                end;

                now

                  assume ( len r) <= ( len p);

                  then ex r2 be FinSequence st (r ^ r2) = p by A19, FINSEQ_1: 47;

                  then (p | ( dom r)) = r by FINSEQ_1: 21;

                  then

                   A23: (p | ( Seg ( len r))) = r by FINSEQ_1:def 3;

                  then

                  reconsider r3 = r as FinSequence of NAT by FINSEQ_1: 18;

                  

                   A24: r3 is_a_prefix_of p by A23;

                  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

                     A25: p9 in P;

                    assume

                     A26: p9 is_a_proper_prefix_of r3;

                    then p9 is_a_prefix_of r3;

                    then p9 is_a_prefix_of p by A24;

                    then

                     A27: (p,p9) are_c=-comparable ;

                    per cases ;

                      suppose p <> p9;

                      hence contradiction by A17, A25, A27, TREES_1:def 10;

                    end;

                      suppose p = p9;

                      hence contradiction by A24, A26, 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 A20;

              end;

            end;

            hence thesis by A8, A9, XBOOLE_0:def 3;

          end;

          let q, k, n such that

           A28: (q ^ <*k*>) in X and

           A29: n <= k;

           A30:

          now

            assume

             A31: (q ^ <*k*>) in { t : for p st p in P holds not p is_a_proper_prefix_of t };

            then ex s be 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 A29, TREES_1:def 3;

            now

              let p such that

               A32: p in P;

              assume p is_a_proper_prefix_of u;

              then

               A33: p is_a_prefix_of q by TREES_1: 9;

              ex s be Element of T st (q ^ <*k*>) = s & for p st p in P holds not p is_a_proper_prefix_of s by A31;

              hence contradiction by A32, A33, 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 be Element of T, s be Element of T1 such that

             A34: (q ^ <*k*>) = (p ^ s) and

             A35: p in P by A4;

             A36:

            now

              assume ( len q) <= ( len p);

              then

              consider r be FinSequence such that

               A37: (q ^ r) = p by A34, FINSEQ_1: 47;

              (q ^ <*k*>) = (q ^ (r ^ s)) by A34, A37, FINSEQ_1: 32;

              then

               A38: <*k*> = (r ^ s) by FINSEQ_1: 33;

               A39:

              now

                assume

                 A40: r = <*k*>;

                then

                reconsider s9 = (q ^ <*n*>) as Element of T by A29, A37, TREES_1:def 3;

                now

                  let p9 such that

                   A41: p9 in P;

                  assume

                   A42: p9 is_a_proper_prefix_of s9;

                  

                   A43: ( len p) = (( len q) + ( len <*k*>)) by A37, A40, 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 A42, A43, CARD_2: 102;

                  end;

                    suppose

                     A44: p9 <> p;

                    q is_a_prefix_of p & p9 is_a_prefix_of q by A37, A42, TREES_1: 1, TREES_1: 9;

                    then p9 is_a_prefix_of p;

                    then (p,p9) are_c=-comparable ;

                    hence contradiction by A35, A41, 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 A29, A45, TREES_1:def 3;

                then

                reconsider t = <*n*> as Element of T1 by FINSEQ_1: 34;

                (q ^ <*n*>) = (p ^ t) by A37, A46, FINSEQ_1: 34;

                hence (q ^ <*n*>) in Z by A4, A35;

              end;

              hence (q ^ <*n*>) in X by A38, A39, FINSEQ_1: 88, XBOOLE_0:def 3;

            end;

            now

              assume ( len p) <= ( len q);

              then

              consider r be FinSequence such that

               A47: (p ^ r) = q by A34, FINSEQ_1: 47;

              (p ^ (r ^ <*k*>)) = (p ^ s) by A34, 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 A29, A48, TREES_1:def 3;

              (q ^ <*n*>) = (p ^ t) by A47, FINSEQ_1: 32;

              then (q ^ <*n*>) in { (p9 ^ v) where p9 be Element of T, v be Element of T1 : p9 in P } by A35;

              hence (q ^ <*n*>) in X by A4, XBOOLE_0:def 3;

            end;

            hence (q ^ <*n*>) in X by A36;

          end;

          hence (q ^ <*n*>) in X by A28, A30, 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 be 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 be Element of T st ex s be 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 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 A4, 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 :: TREES_A:2

    

     Th2: P <> {} implies ( tree (T,P,T1)) = ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p be Element of T, s be 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 be Element of T, s be Element of T1 : p in P })

      proof

        let x be object;

        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 be Element of T, s be 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 object 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 be Element of T, s be Element of T1 : p in P });

       A6:

      now

        assume x in { (p ^ s) where p be Element of T, s be Element of T1 : p in P };

        then ex p be Element of T st ex s be 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 :: TREES_A:3

    

     Th3: { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } c= { t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 }

    proof

      let x be object;

      assume x in { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 };

      then

      consider t9 be Element of T such that

       A1: x = t9 and

       A2: for p st p in P holds not p is_a_prefix_of t9;

      for p st p in P holds not p is_a_proper_prefix_of t9 by A2;

      hence thesis by A1;

    end;

    theorem :: TREES_A:4

    

     Th4: P c= { t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 }

    proof

      let x be object;

      assume

       A1: x in P;

      ex t1 be 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 be 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;

          end;

        end;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    theorem :: TREES_A:5

    

     Th5: ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \ { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 }) = P

    proof

      now

        let x be object;

        assume

         A1: x in ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \ { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 });

        then

         A2: x in { t1 where t1 be 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 be 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 be Element of T st x = t1 & for p st p in P holds not p is_a_prefix_of t1

        proof

          consider t9 be 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;

              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 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \ { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 }) c= P;

      let x be object;

      assume

       A9: x in P;

      

       A10: P c= { t1 where t1 be 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 be Element of T : for p st p in P holds not p is_a_prefix_of t1 }

      proof

        assume x in { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 };

        then ex t9 be 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 :: TREES_A:6

    

     Th6: for T, T1, P holds P c= { (p ^ s) where p be Element of T, s be Element of T1 : p in P }

    proof

      let T, T1, P;

      now

        let x be object;

        assume

         A1: x in P;

        P c= T by TREES_1:def 11;

        then

        consider q be Element of T such that

         A2: q = x by A1;

        ( <*> NAT ) in T1 by TREES_1: 22;

        then

        consider s9 be Element of T1 such that

         A3: s9 = ( <*> NAT );

        q = (q ^ s9) by A3, FINSEQ_1: 34;

        hence x in { (p ^ s) where p be Element of T, s be Element of T1 : p in P } by A1, A2;

      end;

      hence thesis;

    end;

    theorem :: TREES_A:7

    

     Th7: P <> {} implies ( tree (T,P,T1)) = ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } \/ { (p ^ s) where p be Element of T, s be Element of T1 : p in P })

    proof

      assume

       A1: P <> {} ;

      then

       A2: ( tree (T,P,T1)) = ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p be Element of T, s be Element of T1 : p in P }) by Th2;

      thus ( tree (T,P,T1)) c= ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } \/ { (p ^ s) where p be Element of T, s be Element of T1 : p in P })

      proof

        let x be object;

        assume x in ( tree (T,P,T1));

        then

         A3: x in ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p be Element of T, s be Element of T1 : p in P }) by A1, Th2;

        now

          per cases ;

            suppose

             A4: x in P;

            P c= { (p ^ s) where p be Element of T, s be Element of T1 : p in P } by Th6;

            hence x in { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } or x in { (p ^ s) where p be Element of T, s be 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 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 };

                x in { t1 where t1 be 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 be Element of T : for p st p in P holds not p is_a_prefix_of t1 };

                  ({ t1 where t1 be Element of T : for p st p in P holds not p is_a_proper_prefix_of t1 } \ { t1 where t1 be 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 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } or x in { (p ^ s) where p be Element of T, s be Element of T1 : p in P };

              end;

                suppose x in { (p ^ s) where p be Element of T, s be Element of T1 : p in P };

                hence x in { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } or x in { (p ^ s) where p be Element of T, s be Element of T1 : p in P };

              end;

            end;

            hence x in { t1 where t1 be Element of T : for p st p in P holds not p is_a_prefix_of t1 } or x in { (p ^ s) where p be Element of T, s be 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 :: TREES_A:8

    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

          .= (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 be 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 object;

          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;

      :: original: {

      redefine

      func {t} -> AntiChain_of_Prefixes of T ;

      correctness by TREES_1: 39;

    end

    theorem :: TREES_A:9

    

     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 <> {} ;

      :: TREES_A:def2

      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))) holds 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 be Element of ( dom T) : for p st p in P holds not p is_a_prefix_of t } \/ { (p ^ s) where p be Element of ( dom T), s be Element of ( dom T1) : p in P }) by A1, Th7;

           A4:

          now

            assume q in { t where t be 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 be Element of ( dom T), s be Element of ( dom T1) : p in P };

            then

            consider p be Element of ( dom T), s be 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 be 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 be object 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 :: TREES_A:10

    

     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 :: TREES_A:11

    

     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 :: TREES_A:12

    

     Th12: P <> {} implies for q st q in ( dom ( tree (T,P,T1))) & q in { t1 where t1 be 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 be Element of ( dom T) : for p st p in P holds not p is_a_prefix_of t1 };

      

       A4: ex t9 be 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 be object 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 :: TREES_A:13

    

     Th13: p in ( dom T) implies for q st q in ( dom (T with-replacement (p,T1))) & q in { t1 where t1 be 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 be 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 be 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 :: TREES_A:14

    

     Th14: for q st q in ( dom ( tree (T,P,T1))) & q in { (p ^ s) where p be Element of ( dom T), s be Element of ( dom T1) : p in P } holds ex p9 be Element of ( dom T), r be 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 be Element of ( dom T), s be 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 be Element of ( dom T), r be Element of ( dom T1) such that

         A4: q = (p9 ^ r) and

         A5: p9 in P by A2;

        (( tree (T,P,T1)) . q) = (T1 . r) by A4, TREES_1: 1, A3, A5;

        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 be Element of ( dom T), r9 be 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 :: TREES_A:15

    

     Th15: p in ( dom T) implies for q st q in ( dom (T with-replacement (p,T1))) & q in the set of all (p ^ s) where s be Element of ( dom T1) holds ex r be 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 the set of all (p ^ s) where s be Element of ( dom T1);

      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 be Element of ( dom T1) st q = (p ^ 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 :: TREES_A:16

    ( 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 be Element of ( dom T) : for p st p in {t} holds not p is_a_prefix_of t1 } \/ { (p ^ s) where p be Element of ( dom T), s be 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 be Element of ( dom T) : for p st p in {t} holds not p is_a_prefix_of t1 };

          then

          consider t9 be 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 be 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 be Element of ( dom T), s be Element of ( dom T1) : p9 in {t} };

          then

          consider p be Element of ( dom T), r be Element of ( dom T1) such that

           A11: q = (p ^ r) and

           A12: p in {t};

          

           A13: q in the set of all (p ^ s) where s be Element of ( dom T1) by A11;

          consider p1 be Element of ( dom T), r1 be 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 be 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 non empty AntiChain_of_Prefixes of ( dom T);

    registration

      let D, T, P, T1;

      cluster ( tree (T,P,T1)) -> D -valued;

      coherence

      proof

        set T2 = ( tree (T,P,T1));

        let y be object;

        assume y in ( rng T2);

        then

        consider x be object 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 Def2;

        then

         A4: ( dom T2) = ({ t1 where t1 be Element of ( dom T) : for p st p in P holds not p is_a_prefix_of t1 } \/ { (p ^ s) where p be Element of ( dom T), s be Element of ( dom T1) : p in P }) by Th7;

        per cases by A2, A4, XBOOLE_0:def 3;

          suppose

           A5: q in { t1 where t1 be 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 A2, Th12;

          now

            ex t9 be 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 be Element of ( dom T), s be Element of ( dom T1) : p in P };

          then ex p be Element of ( dom T), r be 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;

    end