let S be Language; :: thesis:
let psi be wff string of S; :: thesis:
let D1 be 0 -ranked 1 -ranked RuleSet of S; :: thesis:
let X be D1 -expanded set ; :: thesis:
set TT = AllTermsOf S;
set E = TheEqSymbOf S;
set F = S -firstChar ;
set N = TheNorSymbOf S;
set R = (X,D1) -termEq ;
set U = Class ((X,D1) -termEq);
set L = LettersOf S;
set AF = AtomicFormulasOf S;
set d = (Class ((X,D1) -termEq)) -deltaInterpreter ;
set i = (S,X) -freeInterpreter ;
set II = (Class ((X,D1) -termEq)) -InterpretersOf S;
set D = D1;
set ii = (AllTermsOf S) -InterpretersOf S;
set G0 = R#0 S;
set G1 = R#1 S;
set G2 = R#2 S;
set G4 = R#4 S;
set G6 = R#6 S;
set G7 = R#7 S;
set G8 = R#8 S;
set E0 = {(R#0 S)};
set E1 = {(R#1 S)};
set E2 = {(R#2 S)};
set E4 = {(R#4 S)};
set E6 = {(R#6 S)};
set E7 = {(R#7 S)};
set E8 = {(R#8 S)};
reconsider E0 = {(R#0 S)}, E1 = {(R#1 S)}, E2 = {(R#2 S)}, E4 = {(R#4 S)}, E6 = {(R#6 S)}, E7 = {(R#7 S)}, E8 = {(R#8 S)} as RuleSet of S ;
assume ( R#1 S in D1 & R#4 S in D1 & R#6 S in D1 & R#7 S in D1 & R#8 S in D1 ) ; :: thesis:
then ( R#0 S in D1 & R#1 S in D1 & R#2 S in D1 & R#4 S in D1 & R#6 S in D1 & R#7 S in D1 & R#8 S in D1 ) by Def62;
then reconsider F0 = E0, F1 = E1, F2 = E2, F4 = E4, F6 = E6, F7 = E7, F8 = E8 as Subset of D1 by ZFMISC_1:31;
A1: ( F0 \/ ((F0 \/ F1) \/ F8) c= D1 & F0 \/ F6 c= D1 & F0 c= D1 & F0 \/ (((F0 \/ F1) \/ F8) \/ F7) c= D1 ) ;
reconsider I = D1 Henkin X as Element of (Class ((X,D1) -termEq)) -InterpretersOf S ;
set UV = I -TermEval ;
set uv = ((S,X) -freeInterpreter) -TermEval ;
set O = OwnSymbolsOf S;
set FF = AllFormulasOf S;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
assume A2: ( X is S -mincover & X is S -witnessed ) ; :: thesis:
defpred S₁[ Nat] means for phi being wff string of S st phi is $1 -wff holds
( I -TruthEval phi = 1 iff phi in X );
A3: S₁[ 0 ]

let phi be wff string of S; :: thesis:
assume phi is 0 -wff ; :: thesis:
then reconsider phi0 = phi as 0wff string of S ;
( I -AtomicEval phi0 = 1 iff phi0 in X ) by Lm50;
hence ( I -TruthEval phi = 1 iff phi in X ) ; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
set Vn = (I,n) -TruthEval ;
assume A5: S₁[n] ; :: thesis:
let phi be wff string of S; :: thesis:
set s = (S -firstChar) . phi;
set V = I -TruthEval phi;
assume A6: phi is n + 1 -wff ; :: thesis:

per cases ;

suppose ( not phi is 0wff & phi is exal ) ; :: thesis:

then reconsider phii = phi as non 0wff n + 1 -wff exal string of S by A6;
reconsider phi1 = head phii as n -wff string of S ;
reconsider l = (S -firstChar) . phii as literal Element of S ;
A7: phii = (<*l*> ^ phi1) ^ (tail phii) by FOMODEL2:23
.= <*l*> ^ phi1 ;

hereby :: thesis:

assume I -TruthEval phi = 1 ; :: thesis:
then consider u being Element of Class ((X,D1) -termEq) such that
A8: ((l,u) ReassignIn I) -TruthEval phi1 = 1 by A7, FOMODEL2:19;
consider x being object such that
A9: ( x in AllTermsOf S & u = Class (((X,D1) -termEq),x) ) by EQREL_1:def 3;
reconsider tt = x as Element of AllTermsOf S by A9;
reconsider psi1 = (l,tt) SubstIn phi1 as n -wff string of S ;
( (id (AllTermsOf S)) . tt = tt & (((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt) \+\ ((((X,D1) -termEq) -class) . ((((S,X) -freeInterpreter) -TermEval) . tt)) = {} ) ;
then A10: ( (((S,X) -freeInterpreter) -TermEval) . tt = tt & ((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt = (((X,D1) -termEq) -class) . ((((S,X) -freeInterpreter) -TermEval) . tt) ) by FOMODEL0:29, FOMODEL3:4;
(I -TermEval) . tt = ((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt by FOMODEL3:3
.= u by A10, FOMODEL3:def 13, A9 ;
then 1 = I -TruthEval psi1 by A8, FOMODEL3:10;
then A11: psi1 in X by A5;
[{((l,tt) SubstIn phi1)},(<*l*> ^ phi1)] is 1, {} ,{(R#4 S)} -derivable ;
then ( <*l*> ^ phi1 is X,E4 -provable & F4 c= D1 & E4 is isotone ) by A11, ZFMISC_1:31;
then phii is X,D1 -provable by A7, Lm19;
hence phi in X by Def18; :: thesis:

end;

assume phi in X ; :: thesis:
then consider l2 being literal Element of S such that
A12: ( (l,l2) -SymbolSubstIn phi1 in X & not l2 in rng phi1 ) by A2, A7;
reconsider psi1 = (l,l2) -SymbolSubstIn phi1 as n -wff string of S ;
consider u being Element of Class ((X,D1) -termEq) such that
A13: ( u = (I . l2) . {} & (l2,u) ReassignIn I = I ) by FOMODEL2:26;
reconsider I2 = (l2,u) ReassignIn I, I1 = (l,u) ReassignIn I as Element of (Class ((X,D1) -termEq)) -InterpretersOf S ;
I2 -TruthEval psi1 = 1 by A12, A5, A13;
then I1 -TruthEval phi1 = 1 by A12, FOMODEL3:9;
hence I -TruthEval phi = 1 by A7, FOMODEL2:19; :: thesis:

end;

suppose ( not phi is 0wff & not phi is exal ) ; :: thesis:

then reconsider phii = phi as non 0wff n + 1 -wff non exal string of S by A6;
set phi1 = head phii;
set phi2 = tail phii;
((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} ;
then (S -firstChar) . phi = TheNorSymbOf S by FOMODEL0:29;
then A14: phi = (<*(TheNorSymbOf S)*> ^ (head phii)) ^ (tail phii) by FOMODEL2:23;
( I -TruthEval phi = 1 iff ( I -TruthEval (head phii) = 0 & I -TruthEval (tail phii) = 0 ) ) by A14, FOMODEL2:19;
then ( I -TruthEval phi = 1 iff ( not I -TruthEval (head phii) = 1 & not I -TruthEval (tail phii) = 1 ) ) by FOMODEL0:39;
then A15: ( I -TruthEval phi = 1 iff ( not head phii in X & not tail phii in X ) ) by A5;

A16: now :: thesis:

assume ( xnot (head phii) in X & xnot (tail phii) in X ) ; :: thesis:
then ( xnot (head phii) is X,{(R#0 S)} -provable & xnot (tail phii) is X,{(R#0 S)} -provable ) by Th6;
then ( xnot (head phii) is X,D1 -provable & xnot (tail phii) is X,D1 -provable ) by A1, Lm19;
then ( xnot (head phii) in X & xnot (tail phii) in X ) by Def18;
then reconsider Y = {(xnot (head phii)),(xnot (tail phii))} as Subset of X by ZFMISC_1:32;
phi is X null Y,D1 -provable by Lm19, A1, A14;
hence phi in X by Def18; :: thesis:

end;

now :: thesis:

reconsider H = {phi} as S -premises-like set ;
assume phi in X ; :: thesis:
then E7: H c= X by ZFMISC_1:31;
A17: [{phi},phi] is 1, {} ,E0 -derivable ;
A18: [(H null (tail phii)),(xnot (head phii))] is 2,{[{phi},phi]},(E0 \/ E1) \/ E8 -derivable by A14;
A19: [(H null (head phii)),(xnot (tail phii))] is 3,{[H,phi]},((E0 \/ E1) \/ E8) \/ E7 -derivable by A14;
[H,(xnot (head phii))] is 1 + 2, {} ,E0 \/ ((E0 \/ E1) \/ E8) -derivable by A18, Lm22;
then [H,(xnot (head phii))] is 3, {} ,D1 -derivable by A1, Th2;
then xnot (head phii) is X,D1 -provable by E7;
hence xnot (head phii) in X by Def18; :: thesis:
[H,(xnot (tail phii))] is 1 + 3, {} ,E0 \/ (((E0 \/ E1) \/ E8) \/ E7) -derivable by A17, A19, Lm22;
then [H,(xnot (tail phii))] is 4, {} ,D1 -derivable by A1, Th2;
then xnot (tail phii) is X,D1 -provable by E7;
hence xnot (tail phii) in X by Def18; :: thesis:

end;

hence ( I -TruthEval phi = 1 iff phi in X ) by A15, A2, A16; :: thesis:

end;

suppose phi is 0wff ; :: thesis:

hence ( I -TruthEval phi = 1 iff phi in X ) by A3; :: thesis:

end;

A21: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
psi is Depth psi -wff by FOMODEL2:def 31;
hence ( (D1 Henkin X) -TruthEval psi = 1 iff psi in X ) by A21; :: thesis: