let X be set ; for U being non empty set
for S being Language
for l being literal Element of S
for I being b2,b1 -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let U be non empty set ; for S being Language
for l being literal Element of S
for I being b1,U -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let S be Language; for l being literal Element of S
for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let l be literal Element of S; for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let I be S,U -interpreter-like Function; for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let tt be Element of AllTermsOf S; (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
set TI = I -TermEval ;
set u = (I -TermEval) . tt;
set J = (l,((I -TermEval) . tt)) ReassignIn I;
set TJ = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval ;
set F = S -firstChar ;
set C = S -multiCat ;
set FI = (S,X) -freeInterpreter ;
set FJ = (l,tt) ReassignIn ((S,X) -freeInterpreter);
set TF = ((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider LH = (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval), RH = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval as Function of (AllTermsOf S),U ;
now for tt0 being Element of AllTermsOf S holds LH . tt0 = RH . tt0let tt0 be
Element of
AllTermsOf S;
LH . tt0 = RH . tt0reconsider t =
tt0 as
termal string of
S ;
set n =
Depth t;
reconsider nn =
Depth t,
NN =
(Depth t) + 1 as
Element of
NAT by ORDINAL1:def 12;
reconsider tn =
t as
Depth t -termal string of
S by FOMODEL1:def 40;
tn is
(Depth t) + (0 * 1) -termal
;
then reconsider tN =
tn as
NN -termal string of
S ;
reconsider TN =
(S -termsOfMaxDepth) . NN,
Tn =
(S -termsOfMaxDepth) . nn as
Subset of
(AllTermsOf S) by FOMODEL1:2;
reconsider tnn =
tn as
Element of
Tn by FOMODEL1:def 33;
reconsider tNN =
tN as
Element of
TN by FOMODEL1:def 33;
((((l,tt) ReassignIn ((S,X) -freeInterpreter)),tt) -TermEval) . NN is
Element of
Funcs (
(AllTermsOf S),
(AllTermsOf S))
;
then reconsider FJN =
((((l,tt) ReassignIn ((S,X) -freeInterpreter)),tt) -TermEval) . NN as
Function of
(AllTermsOf S),
(AllTermsOf S) ;
((((l,((I -TermEval) . tt)) ReassignIn I),((I -TermEval) . tt)) -TermEval) . NN is
Element of
Funcs (
(AllTermsOf S),
U)
;
then reconsider JN =
((((l,((I -TermEval) . tt)) ReassignIn I),((I -TermEval) . tt)) -TermEval) . NN as
Function of
(AllTermsOf S),
U ;
(
((I -TermEval) . (FJN . tt0)) \+\ (((I -TermEval) * FJN) . tt0) = {} &
((((I -TermEval) * FJN) | TN) . tNN) \+\ (((I -TermEval) * FJN) . tNN) = {} &
((JN | TN) . tNN) \+\ (JN . tNN) = {} )
;
then A1:
(
((I -TermEval) * FJN) . tt0 = (I -TermEval) . (FJN . tt0) &
(((I -TermEval) * FJN) | TN) . tt0 = ((I -TermEval) * FJN) . tt0 &
(JN | TN) . tt0 = JN . tt0 )
by FOMODEL0:29;
(LH . tt0) \+\ ((I -TermEval) . ((((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) . tt0)) = {}
;
then LH . tt0 =
(I -TermEval) . ((((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) . tt0)
by FOMODEL0:29
.=
(I -TermEval) . (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval tt0)
by FOMODEL2:def 10
.=
(I -TermEval) . (FJN . tnn)
by FOMODEL2:def 9
.=
(((((l,((I -TermEval) . tt)) ReassignIn I),((I -TermEval) . tt)) -TermEval) . NN) . tnn
by A1, Th7
.=
((l,((I -TermEval) . tt)) ReassignIn I) -TermEval tt0
by FOMODEL2:def 9
.=
(((l,((I -TermEval) . tt)) ReassignIn I) -TermEval) . tt0
by FOMODEL2:def 10
;
hence
LH . tt0 = RH . tt0
;
verum end;
hence
(I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
by FUNCT_2:63; verum