let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- p & X |- p => q holds
X |- q
let X be Subset of LTLB_WFF; :: thesis: ( X |- p & X |- p => q implies X |- q )
assume X |- p ; :: thesis: ( not X |- p => q or X |- q )
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = p and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ;
set j = len f;
assume X |- p => q ; :: thesis: X |- q
then consider f1 being FinSequence of LTLB_WFF such that
A4: f1 . (len f1) = p => q and
A5: 1 <= len f1 and
A6: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ;
A7: 1 <= (len f) + (len f1) by A2, NAT_1:12;
set g = (f ^ f1) ^ <*q*>;
A8: (f ^ f1) ^ <*q*> = f ^ (f1 ^ <*q*>) by FINSEQ_1:32;
A9: for i being Nat st 1 <= i & i <= len f1 holds
((f ^ f1) ^ <*q*>) . ((len f) + i) = f1 . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len f1 implies ((f ^ f1) ^ <*q*>) . ((len f) + i) = f1 . i )
assume that
A10: 1 <= i and
A11: i <= len f1 ; :: thesis: ((f ^ f1) ^ <*q*>) . ((len f) + i) = f1 . i
len (f1 ^ <*q*>) = (len f1) + (len <*q*>) by FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
then i <= len (f1 ^ <*q*>) by A11, NAT_1:12;
hence ((f ^ f1) ^ <*q*>) . ((len f) + i) = (f1 ^ <*q*>) . i by A8, A10, FINSEQ_1:65
.= f1 . i by A10, A11, FINSEQ_1:64 ;
:: thesis: verum
end;
A12: len ((f ^ f1) ^ <*q*>) = (len (f ^ f1)) + (len <*q*>) by FINSEQ_1:22
.= (len (f ^ f1)) + 1 by FINSEQ_1:39 ;
then A13: len ((f ^ f1) ^ <*q*>) = ((len f) + (len f1)) + 1 by FINSEQ_1:22;
then len ((f ^ f1) ^ <*q*>) = (len f) + ((len f1) + 1) ;
then A14: len f < len ((f ^ f1) ^ <*q*>) by NAT_1:16;
then A15: ((f ^ f1) ^ <*q*>) /. (len f) = ((f ^ f1) ^ <*q*>) . (len f) by A2, Lm1
.= p by A1, A2, A8, FINSEQ_1:64 ;
set k = (len f) + (len f1);
A16: 1 <= (len f) + (len f1) by A2, NAT_1:12;
( ((f ^ f1) ^ <*q*>) . (len ((f ^ f1) ^ <*q*>)) = q & 1 <= len ((f ^ f1) ^ <*q*>) ) by A12, FINSEQ_1:42, NAT_1:11;
then A17: ((f ^ f1) ^ <*q*>) /. (len ((f ^ f1) ^ <*q*>)) = q by Lm1;
A18: (len f) + (len f1) < len ((f ^ f1) ^ <*q*>) by A13, NAT_1:16;
then ((f ^ f1) ^ <*q*>) /. ((len f) + (len f1)) = ((f ^ f1) ^ <*q*>) . ((len f) + (len f1)) by A2, Lm1, NAT_1:12
.= p => q by A4, A5, A9 ;
then ((f ^ f1) ^ <*q*>) /. (len f),((f ^ f1) ^ <*q*>) /. ((len f) + (len f1)) MP_rule ((f ^ f1) ^ <*q*>) /. (len ((f ^ f1) ^ <*q*>)) by A15, A17;
then A19: ( len (f ^ f1) = (len f) + (len f1) & prc (f ^ f1) ^ <*q*>,X, len ((f ^ f1) ^ <*q*>) ) by A2, A14, A16, A18, FINSEQ_1:22;
for i being Nat st 1 <= i & i <= len (f ^ f1) holds
prc f ^ f1,X,i by A2, A3, A5, A6, Th39;
hence X |- q by A7, A19, Th40; :: thesis: verum