:: 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 b₄ being DecoratedTree holds
( b₄ = tree (T,P,T1) iff ( dom b₄ = 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 & b₄ . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b₄ . q = T1 . r ) ) ) ) );