let X be set ; :: thesis: for S being Language
for phi being wff string of S
for l1, l2 being literal Element of S
for D being RuleSet of 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 & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & l2 is X \/ {phi} -absent holds
X \/ {(<*l1*> ^ phi)} is D -inconsistent
let S be Language; :: thesis: for phi being wff string of S
for l1, l2 being literal Element of S
for D being RuleSet of 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 & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & l2 is X \/ {phi} -absent holds
X \/ {(<*l1*> ^ phi)} is D -inconsistent
let phi be wff string of S; :: thesis: for l1, l2 being literal Element of S
for D being RuleSet of 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 & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & l2 is X \/ {phi} -absent holds
X \/ {(<*l1*> ^ phi)} is D -inconsistent
let l1, l2 be literal Element of S; :: thesis: for D being RuleSet of 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 & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & l2 is X \/ {phi} -absent holds
X \/ {(<*l1*> ^ phi)} is D -inconsistent
let D be RuleSet of S; :: thesis: ( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & l2 is X \/ {phi} -absent implies X \/ {(<*l1*> ^ phi)} is D -inconsistent )
set E = TheEqSymbOf S;
set L = LettersOf S;
set SS = AllSymbolsOf S;
set Q = S -sequents ;
set psi = (l1,l2) -SymbolSubstIn phi;
set E1 = R#1 S;
set E2 = R#2 S;
set E5 = R#5 S;
set ll = the Element of (rng phi) /\ (LettersOf S);
the Element of (rng phi) /\ (LettersOf S) in LettersOf S by TARSKI:def 3;
then reconsider l = the Element of (rng phi) /\ (LettersOf S) as literal Element of S ;
reconsider t = <*l*> as termal string of S ;
set N = TheNorSymbOf S;
reconsider yes = (<*(TheEqSymbOf S)*> ^ t) ^ t as 0wff string of S ;
A1: rng yes = (rng (<*(TheEqSymbOf S)*> ^ t)) \/ (rng t) by FINSEQ_1:31
.= ((rng <*(TheEqSymbOf S)*>) \/ (rng t)) \/ (rng t) by FINSEQ_1:31
.= (rng <*(TheEqSymbOf S)*>) \/ ((rng t) \/ (rng t)) by XBOOLE_1:4
.= {(TheEqSymbOf S)} \/ (rng t) by FINSEQ_1:38
.= {(TheEqSymbOf S)} \/ {l} by FINSEQ_1:38 ;
reconsider lll = the Element of (rng phi) /\ (LettersOf S) as Element of rng phi by XBOOLE_0:def 4;
A2: {lll} \/ {(TheEqSymbOf S),(TheNorSymbOf S)} c= (rng phi) \/ {(TheEqSymbOf S),(TheNorSymbOf S)} by XBOOLE_1:9;
reconsider no = xnot yes as wff string of S ;
A3: rng no = (rng (<*(TheNorSymbOf S)*> ^ yes)) \/ (rng yes) by FINSEQ_1:31
.= ((rng <*(TheNorSymbOf S)*>) \/ (rng yes)) \/ (rng yes) by FINSEQ_1:31
.= (rng <*(TheNorSymbOf S)*>) \/ ((rng yes) \/ (rng yes)) by XBOOLE_1:4
.= {(TheNorSymbOf S)} \/ (rng yes) by FINSEQ_1:38
.= {(TheEqSymbOf S),(TheNorSymbOf S)} \/ {l} by A1, XBOOLE_1:4 ;
assume A4: ( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent ) ; :: thesis: ( not l2 is X \/ {phi} -absent or X \/ {(<*l1*> ^ phi)} is D -inconsistent )
then no is X \/ {((l1,l2) -SymbolSubstIn phi)},D -provable by Lm48;
then consider H3 being set , m being Nat such that
A5: ( H3 c= X \/ {((l1,l2) -SymbolSubstIn phi)} & [H3,no] is m, {} ,D -derivable ) ;
reconsider seqt1 = [H3,no] as Element of S -sequents by Def2, A5;
(seqt1 `1) \+\ H3 = {} ;
then reconsider H33 = H3 as S -premises-like Subset of (X \/ {((l1,l2) -SymbolSubstIn phi)}) by A5;
reconsider H1 = H33 /\ X as S -premises-like Subset of X ;
reconsider H2 = H33 /\ {((l1,l2) -SymbolSubstIn phi)} as S -premises-like Subset of {((l1,l2) -SymbolSubstIn phi)} ;
( {phi} null X c= X \/ {phi} & X null {phi} c= X \/ {phi} ) ;
then reconsider XX = X, Phi = {phi} as Subset of (X \/ {phi}) ;
reconsider H11 = H1 as S -premises-like Subset of XX ;
reconsider NO = {no}, Phii = {phi} as Subset of (((AllSymbolsOf S) *) \ {{}}) ;
assume A6: l2 is X \/ {phi} -absent ; :: thesis: X \/ {(<*l1*> ^ phi)} is D -inconsistent
then A7: ( l2 is XX -absent & l2 is Phi -absent ) ;
then not l2 in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ Phii) ;
then ( not l2 in rng phi & not l2 in {(TheEqSymbOf S),(TheNorSymbOf S)} ) by TARSKI:def 2, FOMODEL0:45;
then not l2 in rng no by A3, A2, XBOOLE_0:def 3;
then not l2 in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ NO) by FOMODEL0:45;
then reconsider ln = l2 as {no} -absent Element of S by FOMODEL2:def 38;
reconsider lN = ln as literal {phi} \/ {no} -absent Element of S by A7;
lN is H11 -absent by A6;
then reconsider lx = lN as literal H11 \/ ({phi} \/ {no}) -absent Element of S ;
H11 \/ ({phi} \/ {no}) = (H1 \/ {phi}) \/ {no} by XBOOLE_1:4;
then lx is (H1 \/ {phi}) \/ {no} -absent ;
then reconsider l22 = l2 as literal (H1 \/ {phi}) \/ {no} -absent Element of S ;
reconsider F2 = {(R#2 S)}, F1 = {(R#1 S)}, F5 = {(R#5 S)} as Subset of D by ZFMISC_1:31, A4;
A8: ( D \/ (F1 \/ F5) = D & F2 c= D & {} c= X \/ {(<*l1*> ^ phi)} & H1 \/ {(<*l1*> ^ phi)} c= X \/ {(<*l1*> ^ phi)} ) by XBOOLE_1:9;
B3: H33 null (X \/ {((l1,l2) -SymbolSubstIn phi)}) = H1 \/ H2 by XBOOLE_1:23;
B2: [((H1 \/ {(<*l1*> ^ phi)}) null l22),no] is 1,{[(H1 \/ {((l1,l2) -SymbolSubstIn phi)}),no]},{(R#5 S)} -derivable ;
[((H1 \/ H2) \/ {((l1,l2) -SymbolSubstIn phi)}),no] is 1,{[(H1 \/ H2),no]},{(R#1 S)} -derivable ;
then [(H1 \/ ({((l1,l2) -SymbolSubstIn phi)} null H2)),no] is 1,{[H33,no]},{(R#1 S)} -derivable by XBOOLE_1:4, B3;
then [(H1 \/ {(<*l1*> ^ phi)}),no] is 1 + 1,{[H33,no]},{(R#1 S)} \/ {(R#5 S)} -derivable by B2, Lm22;
then [(H1 \/ {(<*l1*> ^ phi)}),no] is m + 2, {} ,D -derivable by A8, A4, Lm22, A5;
then A9: no is X \/ {(<*l1*> ^ phi)},D -provable by A8;
set seqt2 = [{},yes];
( {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} is {(R#2 S)} -derivable & ([{},yes] `1) \+\ {} = {} & ([{},yes] `2) \+\ yes = {} ) ;
then yes is {} ,{(R#2 S)} -provable ;
then yes is X \/ {(<*l1*> ^ phi)},D -provable by A8, Lm19;
hence X \/ {(<*l1*> ^ phi)} is D -inconsistent by A9; :: thesis: verum