:: deftheorem Def3 defines -flat_tree TREES_4:def 3 :
for x being object
for p being FinSequence
for b₃ being DecoratedTree holds
( b₃ = x -flat_tree p iff ( dom b₃ = elementary_tree (len p) & b₃ . {} = x & ( for n being Nat st n < len p holds
b₃ . <*n*> = p . (n + 1) ) ) );