:: deftheorem Def30 defines -termsOfMaxDepth FOMODEL1:def 30 :
for S being Language
for b₂ being Function holds
( b₂ = S -termsOfMaxDepth iff ( dom b₂ = NAT & b₂ . 0 = AtomicTermsOf S & ( for n being Nat holds b₂ . (n + 1) = (union { (Compound (s,(b₂ . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b₂ . n) ) ) );