let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF holds X |- ('X' (p '&&' q)) => (('X' p) '&&' ('X' q))
let X be Subset of LTLB_WFF; :: thesis: X |- ('X' (p '&&' q)) => (('X' p) '&&' ('X' q))
set xp = 'X' p;
set xq = 'X' q;
set np = 'not' p;
set nq = 'not' q;
set xnp = 'X' ('not' p);
set xnq = 'X' ('not' q);
set nxp = 'not' ('X' p);
set nxq = 'not' ('X' q);
set npq = ('not' p) '&&' ('not' q);
A1: X |- (('X' p) => ('X' ('not' q))) => ('X' (p => ('not' q))) by Th58;
(('X' p) => ('not' ('X' q))) => (('X' p) => ('not' ('X' q))) is ctaut by Th24;
then (('X' p) => ('not' ('X' q))) => (('X' p) => ('not' ('X' q))) in LTL_axioms by LTLAXIO1:def 17;
then A2: X |- (('X' p) => ('not' ('X' q))) => (('X' p) => ('not' ('X' q))) by LTLAXIO1:42;
('not' ('X' q)) => ('X' ('not' q)) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('not' ('X' q)) => ('X' ('not' q)) by LTLAXIO1:42;
then X |- (('X' p) => ('not' ('X' q))) => (('X' p) => ('X' ('not' q))) by A2, LTLAXIO1:51;
then A3: X |- (('X' p) => ('not' ('X' q))) => ('X' (p => ('not' q))) by A1, LTLAXIO1:47;
('X' ('not' (p => ('not' q)))) => ('not' ('X' (p => ('not' q)))) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' ('not' (p => ('not' q)))) => ('not' ('X' (p => ('not' q)))) by LTLAXIO1:42;
then A4: X |- ('not' ('not' ('X' (p => ('not' q))))) => ('not' ('X' ('not' (p => ('not' q))))) by LTLAXIO1:52;
('X' ('not' (p => ('not' q)))) => ('not' ('not' ('X' ('not' (p => ('not' q)))))) is ctaut by Th26;
then ('X' ('not' (p => ('not' q)))) => ('not' ('not' ('X' ('not' (p => ('not' q)))))) in LTL_axioms by LTLAXIO1:def 17;
then A5: X |- ('X' ('not' (p => ('not' q)))) => ('not' ('not' ('X' ('not' (p => ('not' q)))))) by LTLAXIO1:42;
('X' (p => ('not' q))) => ('not' ('not' ('X' (p => ('not' q))))) is ctaut by Th26;
then ('X' (p => ('not' q))) => ('not' ('not' ('X' (p => ('not' q))))) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' (p => ('not' q))) => ('not' ('not' ('X' (p => ('not' q))))) by LTLAXIO1:42;
then X |- (('X' p) => ('not' ('X' q))) => ('not' ('not' ('X' (p => ('not' q))))) by A3, LTLAXIO1:47;
then X |- (('X' p) => ('not' ('X' q))) => ('not' ('X' ('not' (p => ('not' q))))) by A4, LTLAXIO1:47;
then X |- ('not' ('not' ('X' ('not' (p => ('not' q)))))) => ('not' (('X' p) => ('not' ('X' q)))) by LTLAXIO1:52;
hence X |- ('X' (p '&&' q)) => (('X' p) '&&' ('X' q)) by A5, LTLAXIO1:47; :: thesis: verum