let A, B be Element of LTLB_WFF ; :: thesis: for P being consistent PNPair st A in rng P & B in rng P & A => B in rng P holds
( A => B in rng (P `1) iff ( A in rng (P `2) or B in rng (P `1) ) )
let P be consistent PNPair; :: thesis: ( A in rng P & B in rng P & A => B in rng P implies ( A => B in rng (P `1) iff ( A in rng (P `2) or B in rng (P `1) ) ) )
assume that
A1: A in rng P and
A2: B in rng P and
A3: A => B in rng P ; :: thesis: ( A => B in rng (P `1) iff ( A in rng (P `2) or B in rng (P `1) ) )
set p = P ^ ;
set pa = (P ^) => A;
set pna = (P ^) => ('not' A);
set pb = (P ^) => B;
set pnb = (P ^) => ('not' B);
set pab = (P ^) => (A => B);
set pnab = (P ^) => ('not' (A => B));
set np = 'not' (P ^);

hereby :: thesis: ( ( A in rng (P `2) or B in rng (P `1) ) implies A => B in rng (P `1) )

((P ^) => A) => (((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^)))) is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . (((P ^) => A) => (((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^))))) = 1
set v = VAL g;
set vf = (VAL g) . TFALSUM;
A4: ( (VAL g) . A = 1 or (VAL g) . A = 0 ) by XBOOLEAN:def 3;
A5: ( (VAL g) . B = 1 or (VAL g) . B = 0 ) by XBOOLEAN:def 3;
A6: ( (VAL g) . (P ^) = 1 or (VAL g) . (P ^) = 0 ) by XBOOLEAN:def 3;
A7: ( (VAL g) . TFALSUM = 0 & (VAL g) . ((P ^) => A) = ((VAL g) . (P ^)) => ((VAL g) . A) ) by LTLAXIO1:def 15;
A8: (VAL g) . ((P ^) => (A => B)) = ((VAL g) . (P ^)) => ((VAL g) . (A => B)) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => (((VAL g) . A) => ((VAL g) . B)) by LTLAXIO1:def 15 ;
A9: (VAL g) . ((P ^) => ('not' B)) = ((VAL g) . (P ^)) => ((VAL g) . ('not' B)) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => (((VAL g) . B) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15 ;
thus (VAL g) . (((P ^) => A) => (((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^))))) = ((VAL g) . ((P ^) => A)) => ((VAL g) . (((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^))))) by LTLAXIO1:def 15
.= ((VAL g) . ((P ^) => A)) => (((VAL g) . ((P ^) => ('not' B))) => ((VAL g) . (((P ^) => (A => B)) => ('not' (P ^))))) by LTLAXIO1:def 15
.= ((VAL g) . ((P ^) => A)) => (((VAL g) . ((P ^) => ('not' B))) => (((VAL g) . ((P ^) => (A => B))) => ((VAL g) . ('not' (P ^))))) by LTLAXIO1:def 15
.= 1 by A4, A5, A6, A7, A8, LTLAXIO1:def 15, A9 ; :: thesis: verum

end;

then ((P ^) => A) => (((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^)))) in LTL_axioms by LTLAXIO1:def 17;
then A10: {} LTLB_WFF |- ((P ^) => A) => (((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^)))) by LTLAXIO1:42;
assume A => B in rng (P `1) ; :: thesis: ( not A in rng (P `2) implies B in rng (P `1) )
then A11: {} LTLB_WFF |- (P ^) => (A => B) by Th28;
assume that
A12: not A in rng (P `2) and
A13: not B in rng (P `1) ; :: thesis: contradiction
B in rng (P `2) by A13, A2, XBOOLE_0:def 3;
then A14: {} LTLB_WFF |- (P ^) => ('not' B) by Th29;
A in rng (P `1) by A12, A1, XBOOLE_0:def 3;
then {} LTLB_WFF |- (P ^) => A by Th28;
then {} LTLB_WFF |- ((P ^) => ('not' B)) => (((P ^) => (A => B)) => ('not' (P ^))) by A10, LTLAXIO1:43;
then {} LTLB_WFF |- ((P ^) => (A => B)) => ('not' (P ^)) by LTLAXIO1:43, A14;
hence contradiction by LTLAXIO1:43, A11, Def10; :: thesis: verum

end;

assume A15: ( A in rng (P `2) or B in rng (P `1) ) ; :: thesis: A => B in rng (P `1)
assume not A => B in rng (P `1) ; :: thesis: contradiction
then A => B in rng (P `2) by XBOOLE_0:def 3, A3;
then A16: {} LTLB_WFF |- (P ^) => ('not' (A => B)) by Th29;

per cases ( A in rng (P `2) or B in rng (P `1) ) by A15;

suppose A17: A in rng (P `2) ; :: thesis: contradiction

((P ^) => ('not' A)) => (((P ^) => ('not' (A => B))) => ('not' (P ^))) is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . (((P ^) => ('not' A)) => (((P ^) => ('not' (A => B))) => ('not' (P ^)))) = 1
set v = VAL g;
set vf = (VAL g) . TFALSUM;
A18: (VAL g) . TFALSUM = 0 by LTLAXIO1:def 15;
A19: ( (VAL g) . A = 1 or (VAL g) . A = 0 ) by XBOOLEAN:def 3;
A20: ( (VAL g) . (P ^) = 1 or (VAL g) . (P ^) = 0 ) by XBOOLEAN:def 3;
A21: (VAL g) . ((P ^) => ('not' A)) = ((VAL g) . (P ^)) => ((VAL g) . ('not' A)) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => (((VAL g) . A) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15 ;
A22: (VAL g) . ((P ^) => ('not' (A => B))) = ((VAL g) . (P ^)) => ((VAL g) . ('not' (A => B))) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => (((VAL g) . (A => B)) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => ((((VAL g) . A) => ((VAL g) . B)) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15 ;
thus (VAL g) . (((P ^) => ('not' A)) => (((P ^) => ('not' (A => B))) => ('not' (P ^)))) = ((VAL g) . ((P ^) => ('not' A))) => ((VAL g) . (((P ^) => ('not' (A => B))) => ('not' (P ^)))) by LTLAXIO1:def 15
.= ((VAL g) . ((P ^) => ('not' A))) => (((VAL g) . ((P ^) => ('not' (A => B)))) => ((VAL g) . ('not' (P ^)))) by LTLAXIO1:def 15
.= 1 by A19, A20, A18, LTLAXIO1:def 15, A21, A22 ; :: thesis: verum

end;

then ((P ^) => ('not' A)) => (((P ^) => ('not' (A => B))) => ('not' (P ^))) in LTL_axioms by LTLAXIO1:def 17;
then A23: {} LTLB_WFF |- ((P ^) => ('not' A)) => (((P ^) => ('not' (A => B))) => ('not' (P ^))) by LTLAXIO1:42;
{} LTLB_WFF |- (P ^) => ('not' A) by A17, Th29;
then {} LTLB_WFF |- ((P ^) => ('not' (A => B))) => ('not' (P ^)) by A23, LTLAXIO1:43;
hence contradiction by LTLAXIO1:43, A16, Def10; :: thesis: verum

end;

suppose A24: B in rng (P `1) ; :: thesis: contradiction

((P ^) => B) => (((P ^) => ('not' (A => B))) => ('not' (P ^))) is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . (((P ^) => B) => (((P ^) => ('not' (A => B))) => ('not' (P ^)))) = 1
set v = VAL g;
set vf = (VAL g) . TFALSUM;
A25: ( (VAL g) . B = 1 or (VAL g) . B = 0 ) by XBOOLEAN:def 3;
A26: ( (VAL g) . (P ^) = 1 or (VAL g) . (P ^) = 0 ) by XBOOLEAN:def 3;
A27: ( (VAL g) . TFALSUM = 0 & (VAL g) . ((P ^) => B) = ((VAL g) . (P ^)) => ((VAL g) . B) ) by LTLAXIO1:def 15;
A28: (VAL g) . ((P ^) => ('not' (A => B))) = ((VAL g) . (P ^)) => ((VAL g) . ('not' (A => B))) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => (((VAL g) . (A => B)) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => ((((VAL g) . A) => ((VAL g) . B)) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15 ;
thus (VAL g) . (((P ^) => B) => (((P ^) => ('not' (A => B))) => ('not' (P ^)))) = ((VAL g) . ((P ^) => B)) => ((VAL g) . (((P ^) => ('not' (A => B))) => ('not' (P ^)))) by LTLAXIO1:def 15
.= ((VAL g) . ((P ^) => B)) => (((VAL g) . ((P ^) => ('not' (A => B)))) => ((VAL g) . ('not' (P ^)))) by LTLAXIO1:def 15
.= 1 by A25, A26, A27, LTLAXIO1:def 15, A28 ; :: thesis: verum

end;

then ((P ^) => B) => (((P ^) => ('not' (A => B))) => ('not' (P ^))) in LTL_axioms by LTLAXIO1:def 17;
then A29: {} LTLB_WFF |- ((P ^) => B) => (((P ^) => ('not' (A => B))) => ('not' (P ^))) by LTLAXIO1:42;
{} LTLB_WFF |- (P ^) => B by A24, Th28;
then {} LTLB_WFF |- ((P ^) => ('not' (A => B))) => ('not' (P ^)) by A29, LTLAXIO1:43;
hence contradiction by LTLAXIO1:43, A16, Def10; :: thesis: verum

end;

end;