:: TREES_A semantic presentation

begin


theorem Th1: :: TREES_A:1
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; ::_thesis: ( p ^ q = s ^ r implies p,s are_c=-comparable )
assume A1: p ^ q = s ^ r ; ::_thesis: p,s are_c=-comparable
then  ( p is_a_prefix_of s ^ r & s is_a_prefix_of p ^ q ) by TREES_1:1;
hence  p,s are_c=-comparable by A1, TREES_2:1; ::_thesis: verum
end;

definition
let T, T1 be Tree;
let P be AntiChain_of_Prefixes of T;
assume A1: P <> {} ;
func tree (T,P,T1) ->  Tree means :Def1: :: TREES_A:def 1
 for q being FinSequence of NAT holds
( q in it iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) );
existence
 ex b1 being Tree st
for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) )
proof
reconsider P9 = P as Subset of T by TREES_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_P9_holds_
x_in__{__t_where_t_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t__}_
let x be set ; ::_thesis: ( x in P9 implies x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  )
assume A1: x in P9 ; ::_thesis: x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }
then reconsider x9 = x as FinSequence by TREES_1:def_10;
reconsider x9 = x9 as Element of T by A1;
now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_x9
let p be FinSequence of NAT ; ::_thesis: ( p in P implies not b1 is_a_proper_prefix_of x9 )
assume A2: p in P ; ::_thesis: not b1 is_a_proper_prefix_of x9
percases ( p <> x9 or p = x9 ) ;
suppose p <> x9 ; ::_thesis: not b1 is_a_proper_prefix_of 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; ::_thesis: verum
end;
suppose p = x9 ; ::_thesis: not b1 is_a_proper_prefix_of x9
hence  not p is_a_proper_prefix_of x9 ; ::_thesis: verum
end;
end;
end;
hence  x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ; ::_thesis: verum
end;
then  P c=  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  by TARSKI:def_3;
then reconsider Y =  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  as non empty set by A1, XBOOLE_1:3;
consider Z being set  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: for x being set st x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  holds
( x is FinSequence of NAT & x in NAT * & x in T )
proof
let x be set ; ::_thesis: ( x in  {  t where t is Element of T : for p being FinSequence of NAT 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 ) )
assume  x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ; ::_thesis: ( x is FinSequence of NAT & x in NAT * & x in T )
then A5: ex t being Element of T st
( x = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t ) ) ;
hence  x is FinSequence of NAT ; ::_thesis: ( x in NAT * & x in T )
thus  ( x in NAT * & x in T ) by A5, FINSEQ_1:def_11; ::_thesis: verum
end;
 X is Tree-like
proof
thus  X c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for b1 being FinSequence of NAT holds
( not b1 in X or ProperPrefixes b1 c= X ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in X or not b3 <= b2 or b1 ^ <*b3*> in X ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT * )
assume  x in X ; ::_thesis: x in NAT *
then A6: ( x in  {  t where t is Element of T : for p being FinSequence of NAT 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__::_thesis:_(_x_in__{__(p_^_s)_where_p_is_Element_of_T,_s_is_Element_of_T1_:_p_in_P__}__implies_x_is_FinSequence_of_NAT_)
assume  x in  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }  ; ::_thesis: x is FinSequence of NAT
then  ex p being Element of T ex s being Element of T1 st
( x = p ^ s & p in P ) ;
hence  x is FinSequence of NAT ; ::_thesis: verum
end;
hence  x in NAT * by A4, A6, FINSEQ_1:def_11; ::_thesis: verum
end;
thus  for q being FinSequence of NAT st q in X holds
ProperPrefixes q c= X ::_thesis: for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in X or not b3 <= b2 or b1 ^ <*b3*> in X )
proof
let q be FinSequence of NAT ; ::_thesis: ( q in X implies ProperPrefixes q c= X )
assume A7: q in X ; ::_thesis: ProperPrefixes q c= X
A8: now__::_thesis:_(_q_in__{__t_where_t_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t__}__implies_ProperPrefixes_q_c=_X_)
assume A9: q in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ; ::_thesis: ProperPrefixes q c= X
then  ex t being Element of T st
( q = t & ( for p being FinSequence of NAT 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 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes q or x in X )
assume A11: x in ProperPrefixes q ; ::_thesis: x in X
then consider p1 being FinSequence such that
A12: x = p1 and
A13: p1 is_a_proper_prefix_of q by TREES_1:def_2;
reconsider p1 = p1 as Element of T by A10, A11, A12;
 for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of p1
proof
let p be FinSequence of NAT ; ::_thesis: ( p in P implies not p is_a_proper_prefix_of p1 )
assume A14: p in P ; ::_thesis: not p is_a_proper_prefix_of p1
 ex t being Element of T st
( q = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t ) ) by A9;
hence  not p is_a_proper_prefix_of p1 by A13, A14, XBOOLE_1:56; ::_thesis: verum
end;
then  x in  {  s1 where s1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s1  }  by A12;
hence  x in X by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
now__::_thesis:_(_q_in_Z_implies_ProperPrefixes_q_c=_X_)
assume  q in Z ; ::_thesis: ProperPrefixes q c= X
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 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes q or x in X )
assume A17: x in ProperPrefixes q ; ::_thesis: x in X
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__::_thesis:_(_len_p_<=_len_r_implies_r_in_X_)
assume  len p <= len r ; ::_thesis: r in X
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 = r2 as FinSequence of NAT by FINSEQ_1:18;
 r2 is_a_prefix_of s by A21, TREES_1:def_1;
then reconsider r2 = 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; ::_thesis: verum
end;
now__::_thesis:_(_len_r_<=_len_p_implies_r_in_X_)
assume  len r <= len p ; ::_thesis: r in X
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 = r3 as Element of T by TREES_1:20;
 for p9 being FinSequence of NAT st p9 in P holds
not p9 is_a_proper_prefix_of r3
proof
let p9 be FinSequence of NAT ; ::_thesis: ( p9 in P implies not p9 is_a_proper_prefix_of r3 )
assume A24: p9 in P ; ::_thesis: not p9 is_a_proper_prefix_of r3
assume A25: p9 is_a_proper_prefix_of r3 ; ::_thesis: contradiction
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;
percases ( p <> p9 or p = p9 ) ;
suppose p <> p9 ; ::_thesis: contradiction
hence  contradiction by A16, A24, A26, TREES_1:def_10; ::_thesis: verum
end;
suppose p = p9 ; ::_thesis: contradiction
hence  contradiction by A23, A25, XBOOLE_0:def_8; ::_thesis: verum
end;
end;
end;
then  r3 in  {  t where t is Element of T : for p9 being FinSequence of NAT st p9 in P holds
not p9 is_a_proper_prefix_of t  }  ;
hence  r in X by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in X by A19; ::_thesis: verum
end;
end;
hence  ProperPrefixes q c= X by A7, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
let q be FinSequence of NAT ; ::_thesis: for b1, b2 being Element of NAT holds
( not q ^ <*b1*> in X or not b2 <= b1 or q ^ <*b2*> in X )
let k, n be Element of NAT ; ::_thesis: ( not q ^ <*k*> in X or not n <= k or q ^ <*n*> in X )
assume that
A27: q ^ <*k*> in X and
A28: n <= k ; ::_thesis: q ^ <*n*> in X
A29: now__::_thesis:_(_q_^_<*k*>_in__{__t_where_t_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t__}__implies_q_^_<*n*>_in_X_)
assume A30: q ^ <*k*> in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ; ::_thesis: q ^ <*n*> in X
then  ex s being Element of T st
( q ^ <*k*> = s & ( for p being FinSequence of NAT 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__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_u
let p be FinSequence of NAT ; ::_thesis: ( p in P implies not p is_a_proper_prefix_of u )
assume A31: p in P ; ::_thesis: not p is_a_proper_prefix_of u
assume  p is_a_proper_prefix_of u ; ::_thesis: contradiction
then A32: p is_a_prefix_of q by TREES_1:9;
 ex s being Element of T st
( q ^ <*k*> = s & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s ) ) by A30;
hence  contradiction by A31, A32, TREES_1:8; ::_thesis: verum
end;
then  q ^ <*n*> in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ;
hence  q ^ <*n*> in X by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_q_^_<*k*>_in_Z_implies_q_^_<*n*>_in_X_)
assume  q ^ <*k*> in Z ; ::_thesis: q ^ <*n*> in X
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__::_thesis:_(_len_q_<=_len_p_implies_q_^_<*n*>_in_X_)
assume  len q <= len p ; ::_thesis: q ^ <*n*> in X
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__::_thesis:_(_r_=_<*k*>_implies_q_^_<*n*>_in__{__t_where_t_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t__}__)
assume A39: r = <*k*> ; ::_thesis: q ^ <*n*> in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }
then reconsider s9 = q ^ <*n*> as Element of T by A28, A36, TREES_1:def_3;
now__::_thesis:_for_p9_being_FinSequence_of_NAT_st_p9_in_P_holds_
not_p9_is_a_proper_prefix_of_s9
let p9 be FinSequence of NAT ; ::_thesis: ( p9 in P implies not p9 is_a_proper_prefix_of s9 )
assume A40: p9 in P ; ::_thesis: not p9 is_a_proper_prefix_of s9
assume A41: p9 is_a_proper_prefix_of s9 ; ::_thesis: contradiction
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 ;
percases ( p9 = p or p9 <> p ) ;
suppose p9 = p ; ::_thesis: contradiction
hence  contradiction by A41, A42, A43, TREES_1:2; ::_thesis: verum
end;
supposeA44: p9 <> p ; ::_thesis: contradiction
 ( q is_a_prefix_of p & p9 is_a_prefix_of q ) by A36, A41, TREES_1:1, TREES_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; ::_thesis: verum
end;
end;
end;
hence  q ^ <*n*> in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ; ::_thesis: verum
end;
now__::_thesis:_(_s_=_<*k*>_&_r_=_{}_implies_q_^_<*n*>_in_Z_)
assume that
A45: s = <*k*> and
A46: r = {} ; ::_thesis: q ^ <*n*> in Z
 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; ::_thesis: verum
end;
hence  q ^ <*n*> in X by A37, A38, FINSEQ_1:88, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_len_p_<=_len_q_implies_q_^_<*n*>_in_X_)
assume  len p <= len q ; ::_thesis: q ^ <*n*> in X
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 = 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; ::_thesis: verum
end;
hence  q ^ <*n*> in X by A35; ::_thesis: verum
end;
hence  q ^ <*n*> in X by A27, A29, XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider X = X as Tree ;
take  X ; ::_thesis: for q being FinSequence of NAT holds
( q in X iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) )
let q be FinSequence of NAT ; ::_thesis: ( q in X iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) )
thus  ( not q in X or ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ::_thesis: ( ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) implies q in X )
proof
assume A49: q in X ; ::_thesis: ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) )
A50: now__::_thesis:_(_not_q_in_Y_or_(_q_in_T_&_(_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_q_)_)_or_ex_p,_r_being_FinSequence_of_NAT_st_
(_p_in_P_&_r_in_T1_&_q_=_p_^_r_)_)
assume  q in Y ; ::_thesis: ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) )
then  ex s being Element of T st
( q = s & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s ) ) ;
hence  ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ; ::_thesis: verum
end;
now__::_thesis:_(_q_in_Z_implies_ex_p,_r_being_FinSequence_of_NAT_st_
(_p_in_P_&_r_in_T1_&_q_=_p_^_r_)_)
assume  q in Z ; ::_thesis: ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r )
then  ex p being Element of T ex s being Element of T1 st
( q = p ^ s & p in P ) by A3;
hence  ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ; ::_thesis: verum
end;
hence  ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) by A49, A50, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A51: ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ; ::_thesis: q in X
A52: ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) implies q in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ) ;
now__::_thesis:_(_ex_p,_r_being_FinSequence_of_NAT_st_
(_p_in_P_&_r_in_T1_&_q_=_p_^_r_)_implies_q_in_Z_)
given p, r being FinSequence of NAT  such that A53: ( p in P & r in T1 & q = p ^ r ) ; ::_thesis: q in Z
 P c= T by TREES_1:def_11;
hence  q in Z by A3, A53; ::_thesis: verum
end;
hence  q in X by A51, A52, XBOOLE_0:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Tree st ( for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds
( q in b2 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ) holds
b1 = b2
proof
let S1, S2 be Tree; ::_thesis: ( ( for q being FinSequence of NAT holds
( q in S1 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds
( q in S2 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ) implies S1 = S2 )
assume that
A54: for q being FinSequence of NAT holds
( q in S1 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) and
A55: for q being FinSequence of NAT holds
( q in S2 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ; ::_thesis: S1 = S2
let x be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not x in S1 or x in S2 ) & ( not x in S2 or x in S1 ) )
thus  ( x in S1 implies x in S2 ) ::_thesis: ( not x in S2 or x in S1 )
proof
assume A56: x in S1 ; ::_thesis: x in S2
reconsider q = x as FinSequence of NAT ;
 ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) by A54, A56;
hence  x in S2 by A55; ::_thesis: verum
end;
assume A57: x in S2 ; ::_thesis: x in S1
reconsider q = x as FinSequence of NAT ;
 ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) by A55, A57;
hence  x in S1 by A54; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines tree TREES_A:def_1_:_
 for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
for b4 being Tree holds
( b4 = tree (T,P,T1) iff for q being FinSequence of NAT holds
( q in b4 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) );

theorem Th2: :: TREES_A:2
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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
let T, T1 be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }
let P be AntiChain_of_Prefixes of T; ::_thesis: ( P <> {} implies tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
assume A1: P <> {} ; ::_thesis: tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }
thus  tree (T,P,T1) c=  {  t where t is Element of T : for p being FinSequence of NAT 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  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  c= tree (T,P,T1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in tree (T,P,T1) or x in  {  t where t is Element of T : for p being FinSequence of NAT 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  }  )
assume A2: x in tree (T,P,T1) ; ::_thesis: x in  {  t where t is Element of T : for p being FinSequence of NAT 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  }
then reconsider q = x as FinSequence of NAT by TREES_1:19;
A3: now__::_thesis:_(_ex_p,_r_being_FinSequence_of_NAT_st_
(_p_in_P_&_r_in_T1_&_q_=_p_^_r_)_implies_x_in__{__(p9_^_s)_where_p9_is_Element_of_T,_s_is_Element_of_T1_:_p9_in_P__}__)
given p, r being FinSequence of NAT  such that A4: ( p in P & r in T1 & q = p ^ r ) ; ::_thesis: x in  {  (p9 ^ s) where p9 is Element of T, s is Element of T1 : p9 in P  }
 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; ::_thesis: verum
end;
 ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) implies x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ) ;
hence  x in  {  t where t is Element of T : for p being FinSequence of NAT 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  }  by A1, A2, A3, Def1, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  or x in tree (T,P,T1) )
assume A5: x in  {  t where t is Element of T : for p being FinSequence of NAT 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  }  ; ::_thesis: x in tree (T,P,T1)
A6: now__::_thesis:_(_x_in__{__(p_^_s)_where_p_is_Element_of_T,_s_is_Element_of_T1_:_p_in_P__}__implies_x_in_tree_(T,P,T1)_)
assume  x in  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }  ; ::_thesis: x in tree (T,P,T1)
then  ex p being Element of T ex s being Element of T1 st
( x = p ^ s & p in P ) ;
hence  x in tree (T,P,T1) by Def1; ::_thesis: verum
end;
now__::_thesis:_(_x_in__{__t_where_t_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t__}__implies_x_in_tree_(T,P,T1)_)
assume  x in  {  t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t  }  ; ::_thesis: x in tree (T,P,T1)
then  ex t being Element of T st
( x = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t ) ) ;
hence  x in tree (T,P,T1) by A1, Def1; ::_thesis: verum
end;
hence  x in tree (T,P,T1) by A5, A6, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th3: :: TREES_A:3
for T being Tree
for P being AntiChain_of_Prefixes of T holds  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
proof
let T be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T holds  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
let P be AntiChain_of_Prefixes of T; ::_thesis:  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  or x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  )
assume  x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  ; ::_thesis: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
then consider t9 being Element of T such that
A1: x = t9 and
A2: for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ;
now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t9
let p be FinSequence of NAT ; ::_thesis: ( p in P implies not p is_a_proper_prefix_of t9 )
assume  p in P ; ::_thesis: not p is_a_proper_prefix_of t9
then  not p is_a_prefix_of t9 by A2;
hence  not p is_a_proper_prefix_of t9 by XBOOLE_0:def_8; ::_thesis: verum
end;
hence  x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  by A1; ::_thesis: verum
end;

theorem Th4: :: TREES_A:4
for T being Tree
for P being AntiChain_of_Prefixes of T holds P c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
proof
let T be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T holds P c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
let P be AntiChain_of_Prefixes of T; ::_thesis: P c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  )
assume A1: x in P ; ::_thesis: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
 ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT 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__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t9
let p be FinSequence of NAT ; ::_thesis: ( p in P implies not b1 is_a_proper_prefix_of t9 )
assume A3: p in P ; ::_thesis: not b1 is_a_proper_prefix_of t9
percases ( t9 = p or t9 <> p ) ;
suppose t9 = p ; ::_thesis: not b1 is_a_proper_prefix_of t9
hence  not p is_a_proper_prefix_of t9 ; ::_thesis: verum
end;
suppose t9 <> p ; ::_thesis: not b1 is_a_proper_prefix_of t9
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; ::_thesis: verum
end;
end;
end;
hence  ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 ) ) by A2; ::_thesis: verum
end;
hence  x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  ; ::_thesis: verum
end;

theorem Th5: :: TREES_A:5
for T being Tree
for P being AntiChain_of_Prefixes of T holds  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  = P
proof
let T be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T holds  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  = P
let P be AntiChain_of_Prefixes of T; ::_thesis:  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  = P
now__::_thesis:_for_x_being_set_st_x_in__{__t1_where_t1_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_proper_prefix_of_t1__}__\__{__t1_where_t1_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_prefix_of_t1__}__holds_
x_in_P
let x be set ; ::_thesis: ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  implies x in P )
assume A1: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  ; ::_thesis: x in P
then A2: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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 being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  by A1, XBOOLE_0:def_5;
assume A4: not x in P ; ::_thesis: contradiction
 ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT 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 being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t9 by A2;
now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_prefix_of_t9
let p be FinSequence of NAT ; ::_thesis: ( p in P implies not b1 is_a_prefix_of t9 )
assume A7: p in P ; ::_thesis: not b1 is_a_prefix_of t9
then A8: not p is_a_proper_prefix_of t9 by A6;
percases ( not p is_a_prefix_of t9 or p = t9 ) by A8, XBOOLE_0:def_8;
suppose not p is_a_prefix_of t9 ; ::_thesis: not b1 is_a_prefix_of t9
hence  not p is_a_prefix_of t9 ; ::_thesis: verum
end;
suppose p = t9 ; ::_thesis: not b1 is_a_prefix_of t9
hence  not p is_a_prefix_of t9 by A4, A5, A7; ::_thesis: verum
end;
end;
end;
hence  ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 ) ) by A5; ::_thesis: verum
end;
hence  contradiction by A3; ::_thesis: verum
end;
hence   {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  c= P by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: P c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  )
assume A9: x in P ; ::_thesis: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }
A10: P c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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 being FinSequence of NAT 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 being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  ; ::_thesis: contradiction
then  ex t9 being Element of T st
( x = t9 & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ) ) ;
hence  contradiction by A9; ::_thesis: verum
end;
hence  x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  by A9, A10, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th6: :: TREES_A:6
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T holds P c=  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }
proof
let T, T1 be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T holds P c=  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }
let P be AntiChain_of_Prefixes of T; ::_thesis: P c=  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }
now__::_thesis:_for_x_being_set_st_x_in_P_holds_
x_in__{__(p_^_s)_where_p_is_Element_of_T,_s_is_Element_of_T1_:_p_in_P__}_
let x be set ; ::_thesis: ( x in P implies x in  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }  )
assume A1: x in P ; ::_thesis: x in  {  (p ^ s) where p is Element of T, s is Element of T1 : p 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;
hence  x in  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }  by A1, A2; ::_thesis: verum
end;
hence  P c=  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }  by TARSKI:def_3; ::_thesis: verum
end;

theorem Th7: :: TREES_A:7
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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 T, T1 be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }
let P be AntiChain_of_Prefixes of T; ::_thesis: ( P <> {} implies tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
assume A1: P <> {} ; ::_thesis: tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }
then A2: tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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 being FinSequence of NAT 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  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in tree (T,P,T1) or x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
assume  x in tree (T,P,T1) ; ::_thesis: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }
then A3: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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__::_thesis:_(_x_in__{__t1_where_t1_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_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__}__)
percases ( x in P or not x in P ) ;
supposeA4: x in P ; ::_thesis: ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
 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 being FinSequence of NAT 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; ::_thesis: verum
end;
supposeA5: not x in P ; ::_thesis: ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
now__::_thesis:_(_x_in__{__t1_where_t1_is_Element_of_T_:_for_p_being_FinSequence_of_NAT_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__}__)
percases ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  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;
supposeA6: x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  ; ::_thesis: ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
 x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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 being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  ; ::_thesis: contradiction
  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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; ::_thesis: verum
end;
hence  ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  ) ; ::_thesis: verum
end;
suppose x in  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }  ; ::_thesis: ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  )
hence  ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  ) ; ::_thesis: verum
end;
end;
end;
hence  ( x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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  }  ) ; ::_thesis: verum
end;
end;
end;
hence  x in  {  t1 where t1 is Element of T : for p being FinSequence of NAT 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_3; ::_thesis: verum
end;
thus   {  t1 where t1 is Element of T : for p being FinSequence of NAT 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, Th3, XBOOLE_1:9; ::_thesis: verum
end;

theorem :: TREES_A:8
for T1, T being Tree
for P being AntiChain_of_Prefixes of T
for p being FinSequence of NAT st p in P holds
T1 = (tree (T,P,T1)) | p
proof
let T1, T be Tree; ::_thesis: for P being AntiChain_of_Prefixes of T
for p being FinSequence of NAT st p in P holds
T1 = (tree (T,P,T1)) | p
let P be AntiChain_of_Prefixes of T; ::_thesis: for p being FinSequence of NAT st p in P holds
T1 = (tree (T,P,T1)) | p
let p be FinSequence of NAT ; ::_thesis: ( p in P implies T1 = (tree (T,P,T1)) | p )
assume A1: p in P ; ::_thesis: T1 = (tree (T,P,T1)) | p
 ex q, r being FinSequence of NAT st
( q in P & r in T1 & p = q ^ r )
proof
consider q being FinSequence of NAT  such that
A2: q = p ;
consider r being FinSequence of NAT  such that
A3: r = <*> NAT ;
A4: r in T1 by A3, TREES_1:22;
 p = q ^ r by A2, A3, FINSEQ_1:34;
hence  ex q, r being FinSequence of NAT st
( q in P & r in T1 & p = q ^ r ) by A1, A2, A4; ::_thesis: verum
end;
then A5: p in tree (T,P,T1) by Def1;
let x be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not x in T1 or x in (tree (T,P,T1)) | p ) & ( not x in (tree (T,P,T1)) | p or x in T1 ) )
thus  ( x in T1 implies x in (tree (T,P,T1)) | p ) ::_thesis: ( not x in (tree (T,P,T1)) | p or x in T1 )
proof
assume  x in T1 ; ::_thesis: x in (tree (T,P,T1)) | p
then  p ^ x in tree (T,P,T1) by A1, Def1;
hence  x in (tree (T,P,T1)) | p by A5, TREES_1:def_6; ::_thesis: verum
end;
thus  ( x in (tree (T,P,T1)) | p implies x in T1 ) ::_thesis: verum
proof
assume  x in (tree (T,P,T1)) | p ; ::_thesis: x in T1
then A6: p ^ x in tree (T,P,T1) by A5, TREES_1:def_6;
A7: now__::_thesis:_(_p_^_x_in_T_&_(_for_r_being_FinSequence_of_NAT_st_r_in_P_holds_
not_r_is_a_proper_prefix_of_p_^_x_)_implies_x_in_T1_)
assume that
 p ^ x in T and
A8: for r being FinSequence of NAT st r in P holds
not r is_a_proper_prefix_of p ^ x ; ::_thesis: x in T1
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  x in T1 by TREES_1:22; ::_thesis: verum
end;
now__::_thesis:_(_ex_s,_r_being_FinSequence_of_NAT_st_
(_s_in_P_&_r_in_T1_&_p_^_x_=_s_^_r_)_implies_x_in_T1_)
given s, r being FinSequence of NAT  such that A10: s in P and
A11: r in T1 and
A12: p ^ x = s ^ r ; ::_thesis: x in T1
now__::_thesis:_not_s_<>_p
assume  s <> p ; ::_thesis: contradiction
then  not s,p are_c=-comparable by A1, A10, TREES_1:def_10;
hence  contradiction by A12, Th1; ::_thesis: verum
end;
hence  x in T1 by A11, A12, FINSEQ_1:33; ::_thesis: verum
end;
hence  x in T1 by A1, A6, A7, Def1; ::_thesis: verum
end;
end;

registration
let T be Tree;
cluster non empty AntiChain_of_Prefixes-like for AntiChain_of_Prefixes of T;
existence
 not for b1 being AntiChain_of_Prefixes of T holds b1 is empty
proof
set w = the Element of T;
consider X being set  such that
A1: X = { the Element of T} ;
A2: X is AntiChain_of_Prefixes-like by A1, TREES_1:36;
 X c= T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in T )
assume  x in X ; ::_thesis: x in T
then  x = the Element of T by A1, TARSKI:def_1;
hence  x in T ; ::_thesis: verum
end;
then reconsider X = X as AntiChain_of_Prefixes of T by A2, TREES_1:def_11;
take  X ; ::_thesis: not X is empty
thus  not X is empty by A1; ::_thesis: verum
end;
end;

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

theorem Th9: :: TREES_A:9
for T, T1 being Tree
for t being Element of T holds tree (T,{t},T1) = T with-replacement (t,T1)
proof
let T, T1 be Tree; ::_thesis: for t being Element of T holds tree (T,{t},T1) = T with-replacement (t,T1)
let t be Element of T; ::_thesis: tree (T,{t},T1) = T with-replacement (t,T1)
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in tree (T,{t},T1) or p in T with-replacement (t,T1) ) & ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) ) )
thus  ( p in tree (T,{t},T1) implies p in T with-replacement (t,T1) ) ::_thesis: ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) )
proof
assume A1: p in tree (T,{t},T1) ; ::_thesis: p in T with-replacement (t,T1)
A2: now__::_thesis:_(_p_in_T_&_(_for_s_being_FinSequence_of_NAT_st_s_in_{t}_holds_
not_s_is_a_proper_prefix_of_p_)_implies_(_p_in_T_&_not_t_is_a_proper_prefix_of_p_)_)
assume A3: ( p in T & ( for s being FinSequence of NAT st s in {t} holds
not s is_a_proper_prefix_of p ) ) ; ::_thesis: ( p in T & not t 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; ::_thesis: verum
end;
now__::_thesis:_(_ex_s,_r_being_FinSequence_of_NAT_st_
(_s_in_{t}_&_r_in_T1_&_p_=_s_^_r_)_implies_ex_r_being_FinSequence_of_NAT_st_
(_r_in_T1_&_p_=_t_^_r_)_)
given s being FinSequence of NAT  such that A4: ex r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r ) ; ::_thesis: ex r being FinSequence of NAT st
( r in T1 & p = t ^ r )
 s = t by A4, TARSKI:def_1;
hence  ex r being FinSequence of NAT st
( r in T1 & p = t ^ r ) by A4; ::_thesis: verum
end;
hence  p in T with-replacement (t,T1) by A1, A2, Def1, TREES_1:def_9; ::_thesis: verum
end;
assume A5: p in T with-replacement (t,T1) ; ::_thesis: p in tree (T,{t},T1)
A6: ( p in T & not t is_a_proper_prefix_of p implies ( p in T & ( for s being FinSequence of NAT st s in {t} holds
not s is_a_proper_prefix_of p ) ) ) by TARSKI:def_1;
now__::_thesis:_(_ex_r_being_FinSequence_of_NAT_st_
(_r_in_T1_&_p_=_t_^_r_)_implies_ex_s,_r_being_FinSequence_of_NAT_st_
(_s_in_{t}_&_r_in_T1_&_p_=_s_^_r_)_)
assume A7: ex r being FinSequence of NAT st
( r in T1 & p = t ^ r ) ; ::_thesis: ex s, r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r )
thus  ex s, r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r ) ::_thesis: verum
proof
take  t ; ::_thesis: ex r being FinSequence of NAT st
( t in {t} & r in T1 & p = t ^ r )
 t in {t} by TARSKI:def_1;
hence  ex r being FinSequence of NAT st
( t in {t} & r in T1 & p = t ^ r ) by A7; ::_thesis: verum
end;
end;
hence  p in tree (T,{t},T1) by A5, A6, Def1, TREES_1:def_9; ::_thesis: verum
end;


definition
let T be DecoratedTree;
let P be AntiChain_of_Prefixes of dom T;
let T1 be DecoratedTree;
assume A1: P <> {} ;
func tree (T,P,T1) ->  DecoratedTree means :Def2: :: TREES_A:def 2
( dom it = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & it . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );
existence
 ex b1 being DecoratedTree st
( dom b1 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) )
proof
defpred S1[ FinSequence, set ] means ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of $1 & $2 = T . $1 ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & $1 = p ^ r & $2 = T1 . r ) );
A2: for q being FinSequence of NAT st q in tree ((dom T),P,(dom T1)) holds
ex x being set st S1[q,x]
proof
let q be FinSequence of NAT ; ::_thesis: ( q in tree ((dom T),P,(dom T1)) implies ex x being set st S1[q,x] )
assume  q in tree ((dom T),P,(dom T1)) ; ::_thesis: ex x being set st S1[q,x]
then A3: q in  {  t where t is Element of dom T : for p being FinSequence of NAT 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__::_thesis:_(_q_in__{__t_where_t_is_Element_of_dom_T_:_for_p_being_FinSequence_of_NAT_st_p_in_P_holds_
not_p_is_a_prefix_of_t__}__implies_ex_x_being_set_ex_x_being_set_st_S1[q,x]_)
assume  q in  {  t where t is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t  }  ; ::_thesis: ex x being set ex x being set st S1[q,x]
then consider t being Element of dom T such that
A5: ( q = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t ) ) ;
take x = T . t; ::_thesis: ex x being set st S1[q,x]
 for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & x = T . q ) by A5;
hence  ex x being set st S1[q,x] ; ::_thesis: verum
end;
now__::_thesis:_(_q_in__{__(p_^_s)_where_p_is_Element_of_dom_T,_s_is_Element_of_dom_T1_:_p_in_P__}__implies_ex_x_being_set_ex_x_being_set_st_S1[q,x]_)
assume  q in  {  (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P  }  ; ::_thesis: ex x being set ex x being set st S1[q,x]
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; ::_thesis: ex x being set st S1[q,x]
 ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & x = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & x = T1 . r ) ) by A6;
hence  ex x being set st S1[q,x] ; ::_thesis: verum
end;
hence  ex x being set st S1[q,x] by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
thus  ex T0 being DecoratedTree st
( dom T0 = tree ((dom T),P,(dom T1)) & ( for p being FinSequence of NAT st p in tree ((dom T),P,(dom T1)) holds
S1[p,T0 . p] ) ) from TREES_2:sch_6(A2); ::_thesis: verum
end;
uniqueness
 for b1, b2 being DecoratedTree st dom b1 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & b2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds
b1 = b2
proof
let D1, D2 be DecoratedTree; ::_thesis: ( dom D1 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) ) & dom D2 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ) implies D1 = D2 )
assume that
A7: dom D1 = tree ((dom T),P,(dom T1)) and
A8: for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT 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 being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ; ::_thesis: D1 = D2
now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_dom_D1_holds_
not_D1_._q_<>_D2_._q
let q be FinSequence of NAT ; ::_thesis: ( q in dom D1 implies not D1 . q <> D2 . q )
assume that
A11: q in dom D1 and
A12: D1 . q <> D2 . q ; ::_thesis: contradiction
thus  contradiction ::_thesis: verum
proof
percases ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) by A7, A8, A11;
supposeA13: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A7, A10, A11;
supposeA14: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) ; ::_thesis: contradiction
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 = x as Element of dom T by A15;
A16: ex p9 being FinSequence of NAT st p9 = x ;
then  D1 . q = T . q by A13, A15;
hence  contradiction by A12, A14, A15, A16; ::_thesis: verum
end;
suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; ::_thesis: contradiction
then consider p2, r2 being FinSequence of NAT  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; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ; ::_thesis: contradiction
then consider p1, r1 being FinSequence of NAT  such that
A19: p1 in P and
 r1 in dom T1 and
A20: q = p1 ^ r1 and
A21: D1 . q = T1 . r1 ;
now__::_thesis:_contradiction
percases ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A7, A10, A11;
suppose for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) ; ::_thesis: contradiction
then  not p1 is_a_prefix_of q by A19;
hence  contradiction by A20, TREES_1:1; ::_thesis: verum
end;
suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; ::_thesis: contradiction
then consider p2, r2 being FinSequence of NAT  such that
A22: p2 in P and
 r2 in dom T1 and
A23: q = p2 ^ r2 and
A24: D2 . q = T1 . r2 ;
now__::_thesis:_not_p1_<>_p2
assume A25: p1 <> p2 ; ::_thesis: contradiction
 p1,p2 are_c=-comparable by A20, A23, Th1;
hence  contradiction by A19, A22, A25, TREES_1:def_10; ::_thesis: verum
end;
hence  contradiction by A12, A20, A21, A23, A24, FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
end;
hence  D1 = D2 by A7, A9, TREES_2:31; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines tree TREES_A:def_2_:_
 for T being DecoratedTree
for P being AntiChain_of_Prefixes of dom T
for T1 being DecoratedTree st P <> {} holds
for b4 being DecoratedTree holds
( b4 = tree (T,P,T1) iff ( dom b4 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & b4 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b4 . q = T1 . r ) ) ) ) );

theorem Th10: :: TREES_A:10
for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT holds
( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )
proof
let T, T1 be DecoratedTree; ::_thesis: for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT holds
( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )
let P be AntiChain_of_Prefixes of dom T; ::_thesis: ( P <> {} implies for q being FinSequence of NAT holds
( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ) )
assume A1: P <> {} ; ::_thesis: for q being FinSequence of NAT holds
( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )
let q be FinSequence of NAT ; ::_thesis: ( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )
assume  q in dom (tree (T,P,T1)) ; ::_thesis: ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )
then  q in tree ((dom T),P,(dom T1)) by A1, Def2;
hence  ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ) by Def2; ::_thesis: verum
end;

theorem Th11: :: TREES_A:11
for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT holds
( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )
proof
let p be FinSequence of NAT ; ::_thesis: for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT holds
( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )
let T, T1 be DecoratedTree; ::_thesis: ( p in dom T implies for q being FinSequence of NAT holds
( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ) )
assume A1: p in dom T ; ::_thesis: for q being FinSequence of NAT holds
( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )
let q be FinSequence of NAT ; ::_thesis: ( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )
assume  q in dom (T with-replacement (p,T1)) ; ::_thesis: ( ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )
then  q in (dom T) with-replacement (p,(dom T1)) by A1, TREES_2:def_11;
hence  ( ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ) by A1, TREES_2:def_11; ::_thesis: verum
end;

theorem Th12: :: TREES_A:12
for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  holds
(tree (T,P,T1)) . q = T . q
proof
let T, T1 be DecoratedTree; ::_thesis: for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  holds
(tree (T,P,T1)) . q = T . q
let P be AntiChain_of_Prefixes of dom T; ::_thesis: ( P <> {} implies for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  holds
(tree (T,P,T1)) . q = T . q )
assume A1: P <> {} ; ::_thesis: for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  holds
(tree (T,P,T1)) . q = T . q
let q be FinSequence of NAT ; ::_thesis: ( q in dom (tree (T,P,T1)) & q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  implies (tree (T,P,T1)) . q = T . 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 being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  ; ::_thesis: (tree (T,P,T1)) . q = T . q
A4: ex t9 being Element of dom T st
( t9 = q & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ) ) by A3;
percases ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ) by A2, Th10;
supposeA5: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) ; ::_thesis: (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 = x as Element of dom T by A6;
 ex p9 being FinSequence of NAT st p9 = x ;
hence  (tree (T,P,T1)) . q = T . q by A5, A6; ::_thesis: verum
end;
suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ; ::_thesis: (tree (T,P,T1)) . q = T . q
then consider p, r being FinSequence of NAT  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  (tree (T,P,T1)) . q = T . q by A8, TREES_1:1; ::_thesis: verum
end;
end;
end;

theorem Th13: :: TREES_A:13
for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT 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
let p be FinSequence of NAT ; ::_thesis: for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT 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
let T, T1 be DecoratedTree; ::_thesis: ( p in dom T implies for q being FinSequence of NAT 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 )
assume A1: p in dom T ; ::_thesis: for q being FinSequence of NAT 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
let q be FinSequence of NAT ; ::_thesis: ( 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  }  implies (T with-replacement (p,T1)) . q = T . 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  }  ; ::_thesis: (T with-replacement (p,T1)) . q = T . q
percases ( ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ) by A1, A2, Th11;
suppose ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) ; ::_thesis: (T with-replacement (p,T1)) . q = T . q
hence  (T with-replacement (p,T1)) . q = T . q ; ::_thesis: verum
end;
supposeA4: ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ; ::_thesis: (T with-replacement (p,T1)) . q = T . q
 ex t9 being Element of dom T st
( q = t9 & not p is_a_prefix_of t9 ) by A3;
hence  (T with-replacement (p,T1)) . q = T . q by A4, TREES_1:1; ::_thesis: verum
end;
end;
end;

theorem Th14: :: TREES_A:14
for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T
for q being FinSequence of NAT 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 ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )
proof
let T, T1 be DecoratedTree; ::_thesis: for P being AntiChain_of_Prefixes of dom T
for q being FinSequence of NAT 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 ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )
let P be AntiChain_of_Prefixes of dom T; ::_thesis: for q being FinSequence of NAT 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 ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )
let q be FinSequence of NAT ; ::_thesis: ( 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  }  implies ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) )
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  }  ; ::_thesis: ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )
percases ( for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ) by A1, Th10;
supposeA3: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) ; ::_thesis: ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )
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__::_thesis:_not_(tree_(T,P,T1))_._q_<>_T1_._r
assume  (tree (T,P,T1)) . q <> T1 . r ; ::_thesis: contradiction
 not p9 is_a_prefix_of q by A3, A5;
hence  contradiction by A4, TREES_1:1; ::_thesis: verum
end;
hence  ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A4, A5; ::_thesis: verum
end;
suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ; ::_thesis: ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )
then consider p, r being FinSequence of NAT  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__::_thesis:_not_p_<>_p9
assume A12: p <> p9 ; ::_thesis: contradiction
 p,p9 are_c=-comparable by A8, A10, Th1;
hence  contradiction by A6, A11, A12, TREES_1:def_10; ::_thesis: verum
end;
hence  ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A6, A7, A8, A9; ::_thesis: verum
end;
end;
end;

theorem Th15: :: TREES_A:15
for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT 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
let p be FinSequence of NAT ; ::_thesis: for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT 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 )
let T, T1 be DecoratedTree; ::_thesis: ( p in dom T implies for q being FinSequence of NAT 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 ) )
assume A1: p in dom T ; ::_thesis: for q being FinSequence of NAT 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 )
let q be FinSequence of NAT ; ::_thesis: ( q in dom (T with-replacement (p,T1)) & q in  {  (p ^ s) where s is Element of dom T1 : s = s  }  implies ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )
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  }  ; ::_thesis: ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )
percases ( ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ) by A1, A2, Th11;
supposeA4: ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) ; ::_thesis: ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )
 ex r being Element of dom T1 st
( q = p ^ r & r = r ) by A3;
hence  ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) by A4, TREES_1:1; ::_thesis: verum
end;
suppose ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ; ::_thesis: ex r being Element of dom T1 st
( 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 ) ; ::_thesis: verum
end;
end;
end;

theorem :: TREES_A:16
for T, T1 being DecoratedTree
for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)
proof
let T, T1 be DecoratedTree; ::_thesis: for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)
let t be Element of dom T; ::_thesis: tree (T,{t},T1) = T with-replacement (t,T1)
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 being FinSequence of NAT st q in dom (tree (T,{t},T1)) holds
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
proof
let q be FinSequence of NAT ; ::_thesis: ( q in dom (tree (T,{t},T1)) implies (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q )
assume A2: q in dom (tree (T,{t},T1)) ; ::_thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
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 being FinSequence of NAT 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;
percases ( q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1  }  or q in  {  (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t}  }  ) by A3, A4, XBOOLE_0:def_3;
supposeA5: q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1  }  ; ::_thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
then consider t9 being Element of dom T such that
A6: q = t9 and
A7: for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t9 ;
consider p being FinSequence of NAT  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  (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q by A1, A2, A5, A6, A9, Th12; ::_thesis: verum
end;
supposeA10: q in  {  (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t}  }  ; ::_thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
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  (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q by A14, A16, A17, A18, FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
hence  tree (T,{t},T1) = T with-replacement (t,T1) by A1, TREES_2:31; ::_thesis: verum
end;


definition
let D be non empty set ;
let T be DecoratedTree of D;
let P be AntiChain_of_Prefixes of dom T;
let T1 be DecoratedTree of D;
assume A1: P <> {} ;
func tree (T,P,T1) ->  DecoratedTree of D equals :: TREES_A:def 3
 tree (T,P,T1);
coherence
 tree (T,P,T1) is DecoratedTree of D
proof
set T2 = tree (T,P,T1);
 tree (T,P,T1) is D -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (tree (T,P,T1)) or y in D )
assume  y in rng (tree (T,P,T1)) ; ::_thesis: y in D
then consider x being set  such that
A2: x in dom (tree (T,P,T1)) and
A3: y = (tree (T,P,T1)) . x by FUNCT_1:def_3;
 x is Element of dom (tree (T,P,T1)) by A2;
then reconsider q = x as FinSequence of NAT ;
 dom (tree (T,P,T1)) = tree ((dom T),P,(dom T1)) by A1, Def2;
then A4: dom (tree (T,P,T1)) =  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT 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;
percases ( q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  or q in  {  (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P  }  ) by A2, A4, XBOOLE_0:def_3;
supposeA5: q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  ; ::_thesis: y in D
then A6: (tree (T,P,T1)) . q = T . q by A1, A2, Th12;
now__::_thesis:_q_in_dom_T
 ex t9 being Element of dom T st
( q = t9 & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ) ) by A5;
hence  q in dom T ; ::_thesis: verum
end;
then A7: y in rng T by A3, A6, FUNCT_1:def_3;
 rng T c= D by RELAT_1:def_19;
hence  y in D by A7; ::_thesis: verum
end;
suppose q in  {  (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P  }  ; ::_thesis: y in D
then  ex p being Element of dom T ex r being Element of dom T1 st
( q = p ^ r & p in P & (tree (T,P,T1)) . q = T1 . r ) by A2, Th14;
hence  y in D by A3; ::_thesis: verum
end;
end;
end;
hence  tree (T,P,T1) is DecoratedTree of D ; ::_thesis: verum
end;
end;

:: deftheorem  defines tree TREES_A:def_3_:_
 for D being non empty set
for T being DecoratedTree of D
for P being AntiChain_of_Prefixes of dom T
for T1 being DecoratedTree of D st P <> {} holds
tree (T,P,T1) = tree (T,P,T1);