:: deftheorem defines depth MSAFREE2:def 14 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for v being SortSymbol of S
for e being Element of the Sorts of (FreeMSA X) . v
for b₅ being Nat holds
( b₅ = depth e iff ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & b₅ = height t ) );