for m being Nat
for S being Language
for U being non empty set
for u being Element of U
for I being b₂,b₃ -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)