let A, B be Element of LTLB_WFF ; for P being consistent complete PNPair
for T being pnptree of P st A 'U' B in rng (P `1) holds
ex R being Element of rngr T st B in rng (R `1)
let P be consistent complete PNPair; for T being pnptree of P st A 'U' B in rng (P `1) holds
ex R being Element of rngr T st B in rng (R `1)
let T be pnptree of P; ( A 'U' B in rng (P `1) implies ex R being Element of rngr T st B in rng (R `1) )
set nb = 'not' B;
set gnb = 'G' ('not' B);
set xgnb = 'X' ('G' ('not' B));
set aub = A 'U' B;
set f = the Enumeration of (rngr T) ^ ;
set xaf = 'X' H1( the Enumeration of (rngr T) ^ );
A1:
rng the Enumeration of (rngr T) ^ = (rngr T) ^
by RLAFFIN3:def 1;
{} in dom T
by TREES_1:22;
then
T . {} in rng T
by FUNCT_1:3;
then A2:
P in rng T
by Def11;
reconsider f = the Enumeration of (rngr T) ^ as FinSequence of LTLB_WFF ;
assume A3:
A 'U' B in rng (P `1)
; ex R being Element of rngr T st B in rng (R `1)
assume A4:
for R being Element of rngr T holds not B in rng (R `1)
; contradiction
then A7:
{} LTLB_WFF |- H1(f) => ('not' B)
by LTLAXIO2:57;
('X' (H1(f) => ('G' ('not' B)))) => (('X' H1( the Enumeration of (rngr T) ^ )) => ('X' ('G' ('not' B)))) in LTL_axioms
by LTLAXIO1:def 17;
then A8:
{} LTLB_WFF |- ('X' (H1(f) => ('G' ('not' B)))) => (('X' H1( the Enumeration of (rngr T) ^ )) => ('X' ('G' ('not' B))))
by LTLAXIO1:42;
{} LTLB_WFF |- H1(f) => ('X' H1( the Enumeration of (rngr T) ^ ))
by Th29, A1;
then
{} LTLB_WFF |- 'X' (H1(f) => ('G' ('not' B)))
by LTLAXIO1:45, A7, LTLAXIO1:44;
then A9:
{} LTLB_WFF |- ('X' H1( the Enumeration of (rngr T) ^ )) => ('X' ('G' ('not' B)))
by A8, LTLAXIO1:43;
consider R being object such that
A10:
R in untn P
by XBOOLE_0:def 1;
reconsider R = R as Element of untn P by A10;
set xr = 'X' (R ^);
set g = the Enumeration of (comp R) ^ ;
reconsider g = the Enumeration of (comp R) ^ as FinSequence of LTLB_WFF ;
A11:
rng g = (comp R) ^
by RLAFFIN3:def 1;
(rngr T) ^ =
((comp R) \/ (rngr T)) ^
by Th28, XBOOLE_1:12, A2
.=
((comp R) ^) \/ ((rngr T) ^)
by Th10
;
then
H1(g) => H1(f) is ctaut
by XBOOLE_1:7, A11, A1, LTLAXIO2:30;
then
H1(g) => H1(f) in LTL_axioms
by LTLAXIO1:def 17;
then A12:
{} LTLB_WFF |- H1(g) => H1(f)
by LTLAXIO1:42;
A13:
{} LTLB_WFF |- (P ^) => ('X' (R ^))
by Th18;
('X' ((R ^) => H1(f))) => (('X' (R ^)) => ('X' H1( the Enumeration of (rngr T) ^ ))) in LTL_axioms
by LTLAXIO1:def 17;
then A14:
{} LTLB_WFF |- ('X' ((R ^) => H1(f))) => (('X' (R ^)) => ('X' H1( the Enumeration of (rngr T) ^ )))
by LTLAXIO1:42;
{} LTLB_WFF |- (R ^) => H1(g)
by A11, Th17;
then
{} LTLB_WFF |- 'X' ((R ^) => H1(f))
by A12, LTLAXIO1:47, LTLAXIO1:44;
then
{} LTLB_WFF |- ('X' (R ^)) => ('X' H1( the Enumeration of (rngr T) ^ ))
by LTLAXIO1:43, A14;
then
{} LTLB_WFF |- (P ^) => ('X' H1( the Enumeration of (rngr T) ^ ))
by LTLAXIO1:47, A13;
then A15:
{} LTLB_WFF |- (P ^) => ('X' ('G' ('not' B)))
by LTLAXIO1:47, A9;
A16:
{} LTLB_WFF |- (P ^) => (A 'U' B)
by LTLAXIO3:28, A3;
(A 'U' B) => ('X' ('F' B)) in LTL_axioms
by LTLAXIO1:def 17;
then A17:
{} LTLB_WFF |- (A 'U' B) => ('X' ('F' B))
by LTLAXIO1:42;
('X' ('F' B)) => ('not' ('X' ('G' ('not' B)))) in LTL_axioms
by LTLAXIO1:def 17;
then
{} LTLB_WFF |- ('X' ('F' B)) => ('not' ('X' ('G' ('not' B))))
by LTLAXIO1:42;
then
{} LTLB_WFF |- (A 'U' B) => ('not' ('X' ('G' ('not' B))))
by A17, LTLAXIO1:47;
then
{} LTLB_WFF |- (P ^) => ('not' ('X' ('G' ('not' B))))
by LTLAXIO1:47, A16;
then
{} LTLB_WFF |- (P ^) => (('X' ('G' ('not' B))) '&&' ('not' ('X' ('G' ('not' B)))))
by A15, LTLAXIO2:52;
then
{} LTLB_WFF |- 'not' (P ^)
by LTLAXIO2:55;
hence
contradiction
by LTLAXIO3:def 10; verum