let X be set ; 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; 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; 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; (((((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 S1[ Nat] means (((((S,X) -freeInterpreter),tt) -TermEval) . ($1 + 1)) | ((S -termsOfMaxDepth) . $1) = id ((S -termsOfMaxDepth) . $1);
A1:
S1[ 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;
hence
S1[
0 ]
by FUNCT_1:17, A2;
verum
end;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[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 for x being object st x in dom f holds
f . x = (id ((S -termsOfMaxDepth) . (n + 1))) . xlet x be
object ;
( x in dom f implies f . x = (id ((S -termsOfMaxDepth) . (n + 1))) . x )assume A6:
x in dom f
;
f . x = (id ((S -termsOfMaxDepth) . (n + 1))) . xthen 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
;
verum end;
hence
S1[
n + 1]
by A5, FUNCT_1:2;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
hence
(((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m)
; verum