:: deftheorem Def7 defines -TermEval FOMODEL2:def 8 :
for S being Language
for U being non empty set
for u being Element of U
for I being b₁,b₂ -interpreter-like Function
for b₅ being sequence of (Funcs ((AllTermsOf S),U)) holds
( b₅ = (I,u) -TermEval iff ( b₅ . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b₅ . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b₅ . mm),(S -subTerms)____ ) ) );