let X be set ; :: thesis: for U being non empty set
for n being Nat
for S being Language
for l being literal Element of S
for I being b₃,b₁ -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let U be non empty set ; :: thesis: for n being Nat
for S being Language
for l being literal Element of S
for I being b₂,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let n be Nat; :: thesis: for S being Language
for l being literal Element of S
for I being b₁,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let S be Language; :: thesis: for l being literal Element of S
for I being S,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let l be literal Element of S; :: thesis: for I being S,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let I be S,U -interpreter-like Function; :: thesis: for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let tt0 be Element of AllTermsOf S; :: thesis: ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
set II = U -InterpretersOf S;
reconsider u = (I -TermEval) . tt0 as Element of U ;
set F = S -firstChar ;
set FI = (S,X) -freeInterpreter ;
set H = (l,tt0) ReassignIn ((S,X) -freeInterpreter);
set TT = AllTermsOf S;
set TI = (I,u) -TermEval ;
set TF = (((S,X) -freeInterpreter),tt0) -TermEval ;
set TH = (((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval ;
set TII = I -TermEval ;
set J = (l,((I -TermEval) . tt0)) ReassignIn I;
set TJ = (((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval ;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
reconsider t0 = tt0 as termal string of S ;
set k = Depth t0;
reconsider t00 = t0 as Depth t0 -termal string of S by FOMODEL1:def 40;
B3: ( l in {l} & dom (l .--> ({} .--> tt0)) = {l} & dom (l .--> ({} .--> ((I -TermEval) . tt0))) = {l} ) by FUNCOP_1:13, TARSKI:def 1;
then ( ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . l = (l .--> ({} .--> tt0)) . l & ((l,((I -TermEval) . tt0)) ReassignIn I) . l = (l .--> ({} .--> ((I -TermEval) . tt0))) . l ) by FUNCT_4:13;
then B2: ( ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . l = {} .--> tt0 & ((l,((I -TermEval) . tt0)) ReassignIn I) . l = {} .--> ((I -TermEval) . tt0) ) by B3, FUNCOP_1:7;
defpred S₁[ Nat] means ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . $1)) | ((S -termsOfMaxDepth) . $1) = (((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . $1) | ((S -termsOfMaxDepth) . $1);
B0: S₁[ 0 ]

proof

C0: ( dom ((AllTermsOf S) --> u) = AllTermsOf S & dom ((AllTermsOf S) --> tt0) = AllTermsOf S & dom (I -TermEval) = AllTermsOf S ) by FUNCT_2:def 1;
( ((I,u) -TermEval) . 0 = (AllTermsOf S) --> u & ((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . 0 = (AllTermsOf S) --> tt0 ) by FOMODEL2:def 8;
then (I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . 0) = (AllTermsOf S) --> ((I -TermEval) . tt0) by C0, FUNCOP_1:17
.= ((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . 0 by FOMODEL2:def 8 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

B1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
reconsider mm = m, MM = m + 1 as Element of NAT by ORDINAL1:def 12;
assume C2: S₁[m] ; :: thesis: S₁[m + 1]
reconsider TM = (S -termsOfMaxDepth) . MM, Tm = (S -termsOfMaxDepth) . mm as Subset of (AllTermsOf S) by FOMODEL1:2;
( ((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . mm is Element of Funcs ((AllTermsOf S),U) & ((I,u) -TermEval) . MM is Element of Funcs ((AllTermsOf S),U) & ((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . MM is Element of Funcs ((AllTermsOf S),U) & ((I,u) -TermEval) . mm is Element of Funcs ((AllTermsOf S),U) ) ;
then reconsider Jm = ((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . mm, JM = ((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . MM, IM = ((I,u) -TermEval) . MM, Imm = ((I,u) -TermEval) . mm as Function of (AllTermsOf S),U ;
( ((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . mm is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) & ((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . MM is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) ) ;
then reconsider Hm = ((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . mm, HM = ((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . MM as Function of (AllTermsOf S),(AllTermsOf S) ;
set LH = ((I -TermEval) * HM) | TM;
set RH = JM | TM;
C0: ( dom (((I -TermEval) * HM) | TM) = TM & dom (JM | TM) = TM ) by PARTFUN1:def 2;

now

let x be set ; :: thesis: ( x in dom (((I -TermEval) * HM) | TM) implies (((I -TermEval) * HM) | TM) . b₁ = (JM | TM) . b₁ )
assume D5: x in dom (((I -TermEval) * HM) | TM) ; :: thesis: (((I -TermEval) * HM) | TM) . b₁ = (JM | TM) . b₁
then x in dom ((I -TermEval) * HM) by RELAT_1:57;
then reconsider tt = x as Element of AllTermsOf S ;
reconsider t = x as mm + 1 -termal string of S by C0, D5, FOMODEL1:def 33;
reconsider ttt = x as Element of TM by D5, PARTFUN1:def 2;
set ST = SubTerms t;
set o = (S -firstChar) . t;
set n = abs (ar ((S -firstChar) . t));
( (((IM * HM) | TM) . ttt) \+\ ((IM * HM) . ttt) = {} & ((JM | TM) . ttt) \+\ (JM . ttt) = {} & ((((I -TermEval) * HM) | TM) . ttt) \+\ (((I -TermEval) * HM) . ttt) = {} ) ;
then D7: ( ((IM * HM) | TM) . x = (IM * HM) . x & (JM | TM) . x = JM . x & (((I -TermEval) * HM) | TM) . x = ((I -TermEval) * HM) . x ) by FOMODEL0:29;
( ((IM * HM) . tt) \+\ (IM . (HM . tt)) = {} & (((I -TermEval) * HM) . tt) \+\ ((I -TermEval) . (HM . tt)) = {} ) ;
then C1: ( (IM * HM) . t = IM . (HM . t) & ((I -TermEval) * HM) . tt = (I -TermEval) . (HM . tt) ) by FOMODEL0:29;
reconsider newterms = Hm * (SubTerms t) as abs (ar ((S -firstChar) . t)) -element FinSequence of AllTermsOf S by FOMODEL0:26;
reconsider newtermss = newterms as Element of (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) by FOMODEL0:16;
reconsider newtermsss = newterms as FinSequence of ((AllSymbolsOf S) *) \ {{}} by FOMODEL0:26;
(((((S -firstChar) . t) -compound) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S))) . newtermss) \+\ ((((S -firstChar) . t) -compound) . newtermss) = {} ;
then D0: ((((S -firstChar) . t) -compound) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S))) . newterms = (((S -firstChar) . t) -compound) . newterms by FOMODEL0:29;

per cases ( (S -firstChar) . t = l or (S -firstChar) . t <> l ) ;

suppose (S -firstChar) . t = l ; :: thesis: (((I -TermEval) * HM) | TM) . b₁ = (JM | TM) . b₁

then ( (S -firstChar) . t = l & t is 0 -termal ) by FOMODEL1:16;
then ( ((I -TermEval) * HM) . t = (I -TermEval) . (({} .--> tt0) . {}) & JM . t = ({} .--> ((I -TermEval) . tt0)) . {} & {} in {{}} ) by C1, B2, FOMODEL2:3, TARSKI:def 1;
then ( ((I -TermEval) * HM) . t = (I -TermEval) . tt0 & JM . t = (I -TermEval) . tt0 ) by FUNCOP_1:7;
hence (((I -TermEval) * HM) | TM) . x = (JM | TM) . x by D7; :: thesis: verum

end;

suppose (S -firstChar) . t <> l ; :: thesis: (((I -TermEval) * HM) | TM) . b₁ = (JM | TM) . b₁

then not (S -firstChar) . t in {l} by TARSKI:def 1;
then D5: ( not (S -firstChar) . t in dom (l .--> ({} .--> tt0)) & not (S -firstChar) . t in dom (l .--> ({} .--> ((I -TermEval) . tt0))) ) by FUNCOP_1:13;
then ((S,X) -freeInterpreter) . ((S -firstChar) . t) = ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . ((S -firstChar) . t) by FUNCT_4:11;
then XX: ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . ((S -firstChar) . t) = X -freeInterpreter ((S -firstChar) . t) by DefFree1
.= (((S -firstChar) . t) -compound) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)) by DefFreeInt1 ;
then reconsider newtermssss = newterms as abs (ar ((S -firstChar) . t)) -element Element of (AllTermsOf S) * by FINSEQ_1:def 11;
D1: (((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . ((S -firstChar) . t)) . newterms = ((S -firstChar) . t) -compound newtermssss by D0, DefCompound1, XX;
reconsider t1 = ((S -firstChar) . t) -compound newtermssss as termal string of S ;
set p = Depth t1;
reconsider pp = Depth t1 as Element of NAT by ORDINAL1:def 12;
reconsider t111 = t1 as Depth t1 -termal string of S by FOMODEL1:def 40;
reconsider t11 = t1 as Element of AllTermsOf S by FOMODEL1:def 32;
((I,u) -TermEval) . pp is Element of Funcs ((AllTermsOf S),U) ;
then reconsider Ip = ((I,u) -TermEval) . pp as Function of (AllTermsOf S),U ;
D2: (S -firstChar) . t1 = t1 . 1 by FOMODEL0:6
.= (S -firstChar) . t by FINSEQ_1:41 ;
then D3: SubTerms t1 = newtermssss by FOMODEL1:def 37;
Z6: ( dom (Hm | Tm) = Tm & dom (Jm | Tm) = Tm & rng (SubTerms t) c= Tm ) by PARTFUN1:def 2, RELAT_1:def 19;
((I -TermEval) * HM) . t = (I -TermEval) . t1 by D1, C1, FOMODEL2:3
.= (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t1)) by D2, FOMODEL2:21
.= (I . ((S -firstChar) . t)) . ((I -TermEval) * ((Hm | Tm) * (SubTerms t))) by Z6, D3, RELAT_1:165
.= (I . ((S -firstChar) . t)) . (((I -TermEval) * (Hm | Tm)) * (SubTerms t)) by RELAT_1:36
.= (I . ((S -firstChar) . t)) . ((((I -TermEval) * Hm) | Tm) * (SubTerms t)) by RELAT_1:83
.= (I . ((S -firstChar) . t)) . (Jm * (SubTerms t)) by C2, Z6, RELAT_1:165
.= (((l,((I -TermEval) . tt0)) ReassignIn I) . ((S -firstChar) . t)) . (Jm * (SubTerms t)) by D5, FUNCT_4:11
.= JM . t by FOMODEL2:3 ;
hence (((I -TermEval) * HM) | TM) . x = (JM | TM) . x by D7; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by C0, FUNCT_1:2; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(B0, B1);
hence ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n) ; :: thesis: verum