let S be Language; :: thesis: for U being non empty set
for t being termal string of S
for I being S,b₁ -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))
let U be non empty set ; :: thesis: for t being termal string of S
for I being S,U -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))
let t be termal string of S; :: thesis: for I being S,U -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))
let I be S,U -interpreter-like Function; :: thesis: (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))
set u = the Element of U;
set TI = I -TermEval ;
set TII = (I, the Element of U) -TermEval ;
set TT = AllTermsOf S;
set F = S -firstChar ;
set s = (S -firstChar) . t;
set m = Depth t;
set T = S -termsOfMaxDepth ;
set ST = SubTerms t;
reconsider mm = Depth t, MM = (Depth t) + 1 as Element of NAT by ORDINAL1:def 12;
A1: t is (Depth t) + (0 * 1) -termal by FOMODEL1:def 40;
reconsider tm = t as Depth t -termal string of S by FOMODEL1:def 40;
reconsider tM = t as mm + 1 -termal string of S by A1;
reconsider Tm = (S -termsOfMaxDepth) . mm, TM = (S -termsOfMaxDepth) . MM as Subset of (AllTermsOf S) by FOMODEL1:2;
reconsider ttt = tm as Element of (S -termsOfMaxDepth) . mm by FOMODEL1:def 33;
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
set V = I -TermEval tt;
reconsider IM = ((I, the Element of U) -TermEval) . MM as Function of (AllTermsOf S),U ;
SubTerms tM is Tm -valued ;
then A2: ( dom ((I -TermEval) | Tm) = Tm & dom (IM | Tm) = Tm & rng (SubTerms t) c= Tm ) by RELAT_1:def 19, PARTFUN1:def 2;
(I -TermEval) . t = I -TermEval tt by Def9
.= (((I, the Element of U) -TermEval) . MM) . ttt by Def8
.= (((I, the Element of U) -TermEval) . (((Depth t) + 1) + 1)) . tm by Lm6
.= (I . ((S -firstChar) . t)) . ((((I, the Element of U) -TermEval) . MM) * (SubTerms t)) by Th3
.= (I . ((S -firstChar) . t)) . (((((I, the Element of U) -TermEval) . MM) | Tm) * (SubTerms t)) by RELAT_1:165, A2
.= (I . ((S -firstChar) . t)) . (((I -TermEval) | Tm) * (SubTerms t)) by Th20
.= (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t)) by A2, RELAT_1:165 ;
hence (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t)) ; :: thesis: verum