let A be Element of LTLB_WFF ; :: thesis: for P being PNPair st A in rng (P `1) holds
{} LTLB_WFF |- (P ^) => A
let P be PNPair; :: thesis: ( A in rng (P `1) implies {} LTLB_WFF |- (P ^) => A )
set fp = P `1 ;
set fm = P `2 ;
set nfm = nega (P `2);
assume A in rng (P `1) ; :: thesis: {} LTLB_WFF |- (P ^) => A
then consider i being Nat such that
A1: i in dom (P `1) and
A2: (P `1) . i = A by FINSEQ_2:10;
(P ^) => A is ctaut
proof
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . ((P ^) => A) = 1
set v = VAL g;
set r = (VAL g) . H2((P `1) | (i -' 1));
set s = (VAL g) . H2((P `1) /^ i);
A3: ( (VAL g) . A = 1 or (VAL g) . A = 0 ) by XBOOLEAN:def 3;
thus (VAL g) . ((P ^) => A) = ((VAL g) . (P ^)) => ((VAL g) . A) by LTLAXIO1:def 15
.= (((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega (P `2)))) => ((VAL g) . A) by LTLAXIO1:31
.= (((((VAL g) . H2((P `1) | (i -' 1))) '&' ((VAL g) . ((P `1) /. i))) '&' ((VAL g) . H2((P `1) /^ i))) '&' ((VAL g) . H2( nega (P `2)))) => ((VAL g) . A) by LTLAXIO2:18, A1
.= (((((VAL g) . H2((P `1) | (i -' 1))) '&' ((VAL g) . A)) '&' ((VAL g) . H2((P `1) /^ i))) '&' ((VAL g) . H2( nega (P `2)))) => ((VAL g) . A) by PARTFUN1:def 6, A1, A2
.= 1 by A3 ; :: thesis: verum
end;
then (P ^) => A in LTL_axioms by LTLAXIO1:def 17;
hence {} LTLB_WFF |- (P ^) => A by LTLAXIO1:42; :: thesis: verum