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 for tt being Element of AllTermsOf S holds LH . tt = RH . ttlet tt be
Element of
AllTermsOf S;
LH . tt = RH . ttconsider mm being
Element of
NAT such that A1:
tt in Tf . mm
by FOMODEL1:5;
reconsider ttt =
tt as
Element of
(S -termsOfMaxDepth) . mm by A1;
reconsider M =
mm + 1 as
Element of
NAT ;
reconsider tttt =
tt as
Element of
(S -termsOfMaxDepth) . mm by A1;
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 A2:
(f | ((S -termsOfMaxDepth) . mm)) . ttt = f . ttt
by FOMODEL0:29;
A3:
(
(id ((S -termsOfMaxDepth) . mm)) . tttt = tttt &
(id (AllTermsOf S)) . tt = tt )
;
thus LH . tt =
((S,X) -freeInterpreter) -TermEval tt
by FOMODEL2:def 10
.=
f . tt
by FOMODEL2:def 9, A1
.=
RH . tt
by A3, A2, Lm28
;
verum end;
hence
((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
by FUNCT_2:63; verum