let f be FinSequence of LTLB_WFF ; :: thesis: for k being Nat st k in dom f holds
(f /. k) => ('not' ((con (nega f)) /. (len (con (nega f))))) is ctaut
let k be Nat; :: thesis: ( k in dom f implies (f /. k) => ('not' ((con (nega f)) /. (len (con (nega f))))) is ctaut )
assume A1: k in dom f ; :: thesis: (f /. k) => ('not' ((con (nega f)) /. (len (con (nega f))))) is ctaut
set q = f /. k;
set p = (f /. k) => H₁(f);
assume not (f /. k) => H₁(f) is ctaut ; :: thesis: contradiction
then consider g being Function of LTLB_WFF,BOOLEAN such that
A2: not (VAL g) . ((f /. k) => H₁(f)) = 1 ;
set v = VAL g;
(VAL g) . ((f /. k) => H₁(f)) = 0 by A2, XBOOLEAN:def 3;
then A3: ((VAL g) . (f /. k)) => ((VAL g) . H₁(f)) = 0 by LTLAXIO1:def 15;
( (VAL g) . H₁(f) = TRUE or (VAL g) . H₁(f) = FALSE ) by XBOOLEAN:def 3;
hence contradiction by A3, Th20, A1; :: thesis: verum