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