let k, m be Nat; for S being Language
for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
( ((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 )
let S be Language; for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
( ((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 )
let D be RuleSet of S; for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
( ((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 )
let X be functional set ; for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
( ((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 )
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); ( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent implies ( ((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 ) )
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 )
; ( not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite or not X is D -consistent or ( ((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 ) )
assume A2:
( (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent )
; ( ((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 )
defpred S1[ 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:
S1[ 0 ]
by A2, Def71;
A4:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
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:
S1[
m]
;
S1[m + 1]
hence
((D,num) addw X) . k c= ((D,num) addw X) . (k + (m + 1))
by A6, XBOOLE_1:1;
( (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . (m + 1)) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & ((D,num) addw X) . (m + 1) is D -consistent )
(((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;
((D,num) addw X) . (m + 1) is D -consistent
reconsider LF =
(LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (fm \/ {(head phii)}))) as
Subset of
(LettersOf S) ;
end;
for n being Nat holds S1[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 )
; verum