let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF holds X |- (('X' p) => ('X' q)) => ('X' (p => q))
let X be Subset of LTLB_WFF; :: thesis: X |- (('X' p) => ('X' q)) => ('X' (p => q))
set pq = p => q;
set npq = 'not' (p => q);
set nq = 'not' q;
set xnq = 'X' ('not' q);
set xq = 'X' q;
set xnpq = 'X' ('not' (p => q));
set xpq = 'X' (p => q);
set nxpq = 'not' ('X' (p => q));
set xp = 'X' p;
set nxq = 'not' ('X' q);
('not' ('X' (p => q))) => ('X' ('not' (p => q))) in LTL_axioms by LTLAXIO1:def 17;
then A1: X |- ('not' ('X' (p => q))) => ('X' ('not' (p => q))) by LTLAXIO1:42;
('not' (p => q)) => p is ctaut by Th31;
then ('not' (p => q)) => p in LTL_axioms by LTLAXIO1:def 17;
then X |- ('not' (p => q)) => p by LTLAXIO1:42;
then A2: X |- 'X' (('not' (p => q)) => p) by LTLAXIO1:44;
(('not' ('X' (p => q))) => ('X' p)) => ((('not' ('X' (p => q))) => ('not' ('X' q))) => (('not' ('X' (p => q))) => ('not' (('X' p) => ('X' q))))) is ctaut by Th47;
then (('not' ('X' (p => q))) => ('X' p)) => ((('not' ('X' (p => q))) => ('not' ('X' q))) => (('not' ('X' (p => q))) => ('not' (('X' p) => ('X' q))))) in LTL_axioms by LTLAXIO1:def 17;
then A3: X |- (('not' ('X' (p => q))) => ('X' p)) => ((('not' ('X' (p => q))) => ('not' ('X' q))) => (('not' ('X' (p => q))) => ('not' (('X' p) => ('X' q))))) by LTLAXIO1:42;
('X' ('not' q)) => ('not' ('X' q)) in LTL_axioms by LTLAXIO1:def 17;
then A4: X |- ('X' ('not' q)) => ('not' ('X' q)) by LTLAXIO1:42;
('not' (p => q)) => ('not' q) is ctaut by Th32;
then ('not' (p => q)) => ('not' q) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('not' (p => q)) => ('not' q) by LTLAXIO1:42;
then A5: X |- 'X' (('not' (p => q)) => ('not' q)) by LTLAXIO1:44;
('X' ('not' (p => q))) => ('not' ('X' (p => q))) in LTL_axioms by LTLAXIO1:def 17;
then A6: X |- ('X' ('not' (p => q))) => ('not' ('X' (p => q))) by LTLAXIO1:42;
('X' (('not' (p => q)) => ('not' q))) => (('X' ('not' (p => q))) => ('X' ('not' q))) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' (('not' (p => q)) => ('not' q))) => (('X' ('not' (p => q))) => ('X' ('not' q))) by LTLAXIO1:42;
then X |- ('X' ('not' (p => q))) => ('X' ('not' q)) by LTLAXIO1:43, A5;
then X |- ('not' ('X' (p => q))) => ('X' ('not' q)) by A1, A6, Th54;
then A7: X |- ('not' ('X' (p => q))) => ('not' ('X' q)) by A4, LTLAXIO1:47;
('X' (('not' (p => q)) => p)) => (('X' ('not' (p => q))) => ('X' p)) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' (('not' (p => q)) => p)) => (('X' ('not' (p => q))) => ('X' p)) by LTLAXIO1:42;
then X |- ('X' ('not' (p => q))) => ('X' p) by A2, LTLAXIO1:43;
then X |- ('not' ('X' (p => q))) => ('X' p) by A6, Th54, A1;
then X |- (('not' ('X' (p => q))) => ('not' ('X' q))) => (('not' ('X' (p => q))) => ('not' (('X' p) => ('X' q)))) by A3, LTLAXIO1:43;
then X |- ('not' ('X' (p => q))) => ('not' (('X' p) => ('X' q))) by LTLAXIO1:43, A7;
then A8: X |- ('not' ('not' (('X' p) => ('X' q)))) => ('not' ('not' ('X' (p => q)))) by LTLAXIO1:52;
(('X' p) => ('X' q)) => ('not' ('not' (('X' p) => ('X' q)))) is ctaut by Th26;
then (('X' p) => ('X' q)) => ('not' ('not' (('X' p) => ('X' q)))) in LTL_axioms by LTLAXIO1:def 17;
then A9: X |- (('X' p) => ('X' q)) => ('not' ('not' (('X' p) => ('X' q)))) by LTLAXIO1:42;
('not' ('not' (('X' p) => ('X' q)))) => (('X' p) => ('X' q)) is ctaut by Th25;
then ('not' ('not' (('X' p) => ('X' q)))) => (('X' p) => ('X' q)) in LTL_axioms by LTLAXIO1:def 17;
then A10: X |- ('not' ('not' (('X' p) => ('X' q)))) => (('X' p) => ('X' q)) by LTLAXIO1:42;
('not' ('not' ('X' (p => q)))) => ('X' (p => q)) is ctaut by Th25;
then ('not' ('not' ('X' (p => q)))) => ('X' (p => q)) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('not' ('not' ('X' (p => q)))) => ('X' (p => q)) by LTLAXIO1:42;
then X |- ('not' ('not' (('X' p) => ('X' q)))) => ('X' (p => q)) by LTLAXIO1:47, A8;
hence X |- (('X' p) => ('X' q)) => ('X' (p => q)) by A9, A10, Th54; :: thesis: verum