let P be PNPair; :: thesis: for Q being Element of untn P holds {} LTLB_WFF |- (P ^) => ('X' (Q ^))
let Q be Element of untn P; :: thesis: {} LTLB_WFF |- (P ^) => ('X' (Q ^))
set p = 'X' H₂(Q `1 );
set q = 'X' H<sub>2</sub>( nega (Q `2));
Q in untn P ;
then A1: ex Q1 being PNPair st
( Q = Q1 & rng (Q1 `1) = untn (rng (P `1)) & rng (Q1 `2) = untn (rng (P `2)) ) ;

now :: thesis: for i being Nat st i in dom (nex (nega (Q `2))) holds
{} LTLB_WFF |- (P ^) => ((nex (nega (Q `2))) /. i)

let i be Nat; :: thesis: ( i in dom (nex (nega (Q `2))) implies {} LTLB_WFF |- (P ^) => ((nex (nega (Q `2))) /. i) )
assume A2: i in dom (nex (nega (Q `2))) ; :: thesis: {} LTLB_WFF |- (P ^) => ((nex (nega (Q `2))) /. i)
A3: len (nex (nega (Q `2))) = len (nega (Q `2)) by LTLAXIO2:def 5;
then len (nex (nega (Q `2))) = len (Q `2) by LTLAXIO2:def 4;
then A4: i in dom (Q `2) by FINSEQ_3:29, A2;
then (Q `2) /. i in untn (rng (P `2)) by PARTFUN2:2, A1;
then consider A, B being Element of LTLB_WFF such that
A5: (Q `2) /. i = untn (A,B) and
A6: A 'U' B in rng (P `2) ;
i in dom (nega (Q `2)) by A3, A2, FINSEQ_3:29;
then A7: (nex (nega (Q `2))) /. i = 'X' ((nega (Q `2)) /. i) by LTLAXIO2:9
.= 'X' ('not' ((Q `2) /. i)) by LTLAXIO2:8, A4 ;
( {} LTLB_WFF |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B)))) & {} LTLB_WFF |- (P ^) => ('not' (A 'U' B)) ) by LTLAXIO2:63, LTLAXIO3:29, A6;
hence {} LTLB_WFF |- (P ^) => ((nex (nega (Q `2))) /. i) by A7, LTLAXIO1:47, A5; :: thesis: verum

end;

then ( {} LTLB_WFF |- H₂( nex (nega (Q `2))) => ('X' H<sub>2</sub>( nega (Q `2))) & {} LTLB_WFF |- (P ^) => H₂( nex (nega (Q `2))) ) by LTLAXIO2:60, LTLAXIO2:56;
then A8: {} LTLB_WFF |- (P ^) => ('X' H<sub>2</sub>( nega (Q `2))) by LTLAXIO1:47;

now :: thesis: for i being Nat st i in dom (nex (Q `1)) holds
{} LTLB_WFF |- (P ^) => ((nex (Q `1)) /. i)

let i be Nat; :: thesis: ( i in dom (nex (Q `1)) implies {} LTLB_WFF |- (P ^) => ((nex (Q `1)) /. i) )
assume A9: i in dom (nex (Q `1)) ; :: thesis: {} LTLB_WFF |- (P ^) => ((nex (Q `1)) /. i)
len (Q `1) = len (nex (Q `1)) by LTLAXIO2:def 5;
then A10: i in dom (Q `1) by A9, FINSEQ_3:29;
then (Q `1) /. i in untn (rng (P `1)) by PARTFUN2:2, A1;
then consider A, B being Element of LTLB_WFF such that
A11: (Q `1) /. i = untn (A,B) and
A12: A 'U' B in rng (P `1) ;
A13: {} LTLB_WFF |- (P ^) => (A 'U' B) by LTLAXIO3:28, A12;
(A 'U' B) => (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) in LTL_axioms by LTLAXIO1:def 17;
then A14: {} LTLB_WFF |- (A 'U' B) => (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) by LTLAXIO1:42;
{} LTLB_WFF |- (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) => ('X' (untn (A,B))) by LTLAXIO2:61;
then A15: {} LTLB_WFF |- (A 'U' B) => ('X' (untn (A,B))) by LTLAXIO1:47, A14;
(nex (Q `1)) /. i = 'X' (untn (A,B)) by A11, LTLAXIO2:9, A10;
hence {} LTLB_WFF |- (P ^) => ((nex (Q `1)) /. i) by A15, LTLAXIO1:47, A13; :: thesis: verum

end;

then ( {} LTLB_WFF |- H₂( nex (Q `1)) => ('X' H<sub>2</sub>(Q `1 )) & {} LTLB_WFF |- (P ^) => H₂( nex (Q `1)) ) by LTLAXIO2:60, LTLAXIO2:56;
then A16: {} LTLB_WFF |- (P ^) => ('X' H<sub>2</sub>(Q `1 )) by LTLAXIO1:47;
((P ^) => ('X' H₂(Q `1 ))) => (((P ^) => ('X' H<sub>2</sub>( nega (Q `2)))) => ((P ^) => (('X' H₂(Q `1 )) '&&' ('X' H<sub>2</sub>( nega (Q `2)))))) is ctaut by LTLAXIO2:40;
then ((P ^) => ('X' H₂(Q `1 ))) => (((P ^) => ('X' H<sub>2</sub>( nega (Q `2)))) => ((P ^) => (('X' H₂(Q `1 )) '&&' ('X' H<sub>2</sub>( nega (Q `2)))))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ((P ^) => ('X' H₂(Q `1 ))) => (((P ^) => ('X' H<sub>2</sub>( nega (Q `2)))) => ((P ^) => (('X' H₂(Q `1 )) '&&' ('X' H<sub>2</sub>( nega (Q `2)))))) by LTLAXIO1:42;
then {} LTLB_WFF |- ((P ^) => ('X' H₂( nega (Q `2)))) => ((P ^) => (('X' H<sub>2</sub>(Q `1 )) '&&' ('X' H₂( nega (Q `2))))) by LTLAXIO1:43, A16;
then A17: {} LTLB_WFF |- (P ^) => (('X' H<sub>2</sub>(Q `1 )) '&&' ('X' H₂( nega (Q `2)))) by LTLAXIO1:43, A8;
{} LTLB_WFF |- (('X' H<sub>2</sub>(Q `1 )) '&&' ('X' H₂( nega (Q `2)))) => ('X' (Q ^)) by LTLAXIO1:53;
hence {} LTLB_WFF |- (P ^) => ('X' (Q ^)) by LTLAXIO1:47, A17; :: thesis: verum