let k, m be Nat; :: thesis:
let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
let X be functional set ; :: thesis:
set L = LettersOf S;
set F = S -firstChar ;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set EF = ExFormulasOf S;
let num be sequence of (ExFormulasOf S); :: thesis:
set f = (D,num) addw X;
assume A1: ( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D ) ; :: thesis:
assume A2: ( (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent ) ; :: thesis:
defpred S₁[ Nat] means ( ((D,num) addw X) . k c= ((D,num) addw X) . (k + $1) & (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . $1) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & ((D,num) addw X) . $1 is D -consistent );
A3: S₁[ 0 ] by A2, Def71;
A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis:
reconsider mk = k + m, MM = m + 1, mm = m as Element of NAT by ORDINAL1:def 12;
reconsider phii = num . mm as Element of ExFormulasOf S ;
reconsider phi = num . mm as wff exal string of S by TARSKI:def 3;
reconsider phi1 = head phi as wff string of S ;
reconsider l1 = (S -firstChar) . phi as literal Element of S ;
A5: phi = (<*l1*> ^ phi1) ^ (tail phi) by FOMODEL2:23
.= <*l1*> ^ phi1 ;
reconsider fmk = (D,(num . mk)) AddAsWitnessTo (((D,num) addw X) . mk) as Subset of ((((D,num) addw X) . mk) \/ (AllFormulasOf S)) ;
reconsider fmm = (D,(num . mm)) AddAsWitnessTo (((D,num) addw X) . mm) as Subset of ((((D,num) addw X) . mm) \/ (AllFormulasOf S)) ;
(((D,num) addw X) . mk) \ fmk = {} ;
then ((D,num) addw X) . mk c= fmk by XBOOLE_1:37;
then A6: ( ((D,num) addw X) . mk c= ((D,num) addw X) . (mk + 1) & ((D,num) addw X) . MM = fmm ) by Def71;
assume A7: S₁[m] ; :: thesis:
hence ((D,num) addw X) . k c= ((D,num) addw X) . (k + (m + 1)) by A6, XBOOLE_1:1; :: thesis:
(((D,num) addw X) . mm) \ fmm = {} ;
then reconsider fm = ((D,num) addw X) . mm as functional Subset of fmm by XBOOLE_1:37;
reconsider sm = fm /\ (((AllSymbolsOf S) *) \ {{}}) as Subset of (fmm /\ (((AllSymbolsOf S) *) \ {{}})) by XBOOLE_1:26;
reconsider t = fmm \ (((D,num) addw X) . mm) as trivial set ;
reconsider i = (LettersOf S) \ (SymbolsOf sm) as infinite set by A7;
reconsider T = t /\ (((AllSymbolsOf S) *) \ {{}}) as functional finite FinSequence-membered set ;
fmm = fm \/ t by XBOOLE_1:45;
then SymbolsOf (fmm /\ (((AllSymbolsOf S) *) \ {{}})) = SymbolsOf (sm \/ T) by XBOOLE_1:23
.= (SymbolsOf sm) \/ (SymbolsOf T) by FOMODEL0:47 ;
then (LettersOf S) \ (SymbolsOf (fmm /\ (((AllSymbolsOf S) *) \ {{}}))) = i \ (SymbolsOf T) by XBOOLE_1:41;
hence (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . (m + 1)) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite by Def71; :: thesis:
reconsider LF = (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (fm \/ {(head phii)}))) as Subset of (LettersOf S) ;

per cases ;

suppose A8: ( fm \/ {phii} is D -consistent & LF <> {} ) ; :: thesis:

then reconsider LF = LF as non empty Subset of (LettersOf S) ;
set ll2 = the Element of LF;
reconsider l2 = the Element of LF as literal Element of S by TARSKI:def 3;
not the Element of LF in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (fm \/ {(head phii)})) by XBOOLE_0:def 5;
then ( fm \/ {(<*l1*> ^ phi1)} is D -consistent & l2 is fm \/ {phi1} -absent ) by A8, A5;
then A9: fm \/ {((l1,l2) -SymbolSubstIn phi1)} is D -consistent by Lm49, A1;
thus ((D,num) addw X) . (m + 1) is D -consistent by A8, Def66, A9, A6; :: thesis:

end;

suppose ( not fm \/ {phii} is D -consistent or not LF <> {} ) ; :: thesis:

hence ((D,num) addw X) . (m + 1) is D -consistent by A7, A6, Def66; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence ( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) & (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & ((D,num) addw X) . m is D -consistent ) ; :: thesis: