let P be PNPair; :: thesis: ( P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] implies not P is Inconsistent )

assume A1: P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] ; :: thesis: not P is Inconsistent

not {} LTLB_WFF |= 'not' (P ^)

assume A1: P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] ; :: thesis: not P is Inconsistent

not {} LTLB_WFF |= 'not' (P ^)

proof

hence
P is consistent
by LTLAXIO1:41; :: thesis: verum
reconsider M = NAT --> {} as LTLModel by Th2;

set s = SAT M;

take M ; :: according to LTLAXIO1:def 14 :: thesis: ( M |= {} LTLB_WFF & not M |= 'not' (P ^) )

thus M |= {} LTLB_WFF ; :: thesis: not M |= 'not' (P ^)

(SAT M) . [0,('not' (P ^))] <> 1

end;set s = SAT M;

take M ; :: according to LTLAXIO1:def 14 :: thesis: ( M |= {} LTLB_WFF & not M |= 'not' (P ^) )

thus M |= {} LTLB_WFF ; :: thesis: not M |= 'not' (P ^)

(SAT M) . [0,('not' (P ^))] <> 1

proof

hence
not M |= 'not' (P ^)
; :: thesis: verum
assume
(SAT M) . [0,('not' (P ^))] = 1
; :: thesis: contradiction

then (SAT M) . [0,(P ^)] = 0 by LTLAXIO1:5;

then (SAT M) . [0,TVERUM] <> 1 by LTLAXIO1:7, A1, Th27;

hence contradiction by LTLAXIO1:6; :: thesis: verum

end;then (SAT M) . [0,(P ^)] = 0 by LTLAXIO1:5;

then (SAT M) . [0,TVERUM] <> 1 by LTLAXIO1:7, A1, Th27;

hence contradiction by LTLAXIO1:6; :: thesis: verum