:: deftheorem Def19 defines -TruthEval FOMODEL2:def 20 :
for S being Language
for U being non empty set
for b₃ being sequence of (PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) holds
( b₃ = (S,U) -TruthEval iff ( b₃ . 0 = S -TruthEval U & ( for mm being Element of NAT holds b₃ . (mm + 1) = ((ExIterator (b₃ . mm)) +* (NorIterator (b₃ . mm))) +* (b₃ . mm) ) ) );