let X be set ; :: thesis: for m being Nat
for S being Language
for tt being Element of AllTermsOf S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m)
let m be Nat; :: thesis: for S being Language
for tt being Element of AllTermsOf S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m)
let S be Language; :: thesis: for tt being Element of AllTermsOf S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m)
let tt be Element of AllTermsOf S; :: thesis: (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m)
set I = (S,X) -freeInterpreter ;
set TE = (((S,X) -freeInterpreter),tt) -TermEval ;
set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
defpred S₁[ Nat] means (((((S,X) -freeInterpreter),tt) -TermEval) . ($1 + 1)) | ((S -termsOfMaxDepth) . $1) = id ((S -termsOfMaxDepth) . $1);
A1: S₁[ 0 ]

proof

reconsider Z = 0 , O = 1 as Element of NAT ;
((((S,X) -freeInterpreter),tt) -TermEval) . O is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) ;
then ( ((((S,X) -freeInterpreter),tt) -TermEval) . O is Function of (AllTermsOf S),(AllTermsOf S) & (S -termsOfMaxDepth) . Z c= AllTermsOf S ) by FOMODEL1:2;
then reconsider f = (((((S,X) -freeInterpreter),tt) -TermEval) . 1) | ((S -termsOfMaxDepth) . 0) as Function of ((S -termsOfMaxDepth) . 0),(AllTermsOf S) by FUNCT_2:32;
A2: dom f = (S -termsOfMaxDepth) . 0 by FUNCT_2:def 1;

now :: thesis: for x being object st x in (S -termsOfMaxDepth) . 0 holds
f . x = x

let x be object ; :: thesis: ( x in (S -termsOfMaxDepth) . 0 implies f . x = x )
assume x in (S -termsOfMaxDepth) . 0 ; :: thesis: f . x = x
then reconsider xx = x as Element of (S -termsOfMaxDepth) . Z ;
reconsider t = xx as 0 -termal string of S by FOMODEL1:def 33;
thus f . x = (((((S,X) -freeInterpreter),tt) -TermEval) . (0 + 1)) . t by A2, FUNCT_1:47
.= x by Lm27 ; :: thesis: verum

end;

hence S₁[ 0 ] by FUNCT_1:17, A2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
reconsider nn = n, NN = n + 1, NNN = (n + 1) + 1 as Element of NAT by ORDINAL1:def 12;
((((S,X) -freeInterpreter),tt) -TermEval) . NNN is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) ;
then ( ((((S,X) -freeInterpreter),tt) -TermEval) . NNN is Function of (AllTermsOf S),(AllTermsOf S) & (S -termsOfMaxDepth) . NN c= AllTermsOf S ) by FOMODEL1:2;
then reconsider f = (((((S,X) -freeInterpreter),tt) -TermEval) . NNN) | ((S -termsOfMaxDepth) . NN) as Function of ((S -termsOfMaxDepth) . NN),(AllTermsOf S) by FUNCT_2:32;
A5: dom f = dom (id ((S -termsOfMaxDepth) . NN)) by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom f holds
f . x = (id ((S -termsOfMaxDepth) . (n + 1))) . x

let x be object ; :: thesis: ( x in dom f implies f . x = (id ((S -termsOfMaxDepth) . (n + 1))) . x )
assume A6: x in dom f ; :: thesis: f . x = (id ((S -termsOfMaxDepth) . (n + 1))) . x
then reconsider tt = x as Element of (S -termsOfMaxDepth) . (nn + 1) ;
reconsider t = tt as nn + 1 -termal string of S by FOMODEL1:def 33;
set s = (S -firstChar) . t;
set p = |.(ar ((S -firstChar) . t)).|;
A7: dom (X -freeInterpreter ((S -firstChar) . t)) = |.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S) by FUNCT_2:def 1;
reconsider subt = SubTerms t as (S -termsOfMaxDepth) . n -valued Function ;
reconsider subtt = subt as Element of dom (X -freeInterpreter ((S -firstChar) . t)) by FOMODEL0:16, A7;
A8: ( subtt in dom (X -freeInterpreter ((S -firstChar) . t)) & X -freeInterpreter ((S -firstChar) . t) = (((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S)) ) by Def3;
SubTerms t in (AllTermsOf S) * ;
then reconsider subttt = SubTerms t as Element of (((AllSymbolsOf S) *) \ {{}}) * ;
reconsider temp = subt null ((S -termsOfMaxDepth) . n) as Function ;
thus f . x = (((((S,X) -freeInterpreter),tt) -TermEval) . NNN) . x by A6, FUNCT_1:47
.= (((S,X) -freeInterpreter) . ((S -firstChar) . t)) . ((((((S,X) -freeInterpreter),tt) -TermEval) . (n + 1)) * (((S -termsOfMaxDepth) . n) |` subt)) by FOMODEL2:3
.= (((S,X) -freeInterpreter) . ((S -firstChar) . t)) . ((((((S,X) -freeInterpreter),tt) -TermEval) . (n + 1)) * ((id ((S -termsOfMaxDepth) . n)) * subt)) by RELAT_1:92
.= (((S,X) -freeInterpreter) . ((S -firstChar) . t)) . (((((((S,X) -freeInterpreter),tt) -TermEval) . (n + 1)) * (id ((S -termsOfMaxDepth) . n))) * subt) by RELAT_1:36
.= (((S,X) -freeInterpreter) . ((S -firstChar) . t)) . (((((((S,X) -freeInterpreter),tt) -TermEval) . (n + 1)) | ((S -termsOfMaxDepth) . n)) * subt) by RELAT_1:65
.= (((S,X) -freeInterpreter) . ((S -firstChar) . t)) . (((S -termsOfMaxDepth) . n) |` subt) by RELAT_1:92, A4
.= (X -freeInterpreter ((S -firstChar) . t)) . subt by Def4
.= (((S -firstChar) . t) -compound) . subttt by A8, FUNCT_1:47
.= ((S -firstChar) . t) -compound subttt by Def2
.= (id ((S -termsOfMaxDepth) . (n + 1))) . x by FOMODEL1:def 37 ; :: thesis: verum

end;

hence S₁[n + 1] by A5, FUNCT_1:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m) ; :: thesis: verum