let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF holds X |- (('X' p) 'or' ('X' q)) => ('X' (p 'or' q))
let X be Subset of LTLB_WFF; :: thesis: X |- (('X' p) 'or' ('X' q)) => ('X' (p 'or' 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);
('not' ('X' ('not' (('not' p) '&&' ('not' q))))) => ('X' ('not' ('not' (('not' p) '&&' ('not' q))))) in LTL_axioms by LTLAXIO1:def 17;
then A1: X |- ('not' ('X' ('not' (('not' p) '&&' ('not' q))))) => ('X' ('not' ('not' (('not' p) '&&' ('not' q))))) by LTLAXIO1:42;
('not' ('not' (('not' p) '&&' ('not' q)))) => (('not' p) '&&' ('not' q)) is ctaut by Th25;
then ('not' ('not' (('not' p) '&&' ('not' q)))) => (('not' p) '&&' ('not' q)) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('not' ('not' (('not' p) '&&' ('not' q)))) => (('not' p) '&&' ('not' q)) by LTLAXIO1:42;
then A2: X |- 'X' (('not' ('not' (('not' p) '&&' ('not' q)))) => (('not' p) '&&' ('not' q))) by LTLAXIO1:44;
('X' (('not' ('not' (('not' p) '&&' ('not' q)))) => (('not' p) '&&' ('not' q)))) => (('X' ('not' ('not' (('not' p) '&&' ('not' q))))) => ('X' (('not' p) '&&' ('not' q)))) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' (('not' ('not' (('not' p) '&&' ('not' q)))) => (('not' p) '&&' ('not' q)))) => (('X' ('not' ('not' (('not' p) '&&' ('not' q))))) => ('X' (('not' p) '&&' ('not' q)))) by LTLAXIO1:42;
then X |- ('X' ('not' ('not' (('not' p) '&&' ('not' q))))) => ('X' (('not' p) '&&' ('not' q))) by LTLAXIO1:43, A2;
then A3: X |- ('not' ('X' ('not' (('not' p) '&&' ('not' q))))) => ('X' (('not' p) '&&' ('not' q))) by LTLAXIO1:47, A1;
X |- ('X' (('not' p) '&&' ('not' q))) => (('X' ('not' p)) '&&' ('X' ('not' q))) by Th59;
then A4: X |- ('not' ('X' ('not' (('not' p) '&&' ('not' q))))) => (('X' ('not' p)) '&&' ('X' ('not' q))) by LTLAXIO1:47, A3;
('X' ('not' q)) => ('not' ('X' q)) in LTL_axioms by LTLAXIO1:def 17;
then A5: X |- ('X' ('not' q)) => ('not' ('X' q)) by LTLAXIO1:42;
('not' ('not' ('X' ('not' (('not' p) '&&' ('not' q)))))) => ('X' ('not' (('not' p) '&&' ('not' q)))) is ctaut by Th25;
then ('not' ('not' ('X' ('not' (('not' p) '&&' ('not' q)))))) => ('X' ('not' (('not' p) '&&' ('not' q)))) in LTL_axioms by LTLAXIO1:def 17;
then A6: X |- ('not' ('not' ('X' ('not' (('not' p) '&&' ('not' q)))))) => ('X' ('not' (('not' p) '&&' ('not' q)))) by LTLAXIO1:42;
('X' ('not' p)) => ('not' ('X' p)) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' ('not' p)) => ('not' ('X' p)) by LTLAXIO1:42;
then X |- (('X' ('not' p)) '&&' ('X' ('not' q))) => (('not' ('X' p)) '&&' ('not' ('X' q))) by A5, Th53;
then X |- ('not' ('X' ('not' (('not' p) '&&' ('not' q))))) => (('not' ('X' p)) '&&' ('not' ('X' q))) by LTLAXIO1:47, A4;
then X |- ('not' (('not' ('X' p)) '&&' ('not' ('X' q)))) => ('not' ('not' ('X' ('not' (('not' p) '&&' ('not' q)))))) by LTLAXIO1:52;
hence X |- (('X' p) 'or' ('X' q)) => ('X' (p 'or' q)) by A6, LTLAXIO1:47; :: thesis: verum