:: deftheorem Def5 defines depth CIRCUIT1:def 5 :
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for v being SortSymbol of S
for e being Element of the Sorts of (FreeEnv A) . v
for b₅ being Element of NAT holds
( b₅ = depth e iff ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b₅ = depth e9 ) );