let m be Nat; for S being Language holds S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)
let S be Language; S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)
set U = the non empty set ;
set n = m + 1;
set II = the non empty set -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set I = the Element of the non empty set -InterpretersOf S;
reconsider mm = m, nn = m + 1 as Element of NAT by ORDINAL1:def 12;
set F = (S, the non empty set ) -TruthEval ;
set Fn = ((S, the non empty set ) -TruthEval) . nn;
set Fc = curry (((S, the non empty set ) -TruthEval) . nn);
set Dm = S -formulasOfMaxDepth m;
set Dn = S -formulasOfMaxDepth (m + 1);
((S, the non empty set ) -TruthEval) . mm is Element of PFuncs ([:( the non empty set -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)
;
then reconsider Fm = ((S, the non empty set ) -TruthEval) . mm as PartFunc of [:( the non empty set -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
A1:
( (S, the non empty set ) -TruthEval (m + 1) = ((S, the non empty set ) -TruthEval) . nn & (S, the non empty set ) -TruthEval m = Fm )
by Def20;
reconsider Fcc = curry (((S, the non empty set ) -TruthEval) . nn) as Function of ( the non empty set -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth (m + 1)),BOOLEAN)) by Lm17, A1;
reconsider fn = Fcc . the Element of the non empty set -InterpretersOf S as Function of (S -formulasOfMaxDepth (m + 1)),BOOLEAN ;
Fm is Element of Funcs ([:( the non empty set -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN)
by Th8;
then reconsider Fmm = Fm as Function of [:( the non empty set -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN ;
( dom fn = S -formulasOfMaxDepth (m + 1) & dom Fcc = the non empty set -InterpretersOf S )
by FUNCT_2:def 1;
then A2:
S -formulasOfMaxDepth (m + 1) = proj2 ((dom (((S, the non empty set ) -TruthEval) . nn)) /\ [:{ the Element of the non empty set -InterpretersOf S},(proj2 (dom (((S, the non empty set ) -TruthEval) . nn))):])
by FUNCT_5:31;
A3:
((S, the non empty set ) -TruthEval) . nn = ((ExIterator (((S, the non empty set ) -TruthEval) . mm)) +* (NorIterator (((S, the non empty set ) -TruthEval) . mm))) +* Fm
by Def19;
reconsider Em = ExIterator (((S, the non empty set ) -TruthEval) . mm) as PartFunc of [:( the non empty set -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
reconsider dEm = dom Em as Relation of ( the non empty set -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}) ;
reconsider dNm = dom (NorIterator (((S, the non empty set ) -TruthEval) . mm)), dFm = dom Fm as Relation of ( the non empty set -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}) ;
A4: dFm =
dom Fmm
.=
[:( the non empty set -InterpretersOf S),(S -formulasOfMaxDepth m):]
by FUNCT_2:def 1
;
A5: dom (((S, the non empty set ) -TruthEval) . nn) =
(dom ((ExIterator (((S, the non empty set ) -TruthEval) . mm)) +* (NorIterator (((S, the non empty set ) -TruthEval) . mm)))) \/ (dom Fm)
by A3, FUNCT_4:def 1
.=
(dEm \/ dNm) \/ dFm
by FUNCT_4:def 1
;
set RNNN = m -NorFormulasOf S;
set REEE = m -ExFormulasOf S;
(S, the non empty set ) -TruthEval m = Fm
by Def20;
then
( dNm = [:( the non empty set -InterpretersOf S),(m -NorFormulasOf S):] & dEm = [:( the non empty set -InterpretersOf S),(m -ExFormulasOf S):] )
by Lm18, Lm19;
then A6: (dEm \/ dNm) \/ dFm =
[:( the non empty set -InterpretersOf S),((m -ExFormulasOf S) \/ (m -NorFormulasOf S)):] \/ [:( the non empty set -InterpretersOf S),(S -formulasOfMaxDepth m):]
by A4, ZFMISC_1:97
.=
[:( the non empty set -InterpretersOf S),(((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)):]
by ZFMISC_1:97
;
reconsider sub = [:{ the Element of the non empty set -InterpretersOf S},(((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)):] as Subset of [:( the non empty set -InterpretersOf S),(((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)):] by ZFMISC_1:96;
S -formulasOfMaxDepth (m + 1) =
rng ([:( the non empty set -InterpretersOf S),(((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)):] /\ sub)
by A6, A2, A5
.=
((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)
;
hence
S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)
; verum