let P be consistent PNPair; rng (P `1) misses rng (P `2)
assume
not rng (P `1) misses rng (P `2)
; contradiction
then
not (rng (P `1)) /\ (rng (P `2)) = {}
;
then consider x being object such that
A1:
x in (rng (P `1)) /\ (rng (P `2))
by XBOOLE_0:def 1;
x in rng (P `1)
by XBOOLE_0:def 4, A1;
then consider n1 being object such that
A2:
n1 in dom (P `1)
and
A3:
(P `1) . n1 = x
by FUNCT_1:def 3;
x in rng (P `2)
by XBOOLE_0:def 4, A1;
then consider n2 being object such that
A4:
n2 in dom (P `2)
and
A5:
(P `2) . n2 = x
by FUNCT_1:def 3;
reconsider n1 = n1, n2 = n2 as Element of NAT by A2, A4;
x = (P `2) /. n2
by PARTFUN1:def 6, A4, A5;
then reconsider x = x as Element of LTLB_WFF ;
A6:
1 <= n2
by FINSEQ_3:25, A4;
A7:
n2 <= len (P `2)
by FINSEQ_3:25, A4;
'not' (P ^) is ctaut
proof
let g be
Function of
LTLB_WFF,
BOOLEAN;
LTLAXIO1:def 16 (VAL g) . ('not' (P ^)) = 1
set nP2 =
nega (P `2);
set v =
VAL g;
A8:
(
(VAL g) . x = TRUE or
(VAL g) . x = FALSE )
by XBOOLEAN:def 3;
A9:
(VAL g) . ((P `1) /. n1) = (VAL g) . x
by PARTFUN1:def 6, A2, A3;
n2 <= len (nega (P `2))
by A7, LTLAXIO2:def 4;
then A10:
n2 in dom (nega (P `2))
by FINSEQ_3:25, A6;
A11:
(VAL g) . ((nega (P `2)) /. n2) =
(VAL g) . ('not' ((P `2) /. n2))
by LTLAXIO2:8, A4
.=
(VAL g) . ('not' x)
by A4, A5, PARTFUN1:def 6
.=
((VAL g) . x) => ((VAL g) . TFALSUM)
by LTLAXIO1:def 15
.=
((VAL g) . x) => FALSE
by LTLAXIO1:def 15
;
A12:
(VAL g) . (P ^) =
((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega (P `2)))
by LTLAXIO1:31
.=
((((VAL g) . H2((P `1) | (n1 -' 1))) '&' ((VAL g) . ((P `1) /. n1))) '&' ((VAL g) . H2((P `1) /^ n1))) '&' ((VAL g) . H2( nega (P `2)))
by LTLAXIO2:18, A2
.=
((((VAL g) . H2((P `1) | (n1 -' 1))) '&' ((VAL g) . ((P `1) /. n1))) '&' ((VAL g) . H2((P `1) /^ n1))) '&' ((((VAL g) . H2((nega (P `2)) | (n2 -' 1))) '&' ((VAL g) . ((nega (P `2)) /. n2))) '&' ((VAL g) . H2((nega (P `2)) /^ n2)))
by LTLAXIO2:18, A10
.=
0
by A8, A11, A9
;
thus (VAL g) . ('not' (P ^)) =
((VAL g) . (P ^)) => ((VAL g) . TFALSUM)
by LTLAXIO1:def 15
.=
1
by A12
;
verum
end;
then
'not' (P ^) in LTL_axioms
by LTLAXIO1:def 17;
then
{} LTLB_WFF |- 'not' (P ^)
by LTLAXIO1:42;
hence
contradiction
by Def10; verum