scheme :: TREES_2:sch 10
DTreeStructEx{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ 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 : P₁[k,T . t] } & ( for n being Nat st P₁[n,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 & P₁[k2,d] holds
P₁[k1,d]