let p be Element of LTLB_WFF ; :: thesis: for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds
{} LTLB_WFF |- (f /. i) => p ) holds
{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p
let f be FinSequence of LTLB_WFF ; :: thesis: ( ( for i being Nat st i in dom f holds
{} LTLB_WFF |- (f /. i) => p ) implies {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p )
set nt = 'not' TVERUM;
assume A1: for i being Nat st i in dom f holds
{} LTLB_WFF |- (f /. i) => p ; :: thesis: {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p

per cases ( len f = 0 or len f > 0 ) ;

suppose A2: len f = 0 ; :: thesis: {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p

('not' TVERUM) => p is ctaut by Th23;
then A3: ('not' TVERUM) => p in LTL_axioms by LTLAXIO1:def 17;
len (nega f) = 0 by A2, Def4;
then nega f = {} ;
hence {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p by A3, Th10, LTLAXIO1:42; :: thesis: verum

end;

suppose A4: len f > 0 ; :: thesis: {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p

defpred S₁[ Nat] means ( $1 <= len f implies {} LTLB_WFF |- ('not' ((con (nega f)) /. $1)) => p );

A5: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

set a = 'not' ((con (nega f)) /. (k + 1));
set b = f /. (k + 1);
set c = (con (nega f)) /. k;
set d = (nega f) /. (k + 1);
set nc = 'not' ((con (nega f)) /. k);
set nd = 'not' ((nega f) /. (k + 1));
(('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' ('not' ((nega f) /. (k + 1))))) => ((('not' ((nega f) /. (k + 1))) => (f /. (k + 1))) => (('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))))) is ctaut by Th48;
then (('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' ('not' ((nega f) /. (k + 1))))) => ((('not' ((nega f) /. (k + 1))) => (f /. (k + 1))) => (('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))))) in LTL_axioms by LTLAXIO1:def 17;
then A7: {} LTLB_WFF |- (('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' ('not' ((nega f) /. (k + 1))))) => ((('not' ((nega f) /. (k + 1))) => (f /. (k + 1))) => (('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))))) by LTLAXIO1:42;
assume A8: k + 1 <= len f ; :: thesis: {} LTLB_WFF |- ('not' ((con (nega f)) /. (k + 1))) => p
then k < len f by NAT_1:13;
then ( 1 <= k & k < len (nega f) ) by NAT_1:25, Def4;
then A9: 'not' ((con (nega f)) /. (k + 1)) = 'not' (((con (nega f)) /. k) '&&' ((nega f) /. (k + 1))) by Th7;
(('not' ((con (nega f)) /. k)) => p) => (((f /. (k + 1)) => p) => ((('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))) => p)) is ctaut by Th49;
then (('not' ((con (nega f)) /. k)) => p) => (((f /. (k + 1)) => p) => ((('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))) => p)) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- (('not' ((con (nega f)) /. k)) => p) => (((f /. (k + 1)) => p) => ((('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))) => p)) by LTLAXIO1:42;
then A10: {} LTLB_WFF |- ((f /. (k + 1)) => p) => ((('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))) => p) by LTLAXIO1:43, A6, A8, NAT_1:13;
A11: 1 <= k + 1 by NAT_1:25;
then {} LTLB_WFF |- (f /. (k + 1)) => p by FINSEQ_3:25, A8, A1;
then A12: {} LTLB_WFF |- (('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))) => p by A10, LTLAXIO1:43;
k + 1 in dom f by A11, FINSEQ_3:25, A8;
then 'not' ((nega f) /. (k + 1)) = 'not' ('not' (f /. (k + 1))) by Th8;
then ('not' ((nega f) /. (k + 1))) => (f /. (k + 1)) is ctaut by Th25;
then ('not' ((nega f) /. (k + 1))) => (f /. (k + 1)) in LTL_axioms by LTLAXIO1:def 17;
then A13: {} LTLB_WFF |- ('not' ((nega f) /. (k + 1))) => (f /. (k + 1)) by LTLAXIO1:42;
('not' (((con (nega f)) /. k) '&&' ((nega f) /. (k + 1)))) => (('not' ((con (nega f)) /. k)) 'or' ('not' ((nega f) /. (k + 1)))) is ctaut by Th35;
then ('not' (((con (nega f)) /. k) '&&' ((nega f) /. (k + 1)))) => (('not' ((con (nega f)) /. k)) 'or' ('not' ((nega f) /. (k + 1)))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' ('not' ((nega f) /. (k + 1)))) by LTLAXIO1:42, A9;
then {} LTLB_WFF |- (('not' ((nega f) /. (k + 1))) => (f /. (k + 1))) => (('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1)))) by A7, LTLAXIO1:43;
then {} LTLB_WFF |- ('not' ((con (nega f)) /. (k + 1))) => (('not' ((con (nega f)) /. k)) 'or' (f /. (k + 1))) by LTLAXIO1:43, A13;
hence {} LTLB_WFF |- ('not' ((con (nega f)) /. (k + 1))) => p by A12, LTLAXIO1:47; :: thesis: verum

end;

end;

A14: len (nega f) > 0 by A4, Def4;
A15: S₁[1]

proof

set nnf = 'not' ('not' (f /. 1));
assume A16: 1 <= len f ; :: thesis: {} LTLB_WFF |- ('not' ((con (nega f)) /. 1)) => p
then A17: 1 in dom f by FINSEQ_3:25;
('not' ('not' (f /. 1))) => (f /. 1) is ctaut by Th25;
then ('not' ('not' (f /. 1))) => (f /. 1) in LTL_axioms by LTLAXIO1:def 17;
then A18: {} LTLB_WFF |- ('not' ('not' (f /. 1))) => (f /. 1) by LTLAXIO1:42;
A19: {} LTLB_WFF |- (f /. 1) => p by A16, FINSEQ_3:25, A1;
'not' ((con (nega f)) /. 1) = 'not' ((nega f) /. 1) by A14, Th6
.= 'not' ('not' (f /. 1)) by Th8, A17 ;
hence {} LTLB_WFF |- ('not' ((con (nega f)) /. 1)) => p by A18, A19, LTLAXIO1:47; :: thesis: verum

end;

A20: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A15, A5);
len f = len (nega f) by Def4
.= len (con (nega f)) by A14, Def2 ;
hence {} LTLB_WFF |- H₁(f) => p by A20, A4; :: thesis: verum

end;

end;