:: deftheorem Def8 defines -TermEval FOMODEL2:def 9 :
for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function
for t being Element of AllTermsOf S
for b₅ being Element of U holds
( b₅ = I -TermEval t iff for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b₅ = (((I,u1) -TermEval) . (mm + 1)) . t );