let X be set ; for S being Language holds ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
let S be Language; ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
set u = the Element of AllTermsOf S;
set I = (S,X) -freeInterpreter ;
set TE = (((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval ;
set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
reconsider Tf = S -termsOfMaxDepth as Function ;
reconsider LH = ((S,X) -freeInterpreter) -TermEval , RH = id (AllTermsOf S) as Function of (AllTermsOf S),(AllTermsOf S) ;
now let tt be
Element of
AllTermsOf S;
LH . tt = RH . ttconsider mm being
Element of
NAT such that C0:
tt in Tf . mm
by FOMODEL1:5;
reconsider ttt =
tt as
Element of
(S -termsOfMaxDepth) . mm by C0;
reconsider M =
mm + 1 as
Element of
NAT ;
reconsider tttt =
tt as
Element of
(S -termsOfMaxDepth) . mm by C0;
set uv =
((S,X) -freeInterpreter) -TermEval tt;
((((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval) . M is
Element of
Funcs (
(AllTermsOf S),
(AllTermsOf S))
;
then reconsider f =
((((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval) . (mm + 1) as
Function of
(AllTermsOf S),
(AllTermsOf S) ;
((f | ((S -termsOfMaxDepth) . mm)) . ttt) \+\ (f . ttt) = {}
;
then C1:
(f | ((S -termsOfMaxDepth) . mm)) . ttt = f . ttt
by FOMODEL0:29;
(
{((id ((S -termsOfMaxDepth) . mm)) . tttt)} \ {tttt} = {} &
{((id (AllTermsOf S)) . tt)} \ {tt} = {} )
;
then C2:
(
(id ((S -termsOfMaxDepth) . mm)) . tttt = tttt &
(id (AllTermsOf S)) . tt = tt )
by ZFMISC_1:15;
thus LH . tt =
((S,X) -freeInterpreter) -TermEval tt
by FOMODEL2:def 10
.=
f . tt
by C0, FOMODEL2:def 9
.=
RH . tt
by C2, C1, Lm30
;
verum end;
hence
((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
by FUNCT_2:63; verum