:: deftheorem Def6 defines depth CIRCUIT1:def 6 :
for S being non empty non void monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for v being SortSymbol of S
for b₄ being Nat holds
( b₄ = depth (v,A) iff ex s being non empty finite Subset of NAT st
( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b₄ = max s ) );