scheme :: TREES_2:sch 8
DTreeStructEx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> set , F₄() -> Function of [:F₁(),NAT:],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in F₃((T . t)) } & ( for n being Nat st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) ) ) )

provided

A1: for d being Element of F₁()
for k1, k2 being Nat st k1 <= k2 & k2 in F₃(d) holds
k1 in F₃(d)