ltlaxio2.miz



    begin

    reserve A,B,p,q,r,s for Element of LTLB_WFF ,

i,j,k,n for Element of NAT ,

X for Subset of LTLB_WFF ,

f,f1 for FinSequence of LTLB_WFF ,

g for Function of LTLB_WFF , BOOLEAN ;

    set l = LTLB_WFF ;

    

     Lm1: for f be FinSequence holds (f . 0 ) = 0

    proof

      let f be FinSequence;

       not 0 in ( dom f) by FINSEQ_3: 24;

      hence (f . 0 ) = 0 by FUNCT_1:def 2;

    end;

    registration

      let f be FinSequence, x be empty set;

      cluster (f . x) -> empty;

      coherence by Lm1;

    end

    theorem :: LTLAXIO2:1

    

     Th1: for f be FinSequence st ( len f) > 0 & n > 0 holds ( len (f | n)) > 0

    proof

      let f be FinSequence;

      assume that

       A1: ( len f) > 0 and

       A2: n > 0 ;

      per cases ;

        suppose n <= ( len f);

        hence thesis by FINSEQ_1: 59, A2;

      end;

        suppose n > ( len f);

        hence thesis by FINSEQ_1: 58, A1;

      end;

    end;

    theorem :: LTLAXIO2:2

    

     Th2: for f be FinSequence st ( len f) = 0 holds (f /^ n) = f

    proof

      let f be FinSequence;

      assume

       A1: ( len f) = 0 ;

      per cases ;

        suppose

         A2: n = 0 ;

        

        then ( len (f /^ n)) = (( len f) - n) by RFINSEQ:def 1

        .= 0 by A1, A2;

        then (f /^ n) = {} ;

        hence thesis by A1;

      end;

        suppose n > 0 ;

        then (f /^ n) = {} by A1, RFINSEQ:def 1;

        hence thesis by A1;

      end;

    end;

    theorem :: LTLAXIO2:3

    

     Th3: for f,g be FinSequence st ( rng f) = ( rng g) holds (( len f) = 0 iff ( len g) = 0 )

    proof

      let f,g be FinSequence;

      assume

       A1: ( rng f) = ( rng g);

      hereby

        assume ( len f) = 0 ;

        then f = {} ;

        then g = {} by RELAT_1: 38, A1, RELAT_1: 41;

        hence ( len g) = 0 ;

      end;

      assume ( len g) = 0 ;

      then g = {} ;

      then f = {} by RELAT_1: 38, A1, RELAT_1: 41;

      hence ( len f) = 0 ;

    end;

    definition

      let A, B;

      :: LTLAXIO2:def1

      func untn (A,B) -> Element of LTLB_WFF equals (B 'or' (A '&&' (A 'U' B)));

      coherence ;

    end

    theorem :: LTLAXIO2:4

    

     Th4: (( VAL g) . TVERUM ) = 1

    proof

      

      thus (( VAL g) . TVERUM ) = ((( VAL g) . TFALSUM ) => (( VAL g) . TFALSUM )) by LTLAXIO1:def 15

      .= ( FALSE => (( VAL g) . TFALSUM )) by LTLAXIO1:def 15

      .= 1;

    end;

    set tf = TFALSUM ;

    theorem :: LTLAXIO2:5

    

     Th5: (( VAL g) . (p 'or' q)) = ((( VAL g) . p) 'or' (( VAL g) . q))

    proof

      set v = ( VAL g);

      

       A1: (v . tf) = FALSE by LTLAXIO1:def 15;

      

      thus (v . (p 'or' q)) = ((v . (( 'not' p) '&&' ( 'not' q))) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . ( 'not' p)) '&' (v . ( 'not' q))) => (v . tf)) by LTLAXIO1: 31

      .= ((((v . p) => (v . tf)) '&' (v . ( 'not' q))) => (v . tf)) by LTLAXIO1:def 15

      .= ((((v . p) => (v . tf)) '&' ((v . q) => (v . tf))) => (v . tf)) by LTLAXIO1:def 15

      .= ((v . p) 'or' (v . q)) by A1;

    end;

    notation

      let p;

      synonym p is ctaut for p is LTL_TAUT_OF_PL;

    end

    begin

    definition

      let f;

      :: LTLAXIO2:def2

      func con f -> FinSequence of LTLB_WFF means

      : Def2: ( len it ) = ( len f) & (it . 1) = (f . 1) & for i be Nat st 1 <= i & i < ( len f) holds (it . (i + 1)) = ((it /. i) '&&' (f /. (i + 1))) if ( len f) > 0

      otherwise it = <* TVERUM *>;

      existence

      proof

        defpred P[ Nat, set, set] means ex A, B st A = $2 & B = $3 & B = (A '&&' (f /. ($1 + 1)));

         A1:

        now

          let n be Nat;

          assume 1 <= n & n < ( len f);

          let x be Element of l;

           P[n, x, (x '&&' (f /. (n + 1)))];

          hence ex y be Element of l st P[n, x, y];

        end;

        consider p be FinSequence of l such that

         A2: ( len p) = ( len f) & ((p . 1) = (f /. 1) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (p . n), (p . (n + 1))] from RECDEF_1:sch 4( A1);

        thus ( len f) > 0 implies ex p be FinSequence of l st ( len p) = ( len f) & (p . 1) = (f . 1) & for i be Nat st 1 <= i & i < ( len f) holds (p . (i + 1)) = ((p /. i) '&&' (f /. (i + 1)))

        proof

           A3:

          now

            let i be Nat;

            assume

             A4: 1 <= i & i < ( len f);

            then ex A, B st A = (p . i) & B = (p . (i + 1)) & B = (A '&&' (f /. (i + 1))) by A2;

            hence (p . (i + 1)) = ((p /. i) '&&' (f /. (i + 1))) by FINSEQ_4: 15, A4, A2;

          end;

          assume ( len f) > 0 ;

          then 1 <= ( len f) by NAT_1: 25;

          hence thesis by A3, A2, FINSEQ_4: 15;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of l;

        thus ( len f) > 0 & (( len f1) = ( len f) & (f1 . 1) = (f . 1) & for i be Nat st 1 <= i & i < ( len f) holds (f1 . (i + 1)) = ((f1 /. i) '&&' (f /. (i + 1)))) & (( len f2) = ( len f) & (f2 . 1) = (f . 1) & for i be Nat st 1 <= i & i < ( len f) holds (f2 . (i + 1)) = ((f2 /. i) '&&' (f /. (i + 1)))) implies f1 = f2

        proof

          assume that

           A5: ( len f) > 0 and

           A6: ( len f1) = ( len f) and

           A7: (f1 . 1) = (f . 1) and

           A8: for i be Nat st 1 <= i & i < ( len f) holds (f1 . (i + 1)) = ((f1 /. i) '&&' (f /. (i + 1))) and

           A9: ( len f2) = ( len f) and

           A10: (f2 . 1) = (f . 1) and

           A11: for i be Nat st 1 <= i & i < ( len f) holds (f2 . (i + 1)) = ((f2 /. i) '&&' (f /. (i + 1)));

          

           A12: 1 <= ( len f2) by NAT_1: 25, A5, A9;

          1 <= ( len f1) by A6, NAT_1: 25, A5;

          

          then

           A13: (f1 /. 1) = (f1 . 1) by FINSEQ_4: 15

          .= (f2 /. 1) by FINSEQ_4: 15, A12, A10, A7;

           A14:

          now

            defpred P[ Nat] means $1 < ( len f) implies (f1 . ($1 + 1)) = (f2 . ($1 + 1));

            let n;

            set m = (n -' 1);

            assume

             A15: n in ( dom f1);

            then (1 + ( - 1)) <= (n + ( - 1)) by XREAL_1: 6, FINSEQ_3: 25;

            then

             A16: m = (n - 1) by XREAL_0:def 2;

            then

             A17: (m + 1) <= ( len f) by A6, A15, FINSEQ_3: 25;

            

             A18: for i be Nat st P[i] holds P[(i + 1)]

            proof

              let i be Nat;

              assume

               A19: P[i];

              assume

               A20: (i + 1) < ( len f);

              

               A21: 1 <= (i + 1) by NAT_1: 25;

              per cases by NAT_1: 25;

                suppose

                 A22: i = 0 ;

                

                thus (f1 . ((i + 1) + 1)) = ((f1 /. (i + 1)) '&&' (f /. ((i + 1) + 1))) by A20, A21, A8

                .= (f2 . ((i + 1) + 1)) by A20, A11, A22, A13;

              end;

                suppose i >= 1;

                (f1 /. (i + 1)) = (f2 . (i + 1)) by A19, A20, NAT_1: 12, FINSEQ_4: 15, A6

                .= (f2 /. (i + 1)) by FINSEQ_4: 15, A21, A9, A20;

                

                hence (f1 . ((i + 1) + 1)) = ((f2 /. (i + 1)) '&&' (f /. ((i + 1) + 1))) by A20, A21, A8

                .= (f2 . ((i + 1) + 1)) by A20, A21, A11;

              end;

            end;

            

             A23: P[ 0 ] by A7, A10;

            

             A24: for i be Nat holds P[i] from NAT_1:sch 2( A23, A18);

            thus (f1 . n) = (f2 . n) by A16, A24, A17, XREAL_1: 145;

          end;

          ( dom f1) = ( dom f2) by A6, A9, FINSEQ_3: 29;

          hence thesis by A14, PARTFUN1: 5;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let f, A;

      :: LTLAXIO2:def3

      func impg (f,A) -> FinSequence of LTLB_WFF means ( len it ) = ( len f) & (it . 1) = (( 'G' (f /. 1)) => A) & for i st 1 <= i & i < ( len f) holds (it . (i + 1)) = (( 'G' (f /. (i + 1))) => (it /. i)) if ( len f) > 0

      otherwise it = ( <*> LTLB_WFF );

      existence

      proof

        defpred P[ Nat, set, set] means ex A, B st A = $2 & B = $3 & B = (( 'G' (f /. ($1 + 1))) => A);

         A1:

        now

          let n be Nat;

          assume 1 <= n & n < ( len f);

          let x be Element of l;

           P[n, x, (( 'G' (f /. (n + 1))) => x)];

          hence ex y be Element of l st P[n, x, y];

        end;

        consider p be FinSequence of l such that

         A2: ( len p) = ( len f) & ((p . 1) = (( 'G' (f /. 1)) => A) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (p . n), (p . (n + 1))] from RECDEF_1:sch 4( A1);

        thus ( len f) > 0 implies ex p be FinSequence of l st ( len p) = ( len f) & (p . 1) = (( 'G' (f /. 1)) => A) & for i st 1 <= i & i < ( len f) holds (p . (i + 1)) = (( 'G' (f /. (i + 1))) => (p /. i))

        proof

          assume

           A3: ( len f) > 0 ;

          take p;

          now

            let i;

            assume

             A4: 1 <= i & i < ( len f);

            then ex A, B st A = (p . i) & B = (p . (i + 1)) & B = (( 'G' (f /. (i + 1))) => A) by A2;

            hence (p . (i + 1)) = (( 'G' (f /. (i + 1))) => (p /. i)) by FINSEQ_4: 15, A4, A2;

          end;

          hence thesis by A2, A3;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of l;

        thus ( len f) > 0 & ( len f1) = ( len f) & (f1 . 1) = (( 'G' (f /. 1)) => A) & (for i st 1 <= i & i < ( len f) holds (f1 . (i + 1)) = (( 'G' (f /. (i + 1))) => (f1 /. i))) & ( len f2) = ( len f) & (f2 . 1) = (( 'G' (f /. 1)) => A) & (for i st 1 <= i & i < ( len f) holds (f2 . (i + 1)) = (( 'G' (f /. (i + 1))) => (f2 /. i))) implies f1 = f2

        proof

          assume that

           A5: ( len f) > 0 and

           A6: ( len f1) = ( len f) and

           A7: (f1 . 1) = (( 'G' (f /. 1)) => A) and

           A8: for i st 1 <= i & i < ( len f) holds (f1 . (i + 1)) = (( 'G' (f /. (i + 1))) => (f1 /. i)) and

           A9: ( len f2) = ( len f) and

           A10: (f2 . 1) = (( 'G' (f /. 1)) => A) and

           A11: for i st 1 <= i & i < ( len f) holds (f2 . (i + 1)) = (( 'G' (f /. (i + 1))) => (f2 /. i));

          

           A12: 1 <= ( len f2) by A9, NAT_1: 25, A5;

          1 <= ( len f1) by A6, NAT_1: 25, A5;

          

          then

           A13: (f1 /. 1) = (f1 . 1) by FINSEQ_4: 15

          .= (f2 /. 1) by FINSEQ_4: 15, A12, A10, A7;

           A14:

          now

            defpred P[ Nat] means $1 < ( len f) implies (f1 . ($1 + 1)) = (f2 . ($1 + 1));

            let n;

            set m = (n -' 1);

            assume n in ( dom f1);

            then

             A15: n in ( Seg ( len f1)) by FINSEQ_1:def 3;

            then 1 <= n by FINSEQ_1: 1;

            then (1 + ( - 1)) <= (n + ( - 1)) by XREAL_1: 6;

            then

             A16: m = (n - 1) by XREAL_0:def 2;

            then

             A17: (m + 1) <= ( len f) by A6, A15, FINSEQ_1: 1;

            

             A18: for i be Nat st P[i] holds P[(i + 1)]

            proof

              let i be Nat;

              assume

               A19: P[i];

              assume

               A20: (i + 1) < ( len f);

              

               A21: 1 <= (i + 1) by NAT_1: 25;

              per cases by NAT_1: 25;

                suppose i = 0 ;

                

                hence (f1 . ((i + 1) + 1)) = (( 'G' (f /. ((i + 1) + 1))) => (f2 /. (i + 1))) by A13, A20, A8

                .= (f2 . ((i + 1) + 1)) by A20, A21, A11;

              end;

                suppose i >= 1;

                

                 A22: (f1 /. (i + 1)) = (f1 . (i + 1)) by FINSEQ_4: 15, A6, A20, A21

                .= (f2 /. (i + 1)) by FINSEQ_4: 15, A9, A20, A19, NAT_1: 12;

                

                thus (f1 . ((i + 1) + 1)) = (( 'G' (f /. ((i + 1) + 1))) => (f1 /. (i + 1))) by A20, A21, A8

                .= (f2 . ((i + 1) + 1)) by A20, A21, A11, A22;

              end;

            end;

            

             A23: P[ 0 ] by A7, A10;

            

             A24: for i be Nat holds P[i] from NAT_1:sch 2( A23, A18);

            thus (f1 . n) = (f2 . n) by A16, A24, A17, XREAL_1: 145;

          end;

          ( dom f1) = ( dom f2) by FINSEQ_3: 29, A6, A9;

          hence thesis by A14, PARTFUN1: 5;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let f;

      :: LTLAXIO2:def4

      func nega f -> FinSequence of LTLB_WFF means

      : Def4: ( len it ) = ( len f) & for i st 1 <= i & i <= ( len f) holds (it . i) = ( 'not' (f /. i));

      existence

      proof

        defpred P1[ set, set] means $2 = ( 'not' (f /. $1));

        

         A1: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of l st P1[k, x];

        consider p be FinSequence of l such that

         A2: ( dom p) = ( Seg ( len f)) & for k be Nat st k in ( Seg ( len f)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A1);

         A3:

        now

          let i;

          assume 1 <= i & i <= ( len f);

          then i in ( Seg ( len f));

          hence (p . i) = ( 'not' (f /. i)) by A2;

        end;

        ( len p) = ( len f) by A2, FINSEQ_1:def 3;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of l such that

         A4: ( len f1) = ( len f) and

         A5: for i st 1 <= i & i <= ( len f) holds (f1 . i) = ( 'not' (f /. i)) and

         A6: ( len f2) = ( len f) and

         A7: for i st 1 <= i & i <= ( len f) holds (f2 . i) = ( 'not' (f /. i));

         A8:

        now

          let x be Element of NAT such that

           A9: x in ( dom f1);

          x in ( Seg ( len f1)) by A9, FINSEQ_1:def 3;

          then

           A10: 1 <= x & x <= ( len f) by FINSEQ_1: 1, A4;

          

          hence (f1 . x) = ( 'not' (f /. x)) by A5

          .= (f2 . x) by A7, A10;

        end;

        ( dom f1) = ( Seg ( len f1)) by FINSEQ_1:def 3

        .= ( dom f2) by A4, A6, FINSEQ_1:def 3;

        hence f1 = f2 by A8, PARTFUN1: 5;

      end;

    end

    deffunc alt( FinSequence of l) = ( 'not' (( con ( nega $1)) /. ( len ( con ( nega $1)))));

    deffunc kon( FinSequence of l) = (( con $1) /. ( len ( con $1)));

    definition

      let f;

      :: LTLAXIO2:def5

      func nex f -> FinSequence of LTLB_WFF means

      : Def5: ( len it ) = ( len f) & for i st 1 <= i & i <= ( len f) holds (it . i) = ( 'X' (f /. i));

      existence

      proof

        defpred P1[ set, set] means $2 = ( 'X' (f /. $1));

        

         A1: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of l st P1[k, x];

        consider p be FinSequence of l such that

         A2: ( dom p) = ( Seg ( len f)) & for k be Nat st k in ( Seg ( len f)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A1);

         A3:

        now

          let i;

          assume 1 <= i & i <= ( len f);

          then i in ( Seg ( len f));

          hence (p . i) = ( 'X' (f /. i)) by A2;

        end;

        ( len p) = ( len f) by A2, FINSEQ_1:def 3;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of l such that

         A4: ( len f1) = ( len f) and

         A5: for i st 1 <= i & i <= ( len f) holds (f1 . i) = ( 'X' (f /. i)) and

         A6: ( len f2) = ( len f) and

         A7: for i st 1 <= i & i <= ( len f) holds (f2 . i) = ( 'X' (f /. i));

         A8:

        now

          let x be Element of NAT such that

           A9: x in ( dom f1);

          x in ( Seg ( len f1)) by A9, FINSEQ_1:def 3;

          then

           A10: 1 <= x & x <= ( len f) by FINSEQ_1: 1, A4;

          

          hence (f1 . x) = ( 'X' (f /. x)) by A5

          .= (f2 . x) by A7, A10;

        end;

        ( dom f1) = ( Seg ( len f1)) by FINSEQ_1:def 3

        .= ( dom f2) by FINSEQ_1:def 3, A4, A6;

        hence f1 = f2 by A8, PARTFUN1: 5;

      end;

    end

    theorem :: LTLAXIO2:6

    

     Th6: ( len f) > 0 implies (( con f) /. 1) = (f /. 1)

    proof

      assume

       A1: ( len f) > 0 ;

      then

       A2: 1 <= ( len f) by NAT_1: 25;

      then ( len ( con f)) >= 1 by Def2;

      

      hence (( con f) /. 1) = (( con f) . 1) by FINSEQ_4: 15

      .= (f . 1) by Def2, A1

      .= (f /. 1) by FINSEQ_4: 15, A2;

    end;

    theorem :: LTLAXIO2:7

    

     Th7: for i be Nat st 1 <= i & i < ( len f) holds (( con f) /. (i + 1)) = ((( con f) /. i) '&&' (f /. (i + 1)))

    proof

      let i be Nat;

      assume that

       A1: 1 <= i and

       A2: i < ( len f);

      reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

      i < ( len ( con f)) by A2, Def2;

      then (i + 1) <= ( len ( con f)) by NAT_1: 13;

      

      hence (( con f) /. (i + 1)) = (( con f) . (i1 + 1)) by FINSEQ_4: 15, NAT_1: 12

      .= ((( con f) /. i) '&&' (f /. (i + 1))) by Def2, A1, A2;

    end;

    theorem :: LTLAXIO2:8

    

     Th8: for i be Nat st i in ( dom f) holds (( nega f) /. i) = ( 'not' (f /. i))

    proof

      let i be Nat;

      reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

      assume

       A1: i in ( dom f);

      then

       A2: 1 <= i by FINSEQ_3: 25;

      

       A3: i <= ( len f) by A1, FINSEQ_3: 25;

      then i <= ( len ( nega f)) by Def4;

      

      hence (( nega f) /. i) = (( nega f) . i1) by A2, FINSEQ_4: 15

      .= ( 'not' (f /. i)) by Def4, A2, A3;

    end;

    theorem :: LTLAXIO2:9

    for i be Nat st i in ( dom f) holds (( nex f) /. i) = ( 'X' (f /. i))

    proof

      let i be Nat;

      reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

      assume

       A1: i in ( dom f);

      then

       A2: 1 <= i by FINSEQ_3: 25;

      

       A3: i <= ( len f) by A1, FINSEQ_3: 25;

      then i <= ( len ( nex f)) by Def5;

      

      hence (( nex f) /. i) = (( nex f) . i1) by A2, FINSEQ_4: 15

      .= ( 'X' (f /. i)) by Def5, A2, A3;

    end;

    theorem :: LTLAXIO2:10

    

     Th10: (( con ( <*> LTLB_WFF )) /. ( len ( con ( <*> LTLB_WFF )))) = TVERUM

    proof

      

       A1: ( len ( <*> l)) = 0 ;

      then ( con ( <*> l)) = <* TVERUM *> by Def2;

      then

       A2: ( len ( con ( <*> l))) = 1 by FINSEQ_1: 39;

      

      hence kon(<*>) = (( con ( <*> l)) . ( len ( con ( <*> l)))) by FINSEQ_4: 15

      .= ( <* TVERUM *> . ( len ( con ( <*> l)))) by Def2, A1

      .= TVERUM by FINSEQ_1: 40, A2;

    end;

    theorem :: LTLAXIO2:11

    

     Th11: (( con <*A*>) /. ( len ( con <*A*>))) = A

    proof

      set f = <*A*>;

      

       A1: ( len f) = 1 by FINSEQ_1: 39;

      

      thus kon(f) = (( con f) /. ( len f)) by Def2

      .= (f /. 1) by Th6, A1

      .= A by FINSEQ_4: 16;

    end;

    theorem :: LTLAXIO2:12

    

     Th12: for k,n be Nat holds n <= k implies (( con f) . n) = (( con (f | k)) . n)

    proof

      let k,n be Nat;

      defpred P[ Nat] means $1 <= k implies (( con f) . $1) = (( con (f | k)) . $1);

       A1:

      now

        let i be Nat;

        assume

         A2: P[i];

        thus P[(i + 1)]

        proof

          assume

           A3: (i + 1) <= k;

          then

           A4: 1 <= k by NAT_1: 25;

          

           A5: i < k by A3, NAT_1: 13;

          per cases ;

            suppose

             A6: k <= ( len f);

            then

             A7: ( len (f | k)) = k by FINSEQ_1: 59;

            

             A8: i < ( len (f | k)) by A5, FINSEQ_1: 59, A6;

            then

             A9: i < ( len ( con (f | k))) by Def2;

            (i + 1) <= ( len f) by A6, A3, XXREAL_0: 2;

            then

             A10: i < ( len f) by NAT_1: 13;

            then

             A11: i < ( len ( con f)) by Def2;

            per cases by NAT_1: 25;

              suppose

               A12: i = 0 ;

              

              hence (( con f) . (i + 1)) = (f . 1) by Def2, A6, A3

              .= ((f | k) . 1) by A4, FINSEQ_3: 112

              .= (( con (f | k)) . (i + 1)) by Def2, A12, A7, A3;

            end;

              suppose

               A13: 1 <= i;

              1 <= (i + 1) by XREAL_1: 31;

              then

               A14: (i + 1) in ( Seg k) by A3;

              k in ( Seg ( len f)) by A6, A4;

              then k in ( dom f) by FINSEQ_1:def 3;

              then

               A15: (f /. (i + 1)) = ((f | k) /. (i + 1)) by A14, FINSEQ_4: 71;

              

               A16: (( con f) /. i) = (( con f) . i) by A11, A13, FINSEQ_4: 15

              .= (( con (f | k)) /. i) by A9, A13, FINSEQ_4: 15, A2, A3, NAT_1: 13;

              

              thus (( con f) . (i + 1)) = ((( con f) /. i) '&&' (f /. (i + 1))) by Def2, A10, A13

              .= (( con (f | k)) . (i + 1)) by Def2, A13, A8, A15, A16;

            end;

          end;

            suppose k > ( len f);

            hence (( con f) . (i + 1)) = (( con (f | k)) . (i + 1)) by FINSEQ_1: 58;

          end;

        end;

      end;

      (( con f) . 0 ) = 0

      .= (( con (f | k)) . 0 );

      then

       A17: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A17, A1);

      hence thesis;

    end;

    theorem :: LTLAXIO2:13

    

     Th13: for k,n be Nat holds (n <= k & 1 <= n & n <= ( len f) implies (( con f) /. n) = (( con (f | k)) /. n))

    proof

      let k,n be Nat;

      assume that

       A1: n <= k and

       A2: 1 <= n and

       A3: n <= ( len f);

      

       A4: n <= ( len ( con f)) by A2, A3, Def2;

      per cases ;

        suppose k <= ( len f);

        then

         A5: n <= ( len (f | k)) by FINSEQ_1: 59, A1;

        then

         A6: ( len ( con (f | k))) = ( len (f | k)) by A2, Def2;

        

        thus (( con f) /. n) = (( con f) . n) by FINSEQ_4: 15, A2, A4

        .= (( con (f | k)) . n) by Th12, A1

        .= (( con (f | k)) /. n) by FINSEQ_4: 15, A2, A6, A5;

      end;

        suppose k > ( len f);

        hence (( con f) /. n) = (( con (f | k)) /. n) by FINSEQ_1: 58;

      end;

    end;

    theorem :: LTLAXIO2:14

    ( nega <*A*>) = <*( 'not' A)*>

    proof

       A1:

      now

        let n;

        assume that

         A2: 1 <= n and

         A3: n <= ( len <*A*>);

        n <= 1 by A3, FINSEQ_1: 39;

        then

         A4: n = 1 by A2, NAT_1: 25;

        

        hence ( <*( 'not' A)*> . n) = ( 'not' A) by FINSEQ_1: 40

        .= ( 'not' ( <*A*> /. n)) by FINSEQ_4: 16, A4;

      end;

      ( len <*( 'not' A)*>) = 1 by FINSEQ_1: 39

      .= ( len <*A*>) by FINSEQ_1: 39;

      hence thesis by A1, Def4;

    end;

    theorem :: LTLAXIO2:15

    ( nega (f ^ <*A*>)) = (( nega f) ^ <*( 'not' A)*>)

    proof

      set p = ( nega (f ^ <*A*>)), q = (( nega f) ^ <*( 'not' A)*>);

      ( len p) = ( len (f ^ <*A*>)) by Def4;

      then

       A1: ( dom p) = ( dom (f ^ <*A*>)) by FINSEQ_3: 29;

      

       A2: ( len p) = ( len (f ^ <*A*>)) by Def4

      .= (( len f) + ( len <*A*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by FINSEQ_1: 39

      .= (( len ( nega f)) + 1) by Def4

      .= (( len ( nega f)) + ( len <*( 'not' A)*>)) by FINSEQ_1: 39

      .= ( len q) by FINSEQ_1: 22;

      now

        let j be Nat;

        

         A3: ( len (f ^ <*A*>)) = (( len f) + ( len <*A*>)) by FINSEQ_1: 22

        .= (( len f) + 1) by FINSEQ_1: 39;

        assume

         A4: j in ( dom p);

        then

         A5: 1 <= j by FINSEQ_3: 25;

        j <= ( len p) by A4, FINSEQ_3: 25;

        then

         A6: j <= (( len f) + 1) by A3, Def4;

        

         A7: j in ( dom q) by A4, A2, FINSEQ_3: 29;

        per cases by A6, XXREAL_0: 1;

          suppose

           A8: j = (( len f) + 1);

          then

           A9: j = (( len ( nega f)) + 1) by Def4;

          

          thus (p . j) = (p /. j) by PARTFUN1:def 6, A4

          .= ( 'not' ((f ^ <*A*>) /. j)) by Th8, A4, A1

          .= ( 'not' A) by FINSEQ_4: 67, A8

          .= (q /. j) by A9, FINSEQ_4: 67

          .= (q . j) by PARTFUN1:def 6, A7;

        end;

          suppose j < (( len f) + 1);

          then

           A10: j <= ( len f) by NAT_1: 13;

          then

           A11: j in ( dom f) by A5, FINSEQ_3: 25;

          j <= ( len ( nega f)) by A10, Def4;

          then

           A12: j in ( dom ( nega f)) by FINSEQ_3: 25, A5;

          

          thus (p . j) = (p /. j) by PARTFUN1:def 6, A4

          .= ( 'not' ((f ^ <*A*>) /. j)) by Th8, A4, A1

          .= ( 'not' (f /. j)) by FINSEQ_4: 68, A11

          .= (( nega f) /. j) by Th8, A11

          .= (q /. j) by FINSEQ_4: 68, A12

          .= (q . j) by PARTFUN1:def 6, A7;

        end;

      end;

      hence thesis by FINSEQ_2: 9, A2;

    end;

    theorem :: LTLAXIO2:16

    ( nega (f ^ f1)) = (( nega f) ^ ( nega f1))

    proof

      set c1 = ( nega (f ^ f1)), c2 = (( nega f) ^ ( nega f1));

      

       A1: ( len c1) = ( len (f ^ f1)) by Def4

      .= (( len f) + ( len f1)) by FINSEQ_1: 22

      .= (( len f) + ( len ( nega f1))) by Def4

      .= (( len ( nega f)) + ( len ( nega f1))) by Def4

      .= ( len c2) by FINSEQ_1: 22;

      now

        let j be Nat;

        assume

         A2: j in ( dom c1);

        then

         A3: 1 <= j by FINSEQ_3: 25;

        j <= ( len c1) by A2, FINSEQ_3: 25;

        then

         A4: j <= ( len (f ^ f1)) by Def4;

        then

         A5: j in ( dom (f ^ f1)) by FINSEQ_3: 25, A3;

        

         A6: j in ( dom c2) by A2, A1, FINSEQ_3: 29;

        per cases ;

          suppose

           A7: j <= ( len f);

          then j <= ( len ( nega f)) by Def4;

          then

           A8: j in ( dom ( nega f)) by A3, FINSEQ_3: 25;

          

           A9: j in ( dom f) by A7, A3, FINSEQ_3: 25;

          

          thus (c1 . j) = (c1 /. j) by PARTFUN1:def 6, A2

          .= ( 'not' ((f ^ f1) /. j)) by Th8, A5

          .= ( 'not' (f /. j)) by FINSEQ_4: 68, A9

          .= (( nega f) /. j) by Th8, A9

          .= (c2 /. j) by FINSEQ_4: 68, A8

          .= (c2 . j) by PARTFUN1:def 6, A6;

        end;

          suppose

           A10: j > ( len f);

          then

          consider k be Nat such that

           A11: j = (( len f) + k) by NAT_1: 10;

           A12:

          now

            assume k > ( len f1);

            then j > (( len f1) + ( len f)) by XREAL_1: 8, A11;

            hence contradiction by A4, FINSEQ_1: 22;

          end;

          k = 0 or k > 0 ;

          then

           A13: 1 <= k by NAT_1: 25, A11, A10;

          then

           A14: k in ( dom f1) by A12, FINSEQ_3: 25;

          

           A15: j = (( len ( nega f)) + k) by A11, Def4;

          k <= ( len ( nega f1)) by Def4, A12;

          then

           A16: k in ( dom ( nega f1)) by A13, FINSEQ_3: 25;

          

          thus (c1 . j) = (c1 /. j) by PARTFUN1:def 6, A2

          .= ( 'not' ((f ^ f1) /. j)) by Th8, A5

          .= ( 'not' (f1 /. k)) by FINSEQ_4: 69, A14, A11

          .= (( nega f1) /. k) by Th8, A14

          .= (c2 /. j) by FINSEQ_4: 69, A16, A15

          .= (c2 . j) by PARTFUN1:def 6, A6;

        end;

      end;

      hence thesis by FINSEQ_2: 9, A1;

    end;

    theorem :: LTLAXIO2:17

    

     Th17: (( VAL g) . (( con (f ^ f1)) /. ( len ( con (f ^ f1))))) = ((( VAL g) . (( con f) /. ( len ( con f)))) '&' (( VAL g) . (( con f1) /. ( len ( con f1)))))

    proof

      set fp = ((f ^ f1) | ( len f)), fk = ((f ^ f1) /^ ( len f)), v = ( VAL g);

      

       A1: fk = f1 by FINSEQ_5: 37;

      

       A2: for f holds (v . kon(f)) = ((v . kon(|)) '&' (v . kon(/^)))

      proof

        let f;

        defpred P[ Nat] means (( VAL g) . kon(f)) = ((( VAL g) . kon(|)) '&' (( VAL g) . kon(/^)));

        ( len (f | 0 )) = 0 ;

        then

         A3: ( con (f | 0 )) = <* TVERUM *> by Def2;

        then ( len ( con (f | 0 ))) = 1 by FINSEQ_1: 39;

        then

         A4: (( con (f | 0 )) /. ( len ( con (f | 0 )))) = TVERUM by FINSEQ_4: 16, A3;

        

         A5: for f, g holds (( VAL g) . kon(f)) = ((( VAL g) . kon(|)) '&' (( VAL g) . kon(/^)))

        proof

          let f, g;

          defpred P[ Nat] means for f st ( len f) = $1 holds (( VAL g) . kon(f)) = ((( VAL g) . kon(|)) '&' (( VAL g) . kon(/^)));

          

           A6: ( len f) = ( len f);

           A7:

          now

            let n be Nat;

            assume

             A8: P[n];

            thus P[(n + 1)]

            proof

              let f;

              set v = ( VAL g), fp1 = (f | 1), fk1 = (f /^ 1), fn = (f | n), fn1 = (f | (n + 1));

              assume

               A9: ( len f) = (n + 1);

              then

               A10: n < ( len f) by NAT_1: 13;

              

               A11: ( len ( con f)) = (n + 1) by Def2, A9;

              

               A12: 1 <= ( len f) by A9, NAT_1: 25;

              

              then

               A13: ( len fk1) = (( len f) - 1) by RFINSEQ:def 1

              .= n by A9;

              ( len fp1) = 1 by A12, FINSEQ_1: 59;

              then

               A14: ( len ( con fp1)) = 1 by Def2;

              

               A15: n <= ( len f) by A9, NAT_1: 13;

              then

               A16: ( len fn) = n by FINSEQ_1: 59;

              

               A17: ( len fn1) = (n + 1) by FINSEQ_1: 59, A9;

              then

               A18: 1 <= ( len fn1) by NAT_1: 11;

              

               A19: 1 <= (n + 1) by NAT_1: 11;

              

              then

               A20: ( len (fn1 /^ 1)) = (( len fn1) - 1) by A17, RFINSEQ:def 1

              .= n by A17;

              per cases ;

                suppose

                 A21: n = 0 ;

                then

                 A22: fk1 = {} by A13;

                ( len ( con f)) = 1 by A21, A9, Def2;

                

                hence (v . kon(f)) = ((v . (( con fp1) /. 1)) '&' TRUE ) by Th13, A21, A9

                .= ((v . kon(fp1)) '&' (v . kon(fk1))) by A14, A22, Th10, Th4;

              end;

                suppose

                 A23: n > 0 ;

                then

                 A24: 1 <= ( len fn) by NAT_1: 25, A16;

                

                 A25: 1 <= n by A23, NAT_1: 25;

                ( len ( con fn)) = ( len fn) by A23, A16, Def2;

                then (( con f) /. n) = kon(fn) by A16, Th13, A25, A15;

                then kon(f) = ( kon(fn) '&&' (f /. (n + 1))) by Th7, A25, A10, A11;

                

                then

                 A26: (v . kon(f)) = ((v . kon(fn)) '&' (v . (f /. (n + 1)))) by LTLAXIO1: 31

                .= (((v . kon(|)) '&' (v . kon(/^))) '&' (v . (f /. (n + 1)))) by A8, A16

                .= (((v . (( con fp1) /. ( len ( con (fn | 1))))) '&' (v . kon(/^))) '&' (v . (f /. (n + 1)))) by A25, FINSEQ_1: 82

                .= (((v . kon(fp1)) '&' (v . kon(/^))) '&' (v . (f /. (n + 1)))) by A25, FINSEQ_1: 82

                .= ((v . kon(fp1)) '&' ((v . kon(/^)) '&' (v . (f /. (n + 1)))))

                .= ((v . kon(fp1)) '&' (v . ( kon(/^) '&&' (f /. (n + 1))))) by LTLAXIO1: 31;

                per cases by A23, NAT_1: 25;

                  suppose

                   A27: n = 1;

                  then

                   A28: 1 in ( dom fk1) by A13, FINSEQ_3: 25;

                  

                   A29: ( len ( con fk1)) = 1 by Def2, A13, A27;

                  

                  thus (v . kon(f)) = (v . ((( con f) /. 1) '&&' (f /. (1 + 1)))) by Th7, A27, A9, A11

                  .= (v . ((( con fp1) /. 1) '&&' (f /. (1 + 1)))) by Th13, A27, A9

                  .= ((v . (( con fp1) /. 1)) '&' (v . (f /. (1 + 1)))) by LTLAXIO1: 31

                  .= ((v . (( con fp1) /. 1)) '&' (v . (fk1 /. 1))) by FINSEQ_5: 27, A28

                  .= ((v . kon(fp1)) '&' (v . kon(fk1))) by A14, A29, Th6, A27, A13;

                end;

                  suppose

                   A30: 1 < n;

                  

                   A31: (fn1 /^ 1) = (fk1 | n)

                  proof

                    set f1 = (fk1 | n), g = (fn1 /^ 1);

                    

                     A32: ( len f1) = ( len g) by A20, FINSEQ_1: 59, A13;

                    now

                      let x be Nat;

                      

                       A33: ( dom f1) c= ( dom fk1) by FINSEQ_5: 18;

                      assume

                       A34: x in ( dom f1);

                      then

                       A35: x in ( dom g) by FINSEQ_3: 29, A32;

                      x <= ( len f1) by A34, FINSEQ_3: 25;

                      then

                       A36: x <= n by FINSEQ_1: 59, A13;

                      

                      hence (f1 . x) = (fk1 . x) by FINSEQ_3: 112

                      .= (f . (x + 1)) by RFINSEQ:def 1, A33, A34, A12

                      .= (fn1 . (x + 1)) by FINSEQ_3: 112, A36, XREAL_1: 6

                      .= (g . x) by RFINSEQ:def 1, A18, A35;

                    end;

                    hence thesis by FINSEQ_2: 9, A32;

                  end;

                  

                   A37: (n + ( - 1)) > (1 + ( - 1)) by A30, XREAL_1: 8;

                  

                  then

                   A38: ((n -' 1) + 1) = ((n - 1) + 1) by XREAL_0:def 2

                  .= n;

                  ( len ( con fk1)) = ( len fk1) by A13, A30, Def2;

                  

                  then

                   A39: ( len ( con fk1)) = (( len f) -' 1) by RFINSEQ: 29

                  .= n by NAT_D: 34, A9;

                  

                   A40: n in ( dom (fn1 /^ 1)) by FINSEQ_3: 25, A30, A20;

                  

                   A41: (n - 1) > 0 by A37;

                  then (n -' 1) > 0 by XREAL_0:def 2;

                  then

                   A42: 1 <= (n -' 1) by NAT_1: 25;

                  

                   A43: (f /. (n + 1)) = (f . (n + 1)) by A19, A9, FINSEQ_4: 15

                  .= (fn1 . (n + 1)) by FINSEQ_3: 112

                  .= ((fn1 /^ 1) . n) by RFINSEQ:def 1, A40, A19, A17

                  .= ((fn1 /^ 1) /. ((n -' 1) + 1)) by A38, PARTFUN1:def 6, A40;

                  

                   A44: (( - 1) + n) < n by XREAL_1: 30;

                  then

                   A45: (n -' 1) < ( len (fn1 /^ 1)) by A20, XREAL_0:def 2, A41;

                  

                   A46: ( len (fn /^ 1)) = (n - 1) by RFINSEQ:def 1, A24, A16;

                  

                  then

                   A47: ( len ( con (fn /^ 1))) = ( len (fn /^ 1)) by A37, Def2

                  .= (n -' 1) by XREAL_0:def 2, A46;

                  then ( len ( con (fn /^ 1))) = (n - 1) by A46, XREAL_0:def 2;

                  then

                   A48: 1 <= ( len ( con (fn /^ 1))) by A37, NAT_1: 25;

                  

                   A49: ( len (fn /^ 1)) = (n -' 1) by XREAL_0:def 2, A46;

                  

                   A50: ((fn1 /^ 1) | (n -' 1)) = (fn /^ 1)

                  proof

                    set f1 = ((fn1 /^ 1) | (n -' 1)), g = (fn /^ 1);

                    

                     A51: ( len f1) = ( len g) by A49, FINSEQ_1: 59, A45;

                    now

                      

                       A52: ( dom f1) c= ( dom (fn1 /^ 1)) by FINSEQ_5: 18;

                      let x be Nat;

                      

                       A53: n <= (n + 1) by XREAL_1: 31;

                      assume

                       A54: x in ( dom f1);

                      then

                       A55: x in ( dom g) by FINSEQ_3: 29, A51;

                      x <= ( len f1) by A54, FINSEQ_3: 25;

                      then

                       A56: x <= (n -' 1) by FINSEQ_1: 59, A45;

                      then

                       A57: (x + 1) <= n by XREAL_1: 6, A38;

                      

                      thus (f1 . x) = ((fn1 /^ 1) . x) by FINSEQ_3: 112, A56

                      .= (fn1 . (x + 1)) by RFINSEQ:def 1, A52, A54, A18

                      .= (f . (x + 1)) by FINSEQ_3: 112, A53, XXREAL_0: 2, A57

                      .= (fn . (x + 1)) by FINSEQ_3: 112, A56, XREAL_1: 6, A38

                      .= (g . x) by RFINSEQ:def 1, A25, A16, A55;

                    end;

                    hence thesis by FINSEQ_2: 9, A51;

                  end;

                  ( len ( con (fn /^ 1))) = ( len (fn /^ 1)) by A46, A37, Def2;

                  

                  then ( kon(/^) '&&' (f /. (n + 1))) = ((( con (fn1 /^ 1)) /. (n -' 1)) '&&' (f /. (n + 1))) by A47, Th13, A48, A46, A44, A20, A50

                  .= (( con (fn1 /^ 1)) /. ((n -' 1) + 1)) by Th7, A45, A42, A43

                  .= (( con fk1) /. ( len ( con fk1))) by A39, A13, A25, Th13, A31, A38;

                  hence (v . kon(f)) = ((v . kon(fp1)) '&' (v . kon(fk1))) by A26;

                end;

              end;

            end;

          end;

          

           A58: P[ 0 ]

          proof

            let f;

            set v = ( VAL g), fp1 = (f | 1), fk1 = (f /^ 1);

            assume

             A59: ( len f) = 0 ;

            then ( len fk1) = 0 by Th2;

            then

             A60: fk1 = {} ;

            f = {} & fp1 = f by A59, FINSEQ_1: 58;

            hence (v . kon(f)) = ((v . kon(fp1)) '&' (v . kon(fk1))) by A60;

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A58, A7);

          hence thesis by A6;

        end;

        

         A61: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume

           A62: P[n];

          set v = ( VAL g), fe = (f /^ n), fs1 = (f | (n + 1)), fs = (f | n), fe1 = (f /^ (n + 1));

          per cases ;

            suppose

             A63: ( len f) = 0 ;

            then

             A64: fe1 = f by Th2;

            

             A65: f = {} by A63;

            then fs1 = {} by FINSEQ_1: 58, A63;

            hence (v . kon(f)) = ((v . kon(fs1)) '&' (v . kon(fe1))) by A64, A65;

          end;

            suppose

             A66: ( len f) > 0 ;

            then ( len f) >= 1 by NAT_1: 25;

            then

             A67: ( len (f | 1)) = 1 by FINSEQ_1: 59;

            then

             A68: 1 in ( dom (f | 1)) by FINSEQ_3: 25;

            

             A69: ( len fs1) > 0 by A66, Th1;

            then ( len fs1) >= 1 by NAT_1: 25;

            then

             A70: 1 in ( dom fs1) by FINSEQ_3: 25;

            

             A71: ( len ( con (f | 1))) = 1 by A67, Def2;

            

             A72: 1 <= (n + 1) by XREAL_1: 31;

            per cases by A69, NAT_1: 25;

              suppose

               A73: ( len fs1) = 1;

              then ( len ( con fs1)) = 1 by Def2;

              

              then

               A74: kon(fs1) = (fs1 /. 1) by Th6, A69

              .= (f /. 1) by FINSEQ_4: 70, A70

              .= ((f | 1) /. 1) by FINSEQ_4: 70, A68

              .= kon(|) by A71, Th6, A67;

              per cases ;

                suppose (n + 1) <= ( len f);

                then ( len fs1) = (n + 1) by FINSEQ_1: 59;

                hence (v . kon(f)) = ((v . kon(fs1)) '&' (v . kon(fe1))) by A73, A5;

              end;

                suppose (n + 1) > ( len f);

                then

                 A75: fe1 = {} by RFINSEQ:def 1;

                then

                 A76: ( len fe1) = 0 ;

                f = (fs1 ^ fe1) by RFINSEQ: 8;

                

                then ( len f) = (( len fs1) + ( len fe1)) by FINSEQ_1: 22

                .= 1 by A73, A76;

                then (f | 1) = f by FINSEQ_1: 58;

                

                hence (v . kon(f)) = ((v . kon(|)) '&' TRUE )

                .= ((v . kon(fs1)) '&' (v . kon(fe1))) by A74, Th10, A75, Th4;

              end;

            end;

              suppose

               A77: ( len fs1) > 1;

              per cases ;

                suppose

                 A78: (n + 1) > ( len f);

                then

                 A79: fe1 = 0 by RFINSEQ:def 1;

                fs1 = f by FINSEQ_1: 58, A78;

                

                hence (v . kon(f)) = ((v . kon(fs1)) '&' TRUE )

                .= ((v . kon(fs1)) '&' (v . kon(fe1))) by A79, Th10, Th4;

              end;

                suppose

                 A80: (n + 1) <= ( len f);

                then

                 A81: ( len fs1) = (n + 1) by FINSEQ_1: 59;

                then

                 A82: (n + 1) in ( dom fs1) by FINSEQ_3: 25, A72;

                

                 A83: (n + 1) = ( len ( con fs1)) & n < ( len fs1) by A81, Def2, XREAL_1: 145;

                

                 A84: ((n + 1) + ( - n)) <= (( len f) + ( - n)) by A80, XREAL_1: 6;

                

                 A85: ( len fe) = (( len f) -' n) by RFINSEQ: 29

                .= (( len f) - n) by XREAL_0:def 2, A84;

                then

                 A86: ( len (fe | 1)) = 1 by A84, FINSEQ_1: 59;

                then

                 A87: 1 in ( dom (fe | 1)) by FINSEQ_3: 25;

                

                 A88: 1 in ( dom fe) by A85, A84, FINSEQ_3: 25;

                ( len ( con (fe | 1))) = 1 by A86, Def2;

                

                then

                 A89: kon(|) = ((fe | 1) /. 1) by Th6, A86

                .= (fe /. 1) by A87, FINSEQ_4: 70

                .= (f /. (n + 1)) by FINSEQ_5: 27, A88

                .= (fs1 /. (n + 1)) by FINSEQ_4: 70, A82;

                

                 A90: ((f /^ n) /^ 1) = fe1 by FINSEQ_6: 81;

                

                 A91: ((n + 1) + ( - 1)) > (1 + ( - 1)) by A77, A81, XREAL_1: 8;

                then

                 A92: n >= 1 by NAT_1: 25;

                

                 A93: n <= (n + 1) by XREAL_1: 31;

                then ( len fs) = n by XXREAL_0: 2, A80, FINSEQ_1: 59;

                then

                 A94: ( len ( con fs)) = n by Def2, A91;

                

                 A95: kon(|) = (( con (fs1 | n)) /. ( len ( con fs))) by FINSEQ_5: 77, A93

                .= (( con fs1) /. n) by A94, Th13, A93, A81, A92;

                

                 A96: 1 <= n by NAT_1: 25, A91;

                

                thus (v . kon(f)) = ((v . kon(|)) '&' ((v . kon(|)) '&' (v . kon(/^)))) by A5, A62

                .= (((v . kon(|)) '&' (v . kon(|))) '&' (v . kon(fe1))) by A90

                .= ((v . ( kon(|) '&&' kon(|))) '&' (v . kon(fe1))) by LTLAXIO1: 31

                .= ((v . kon(fs1)) '&' (v . kon(fe1))) by A83, Th7, A96, A95, A89;

              end;

            end;

          end;

        end;

        (f /^ 0 ) = f by FINSEQ_5: 28;

        

        then (( VAL g) . kon(f)) = ( TRUE '&' (( VAL g) . kon(/^)))

        .= ((( VAL g) . kon(|)) '&' (( VAL g) . kon(/^))) by A4, Th4;

        then

         A97: P[ 0 ];

        for n be Nat holds P[n] from NAT_1:sch 2( A97, A61);

        hence thesis;

      end;

      ( Seg ( len f)) c= ( dom f) by FINSEQ_1:def 3;

      

      then fp = (f | ( len f)) by FINSEQ_6: 11

      .= f by FINSEQ_1: 58;

      hence (v . kon(^)) = ((v . kon(f)) '&' (v . kon(f1))) by A1, A2;

    end;

    theorem :: LTLAXIO2:18

    n in ( dom f) implies (( VAL g) . (( con f) /. ( len ( con f)))) = (((( VAL g) . (( con (f | (n -' 1))) /. ( len ( con (f | (n -' 1)))))) '&' (( VAL g) . (f /. n))) '&' (( VAL g) . (( con (f /^ n)) /. ( len ( con (f /^ n))))))

    proof

      set v = ( VAL g);

      assume n in ( dom f);

      then

       A1: 1 <= n & n <= ( len f) by FINSEQ_3: 25;

      

      then f = (((f | (n -' 1)) ^ <*(f . n)*>) ^ (f /^ n)) by FINSEQ_5: 84

      .= (((f | (n -' 1)) ^ <*(f /. n)*>) ^ (f /^ n)) by FINSEQ_4: 15, A1;

      

      hence (v . kon(f)) = ((v . kon(^)) '&' (v . kon(/^))) by Th17

      .= (((v . kon(|)) '&' (v . kon(<*))) '&' (v . kon(/^))) by Th17

      .= (((v . kon(|)) '&' (v . (f /. n))) '&' (v . kon(/^))) by Th11;

    end;

    theorem :: LTLAXIO2:19

    

     Th19: (( VAL g) . (( con f) /. ( len ( con f)))) = 1 iff for i be Nat st i in ( dom f) holds (( VAL g) . (f /. i)) = 1

    proof

      set v = ( VAL g);

      defpred P[ Nat] means $1 <= ( len f) implies (v . kon(|)) = 1;

      hereby

        assume

         A1: (v . kon(f)) = 1;

        given i be Nat such that

         A2: i in ( dom f) and

         A3: not (v . (f /. i)) = 1;

        

         A4: i <= ( len f) by A2, FINSEQ_3: 25;

        (f /. i) = (f . i) & 1 <= i by PARTFUN1:def 6, A2, FINSEQ_3: 25;

        then f = (((f | (i -' 1)) ^ <*(f /. i)*>) ^ (f /^ i)) by A4, FINSEQ_5: 84;

        

        then

         A5: (v . kon(f)) = ((v . kon(^)) '&' (v . kon(/^))) by Th17

        .= (((v . kon(|)) '&' (v . kon(<*))) '&' (v . kon(/^))) by Th17

        .= (((v . kon(|)) '&' (v . kon(/^))) '&' (v . kon(<*)));

        (v . kon(<*)) = (v . (f /. i)) by Th11

        .= 0 by A3, XBOOLEAN:def 3;

        hence contradiction by A5, A1;

      end;

      assume

       A6: for i be Nat st i in ( dom f) holds (v . (f /. i)) = 1;

       A7:

      now

        let k be Nat;

        assume

         A8: P[k];

        thus P[(k + 1)]

        proof

          

           A9: 1 <= (k + 1) by NAT_1: 11;

          assume

           A10: (k + 1) <= ( len f);

          

          then (f | (k + 1)) = ((f | k) ^ <*(f . (k + 1))*>) by NAT_1: 13, FINSEQ_5: 83

          .= ((f | k) ^ <*(f /. (k + 1))*>) by FINSEQ_4: 15, NAT_1: 11, A10;

          

          hence (v . kon(|)) = ((v . kon(|)) '&' (v . kon(<*))) by Th17

          .= ((v . kon(|)) '&' (v . (f /. (k + 1)))) by Th11

          .= 1 by A6, A9, FINSEQ_3: 25, A10, A8, NAT_1: 13;

        end;

      end;

      

       A11: P[ 0 ] by Th10, Th4;

      

       A12: for k be Nat holds P[k] from NAT_1:sch 2( A11, A7);

      f = (f | ( len f)) by FINSEQ_1: 58;

      hence (v . kon(f)) = 1 by A12;

    end;

    theorem :: LTLAXIO2:20

    

     Th20: (( VAL g) . ( 'not' (( con ( nega f)) /. ( len ( con ( nega f)))))) = 0 iff for i be Nat st i in ( dom f) holds (( VAL g) . (f /. i)) = 0

    proof

      set v = ( VAL g);

      

       A1: (v . alt(f)) = ((v . kon(nega)) => (v . TFALSUM )) by LTLAXIO1:def 15

      .= ((v . kon(nega)) => FALSE ) by LTLAXIO1:def 15;

      

       A2: ( len f) = ( len ( nega f)) by Def4;

      hereby

        assume

         A3: (v . alt(f)) = 0 ;

        let i be Nat;

        reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

        assume

         A4: i in ( dom f);

        then

         A5: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

        

         A6: i in ( dom ( nega f)) by A4, FINSEQ_3: 29, A2;

        

        then

         A7: (( nega f) /. i) = (( nega f) . i1) by PARTFUN1:def 6

        .= ( 'not' (f /. i1)) by Def4, A5;

        

         A8: (v . alt(f)) = ((v . kon(nega)) => (v . TFALSUM )) by LTLAXIO1:def 15

        .= ((v . kon(nega)) => FALSE ) by LTLAXIO1:def 15;

        ((v . (f /. i)) => FALSE ) = ((v . (f /. i)) => (v . TFALSUM )) by LTLAXIO1:def 15

        .= (v . ( 'not' (f /. i))) by LTLAXIO1:def 15

        .= 1 by A8, A3, Th19, A6, A7;

        hence (v . (f /. i)) = 0 ;

      end;

      assume

       A9: for i be Nat st i in ( dom f) holds (v . (f /. i)) = 0 ;

      assume not (v . alt(f)) = 0 ;

      then not (v . kon(nega)) = 1 by A1;

      then

      consider i be Nat such that

       A10: i in ( dom ( nega f)) and

       A11: not (v . (( nega f) /. i)) = 1 by Th19;

      

       A12: i <= ( len f) by A2, A10, FINSEQ_3: 25;

      reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

      

       A13: 1 <= i by A10, FINSEQ_3: 25;

      

       A14: (( nega f) /. i) = (( nega f) . i1) by A10, PARTFUN1:def 6

      .= ( 'not' (f /. i)) by Def4, A13, A12;

      

       A15: ((v . (f /. i1)) => FALSE ) = ((v . (f /. i1)) => (v . TFALSUM )) by LTLAXIO1:def 15

      .= (v . ( 'not' (f /. i))) by LTLAXIO1:def 15

      .= 0 by A11, XBOOLEAN:def 3, A14;

      i in ( dom f) by A2, FINSEQ_3: 29, A10;

      hence contradiction by A15, A9;

    end;

    theorem :: LTLAXIO2:21

    ( rng f) = ( rng f1) implies (( VAL g) . (( con f) /. ( len ( con f)))) = (( VAL g) . (( con f1) /. ( len ( con f1))))

    proof

      set v = ( VAL g);

      assume

       A1: ( rng f) = ( rng f1);

      per cases ;

        suppose

         A2: ( len f) = 0 ;

        then ( len f1) = 0 by Th3, A1;

        then

         A3: f1 = {} ;

        f = {} by A2;

        hence (v . kon(f)) = (v . kon(f1)) by A3;

      end;

        suppose ( len f) > 0 ;

        per cases by XBOOLEAN:def 3;

          suppose

           A4: (v . kon(f)) = 1;

          assume not (v . kon(f)) = (v . kon(f1));

          then

          consider i be Nat such that

           A5: i in ( dom f1) and

           A6: not (v . (f1 /. i)) = 1 by A4, Th19;

          set j = ((f1 /. i) .. f);

          (f1 /. i) in ( rng f) by A5, PARTFUN2: 2, A1;

          then j in ( dom f) & (v . (f /. j)) = (v . (f1 /. i)) by FINSEQ_4: 20, FINSEQ_5: 38;

          hence contradiction by Th19, A4, A6;

        end;

          suppose

           A7: (v . kon(f)) = 0 ;

          assume

           A8: not (v . kon(f)) = (v . kon(f1));

          consider i be Nat such that

           A9: i in ( dom f) and

           A10: not (v . (f /. i)) = 1 by A7, Th19;

          set j = ((f /. i) .. f1);

          

           A11: (f /. i) in ( rng f1) by A9, PARTFUN2: 2, A1;

          then j in ( dom f1) by FINSEQ_4: 20;

          then (v . (f1 /. j)) = 1 by Th19, A8, A7, XBOOLEAN:def 3;

          hence contradiction by A10, FINSEQ_5: 38, A11;

        end;

      end;

    end;

    begin

    theorem :: LTLAXIO2:22

    

     Th22: (p => TVERUM ) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . (p => TVERUM )) = ((v . p) => (v . TVERUM )) by LTLAXIO1:def 15

      .= 1 by A1, Th4;

    end;

    theorem :: LTLAXIO2:23

    

     Th23: (( 'not' TVERUM ) => p) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

      thus (v . (( 'not' TVERUM ) => p)) = ((v . ( 'not' TVERUM )) => (v . p)) by LTLAXIO1:def 15

      .= (((v . TVERUM ) => (v . tf)) => (v . p)) by LTLAXIO1:def 15

      .= (( TRUE => (v . tf)) => (v . p)) by Th4

      .= 1 by A1;

    end;

    theorem :: LTLAXIO2:24

    

     Th24: (p => p) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . (p => p)) = ((v . p) => (v . p)) by LTLAXIO1:def 15

      .= 1 by A1;

    end;

    theorem :: LTLAXIO2:25

    

     Th25: (( 'not' ( 'not' p)) => p) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . (( 'not' ( 'not' p)) => p)) = ((v . ( 'not' ( 'not' p))) => (v . p)) by LTLAXIO1:def 15

      .= (((v . ( 'not' p)) => (v . tf)) => (v . p)) by LTLAXIO1:def 15

      .= ((((v . p) => (v . tf)) => (v . tf)) => (v . p)) by LTLAXIO1:def 15

      .= 1 by A1, LTLAXIO1:def 15;

    end;

    theorem :: LTLAXIO2:26

    

     Th26: (p => ( 'not' ( 'not' p))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . (p => ( 'not' ( 'not' p)))) = ((v . p) => (v . ( 'not' ( 'not' p)))) by LTLAXIO1:def 15

      .= ((v . p) => ((v . ( 'not' p)) => (v . tf))) by LTLAXIO1:def 15

      .= ((v . p) => (((v . p) => (v . tf)) => (v . tf))) by LTLAXIO1:def 15

      .= 1 by A2, A1;

    end;

    theorem :: LTLAXIO2:27

    ((p '&&' q) => p) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . ((p '&&' q) => p)) = ((v . (p '&&' q)) => (v . p)) by LTLAXIO1:def 15

      .= (((v . p) '&' (v . q)) => (v . p)) by LTLAXIO1: 31

      .= 1 by A1;

    end;

    theorem :: LTLAXIO2:28

    ((p '&&' q) => q) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

      thus (v . ((p '&&' q) => q)) = ((v . (p '&&' q)) => (v . q)) by LTLAXIO1:def 15

      .= (((v . p) '&' (v . q)) => (v . q)) by LTLAXIO1: 31

      .= 1 by A1;

    end;

    theorem :: LTLAXIO2:29

    for k be Nat st k in ( dom f) holds ((f /. k) => ( 'not' (( con ( nega f)) /. ( len ( con ( nega f)))))) is ctaut

    proof

      let k be Nat;

      assume

       A1: k in ( dom f);

      set q = (f /. k), p = (q => alt(f));

      assume not p is ctaut;

      then

      consider g such that

       A2: not (( VAL g) . p) = 1;

      set v = ( VAL g);

      (v . p) = 0 by A2, XBOOLEAN:def 3;

      then

       A3: ((v . q) => (v . alt(f))) = 0 by LTLAXIO1:def 15;

      (v . alt(f)) = TRUE or (v . alt(f)) = FALSE by XBOOLEAN:def 3;

      hence contradiction by A3, Th20, A1;

    end;

    theorem :: LTLAXIO2:30

    ( rng f) c= ( rng f1) implies (( 'not' (( con ( nega f)) /. ( len ( con ( nega f))))) => ( 'not' (( con ( nega f1)) /. ( len ( con ( nega f1)))))) is ctaut

    proof

      assume

       A1: ( rng f) c= ( rng f1);

      set p = ( alt(f) => alt(f1));

      assume not p is ctaut;

      then

      consider g such that

       A2: not (( VAL g) . p) = 1;

      set v = ( VAL g);

      (v . p) = 0 by A2, XBOOLEAN:def 3;

      then

       A3: ((v . alt(f)) => (v . alt(f1))) = 0 by LTLAXIO1:def 15;

      

       A4: (v . alt(f)) = TRUE or (v . alt(f)) = FALSE by XBOOLEAN:def 3;

      now

        let i be Nat;

        assume

         A5: i in ( dom f);

        then (f . i) in ( rng f) by FUNCT_1: 3;

        then

        consider j be object such that

         A6: j in ( dom f1) and

         A7: (f . i) = (f1 . j) by A1, FUNCT_1:def 3;

        (f1 /. j) = (f1 . j) by PARTFUN1:def 6, A6

        .= (f /. i) by A5, PARTFUN1:def 6, A7;

        hence (v . (f /. i)) = 0 by A6, Th20, A3, A4;

        reconsider j as Nat by A6;

      end;

      hence contradiction by A3, A4, Th20;

    end;

    theorem :: LTLAXIO2:31

    

     Th31: (( 'not' (p => q)) => p) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . (( 'not' (p => q)) => p)) = ((v . ( 'not' (p => q))) => (v . p)) by LTLAXIO1:def 15

      .= (((v . (p => q)) => (v . tf)) => (v . p)) by LTLAXIO1:def 15

      .= ((((v . p) => (v . q)) => (v . tf)) => (v . p)) by LTLAXIO1:def 15

      .= 1 by A1, LTLAXIO1:def 15;

    end;

    theorem :: LTLAXIO2:32

    

     Th32: (( 'not' (p => q)) => ( 'not' q)) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

      thus (v . (( 'not' (p => q)) => ( 'not' q))) = ((v . ( 'not' (p => q))) => (v . ( 'not' q))) by LTLAXIO1:def 15

      .= (((v . (p => q)) => (v . tf)) => (v . ( 'not' q))) by LTLAXIO1:def 15

      .= ((((v . p) => (v . q)) => (v . tf)) => (v . ( 'not' q))) by LTLAXIO1:def 15

      .= ((((v . p) => (v . q)) => (v . tf)) => ((v . q) => (v . tf))) by LTLAXIO1:def 15

      .= 1 by A2, A1;

    end;

    theorem :: LTLAXIO2:33

    (p => (q => p)) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

      thus (v . (p => (q => p))) = ((v . p) => (v . (q => p))) by LTLAXIO1:def 15

      .= ((v . p) => ((v . q) => (v . p))) by LTLAXIO1:def 15

      .= 1 by A1;

    end;

    theorem :: LTLAXIO2:34

    

     Th34: (p => (q => (p => q))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

      thus (v . (p => (q => (p => q)))) = ((v . p) => (v . (q => (p => q)))) by LTLAXIO1:def 15

      .= ((v . p) => ((v . q) => (v . (p => q)))) by LTLAXIO1:def 15

      .= ((v . p) => ((v . q) => ((v . p) => (v . q)))) by LTLAXIO1:def 15

      .= 1 by A1;

    end;

    theorem :: LTLAXIO2:35

    

     Th35: (( 'not' (p '&&' q)) => (( 'not' p) 'or' ( 'not' q))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ( 'not' (p '&&' q))) = ((v . (p '&&' q)) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . p) '&' (v . q)) => (v . tf)) by LTLAXIO1: 31;

      

       A4: (v . (( 'not' p) 'or' ( 'not' q))) = ((v . ( 'not' p)) 'or' (v . ( 'not' q))) by Th5

      .= (((v . p) => (v . tf)) 'or' (v . ( 'not' q))) by LTLAXIO1:def 15

      .= (((v . p) => (v . tf)) 'or' ((v . q) => (v . tf))) by LTLAXIO1:def 15;

      

       A5: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

      thus (v . (( 'not' (p '&&' q)) => (( 'not' p) 'or' ( 'not' q)))) = ((v . ( 'not' (p '&&' q))) => (v . (( 'not' p) 'or' ( 'not' q)))) by LTLAXIO1:def 15

      .= 1 by A2, A5, A1, A4, A3;

    end;

    theorem :: LTLAXIO2:36

    (( 'not' (p 'or' q)) => (( 'not' p) '&&' ( 'not' q))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . (( 'not' p) '&&' ( 'not' q))) = ((v . ( 'not' p)) '&' (v . ( 'not' q))) by LTLAXIO1: 31

      .= (((v . p) => (v . tf)) '&' (v . ( 'not' q))) by LTLAXIO1:def 15

      .= (((v . p) => (v . tf)) '&' ((v . q) => (v . tf))) by LTLAXIO1:def 15;

      

       A4: (v . ( 'not' (p 'or' q))) = ((v . (p 'or' q)) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . p) 'or' (v . q)) => (v . tf)) by Th5;

      

       A5: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

      thus (v . (( 'not' (p 'or' q)) => (( 'not' p) '&&' ( 'not' q)))) = ((v . ( 'not' (p 'or' q))) => (v . (( 'not' p) '&&' ( 'not' q)))) by LTLAXIO1:def 15

      .= 1 by A2, A5, A1, A3, A4;

    end;

    theorem :: LTLAXIO2:37

    (( 'not' (p '&&' q)) => (p => ( 'not' q))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . (p => ( 'not' q))) = ((v . p) => (v . ( 'not' q))) by LTLAXIO1:def 15

      .= ((v . p) => ((v . q) => (v . tf))) by LTLAXIO1:def 15;

      

       A4: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      (v . ( 'not' (p '&&' q))) = ((v . (p '&&' q)) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . p) '&' (v . q)) => (v . tf)) by LTLAXIO1: 31;

      

      hence (v . (( 'not' (p '&&' q)) => (p => ( 'not' q)))) = ((((v . p) '&' (v . q)) => (v . tf)) => ((v . p) => ((v . q) => (v . tf)))) by LTLAXIO1:def 15, A3

      .= 1 by A2, A4, A1;

    end;

    theorem :: LTLAXIO2:38

    (( 'not' ( TVERUM '&&' ( 'not' A))) => A) is ctaut

    proof

      let g;

      set v = ( VAL g), t = TVERUM ;

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . A) = 0 or (v . A) = 1 by XBOOLEAN:def 3;

      

      thus (v . (( 'not' (t '&&' ( 'not' A))) => A)) = ((v . ( 'not' (t '&&' ( 'not' A)))) => (v . A)) by LTLAXIO1:def 15

      .= (((v . (t '&&' ( 'not' A))) => (v . tf)) => (v . A)) by LTLAXIO1:def 15

      .= ((((v . t) '&' (v . ( 'not' A))) => (v . tf)) => (v . A)) by LTLAXIO1: 31

      .= ((((v . t) '&' ((v . A) => (v . tf))) => (v . tf)) => (v . A)) by LTLAXIO1:def 15

      .= 1 by A2, A1, Th4;

    end;

    theorem :: LTLAXIO2:39

    (( 'not' (s '&&' q)) => ((p => q) => (p => ( 'not' s)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ( 'not' (s '&&' q))) = ((v . (s '&&' q)) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . s) '&' (v . q)) => (v . tf)) by LTLAXIO1: 31;

      

       A4: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      

       A5: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      (v . ((p => q) => (p => ( 'not' s)))) = ((v . (p => q)) => (v . (p => ( 'not' s)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . q)) => (v . (p => ( 'not' s)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . q)) => ((v . p) => (v . ( 'not' s)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . q)) => ((v . p) => ((v . s) => (v . tf)))) by LTLAXIO1:def 15;

      

      hence (v . (( 'not' (s '&&' q)) => ((p => q) => (p => ( 'not' s))))) = ((((v . s) '&' (v . q)) => (v . tf)) => (((v . p) => (v . q)) => ((v . p) => ((v . s) => (v . tf))))) by LTLAXIO1:def 15, A3

      .= 1 by A2, A5, A4, A1;

    end;

    theorem :: LTLAXIO2:40

    

     Th40: ((p => r) => ((p => s) => (p => (r '&&' s)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((p => s) => (p => (r '&&' s)))) = ((v . (p => s)) => (v . (p => (r '&&' s)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . s)) => (v . (p => (r '&&' s)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . s)) => ((v . p) => (v . (r '&&' s)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . s)) => ((v . p) => ((v . r) '&' (v . s)))) by LTLAXIO1: 31;

      

       A4: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      (v . (p => r)) = ((v . p) => (v . r)) by LTLAXIO1:def 15;

      

      hence (v . ((p => r) => ((p => s) => (p => (r '&&' s))))) = (((v . p) => (v . r)) => (((v . p) => (v . s)) => ((v . p) => ((v . r) '&' (v . s))))) by LTLAXIO1:def 15, A3

      .= 1 by A1, A2, A4;

    end;

    theorem :: LTLAXIO2:41

    (( 'not' (p '&&' s)) => ( 'not' ((r '&&' s) '&&' (p '&&' q)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ( 'not' ((r '&&' s) '&&' (p '&&' q)))) = ((v . ((r '&&' s) '&&' (p '&&' q))) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . (r '&&' s)) '&' (v . (p '&&' q))) => (v . tf)) by LTLAXIO1: 31

      .= ((((v . r) '&' (v . s)) '&' (v . (p '&&' q))) => (v . tf)) by LTLAXIO1: 31

      .= ((((v . r) '&' (v . s)) '&' ((v . p) '&' (v . q))) => (v . tf)) by LTLAXIO1: 31;

      

       A4: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      (v . ( 'not' (p '&&' s))) = ((v . (p '&&' s)) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . p) '&' (v . s)) => (v . tf)) by LTLAXIO1: 31;

      

      hence (v . (( 'not' (p '&&' s)) => ( 'not' ((r '&&' s) '&&' (p '&&' q))))) = ((((v . p) '&' (v . s)) => (v . tf)) => ((((v . r) '&' (v . s)) '&' ((v . p) '&' (v . q))) => (v . tf))) by LTLAXIO1:def 15, A3

      .= 1 by A2, A4, A1;

    end;

    theorem :: LTLAXIO2:42

    (( 'not' (p '&&' s)) => ( 'not' ((p '&&' q) '&&' (r '&&' s)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ( 'not' ((p '&&' q) '&&' (r '&&' s)))) = ((v . ((p '&&' q) '&&' (r '&&' s))) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . (p '&&' q)) '&' (v . (r '&&' s))) => (v . tf)) by LTLAXIO1: 31

      .= ((((v . p) '&' (v . q)) '&' (v . (r '&&' s))) => (v . tf)) by LTLAXIO1: 31

      .= ((((v . p) '&' (v . q)) '&' ((v . r) '&' (v . s))) => (v . tf)) by LTLAXIO1: 31;

      

       A4: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      (v . ( 'not' (p '&&' s))) = ((v . (p '&&' s)) => (v . tf)) by LTLAXIO1:def 15

      .= (((v . p) '&' (v . s)) => (v . tf)) by LTLAXIO1: 31;

      

      hence (v . (( 'not' (p '&&' s)) => ( 'not' ((p '&&' q) '&&' (r '&&' s))))) = ((((v . p) '&' (v . s)) => (v . tf)) => ((((v . p) '&' (v . q)) '&' ((v . r) '&' (v . s))) => (v . tf))) by LTLAXIO1:def 15, A3

      .= 1 by A2, A4, A1;

    end;

    theorem :: LTLAXIO2:43

    

     Th43: ((p => (q '&&' ( 'not' q))) => ( 'not' p)) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

      thus (v . ((p => (q '&&' ( 'not' q))) => ( 'not' p))) = ((v . (p => (q '&&' ( 'not' q)))) => (v . ( 'not' p))) by LTLAXIO1:def 15

      .= (((v . p) => (v . (q '&&' ( 'not' q)))) => (v . ( 'not' p))) by LTLAXIO1:def 15

      .= (((v . p) => ((v . q) '&' (v . ( 'not' q)))) => (v . ( 'not' p))) by LTLAXIO1: 31

      .= (((v . p) => ((v . q) '&' ((v . q) => (v . tf)))) => (v . ( 'not' p))) by LTLAXIO1:def 15

      .= 1 by A2, A3, A1, LTLAXIO1:def 15;

    end;

    theorem :: LTLAXIO2:44

    

     Th44: ((q => (p '&&' r)) => ((p => s) => (q => (s '&&' r)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((p => s) => (q => (s '&&' r)))) = ((v . (p => s)) => (v . (q => (s '&&' r)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . s)) => (v . (q => (s '&&' r)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . s)) => ((v . q) => (v . (s '&&' r)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . s)) => ((v . q) => ((v . s) '&' (v . r)))) by LTLAXIO1: 31;

      

       A4: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

       A5: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      (v . (q => (p '&&' r))) = ((v . q) => (v . (p '&&' r))) by LTLAXIO1:def 15

      .= ((v . q) => ((v . p) '&' (v . r))) by LTLAXIO1: 31;

      

      hence (v . ((q => (p '&&' r)) => ((p => s) => (q => (s '&&' r))))) = (((v . q) => ((v . p) '&' (v . r))) => (((v . p) => (v . s)) => ((v . q) => ((v . s) '&' (v . r))))) by LTLAXIO1:def 15, A3

      .= 1 by A1, A2, A5, A4;

    end;

    theorem :: LTLAXIO2:45

    

     Th45: ((p => q) => ((r => s) => ((p '&&' r) => (q '&&' s)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((r => s) => ((p '&&' r) => (q '&&' s)))) = ((v . (r => s)) => (v . ((p '&&' r) => (q '&&' s)))) by LTLAXIO1:def 15

      .= (((v . r) => (v . s)) => (v . ((p '&&' r) => (q '&&' s)))) by LTLAXIO1:def 15

      .= (((v . r) => (v . s)) => ((v . (p '&&' r)) => (v . (q '&&' s)))) by LTLAXIO1:def 15

      .= (((v . r) => (v . s)) => (((v . p) '&' (v . r)) => (v . (q '&&' s)))) by LTLAXIO1: 31

      .= (((v . r) => (v . s)) => (((v . p) '&' (v . r)) => ((v . q) '&' (v . s)))) by LTLAXIO1: 31;

      

       A4: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

       A5: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      (v . (p => q)) = ((v . p) => (v . q)) by LTLAXIO1:def 15;

      

      hence (v . ((p => q) => ((r => s) => ((p '&&' r) => (q '&&' s))))) = (((v . p) => (v . q)) => (((v . r) => (v . s)) => (((v . p) '&' (v . r)) => ((v . q) '&' (v . s))))) by LTLAXIO1:def 15, A3

      .= 1 by A1, A2, A5, A4;

    end;

    theorem :: LTLAXIO2:46

    

     Th46: ((p => q) => ((p => r) => ((r => p) => (r => q)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((p => r) => ((r => p) => (r => q)))) = ((v . (p => r)) => (v . ((r => p) => (r => q)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . r)) => (v . ((r => p) => (r => q)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . r)) => ((v . (r => p)) => (v . (r => q)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . r)) => (((v . r) => (v . p)) => (v . (r => q)))) by LTLAXIO1:def 15

      .= (((v . p) => (v . r)) => (((v . r) => (v . p)) => ((v . r) => (v . q)))) by LTLAXIO1:def 15;

      

       A4: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      (v . (p => q)) = ((v . p) => (v . q)) by LTLAXIO1:def 15;

      

      hence (v . ((p => q) => ((p => r) => ((r => p) => (r => q))))) = (((v . p) => (v . q)) => (((v . p) => (v . r)) => (((v . r) => (v . p)) => ((v . r) => (v . q))))) by LTLAXIO1:def 15, A3

      .= 1 by A1, A2, A4;

    end;

    theorem :: LTLAXIO2:47

    

     Th47: ((p => q) => ((p => ( 'not' r)) => (p => ( 'not' (q => r))))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A2: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((p => ( 'not' r)) => (p => ( 'not' (q => r))))) = ((v . (p => ( 'not' r))) => (v . (p => ( 'not' (q => r))))) by LTLAXIO1:def 15

      .= (((v . p) => (v . ( 'not' r))) => (v . (p => ( 'not' (q => r))))) by LTLAXIO1:def 15

      .= (((v . p) => (v . ( 'not' r))) => ((v . p) => (v . ( 'not' (q => r))))) by LTLAXIO1:def 15

      .= (((v . p) => ((v . r) => (v . tf))) => ((v . p) => (v . ( 'not' (q => r))))) by LTLAXIO1:def 15

      .= (((v . p) => ((v . r) => (v . tf))) => ((v . p) => ((v . (q => r)) => (v . tf)))) by LTLAXIO1:def 15

      .= (((v . p) => ((v . r) => (v . tf))) => ((v . p) => (((v . q) => (v . r)) => (v . tf)))) by LTLAXIO1:def 15;

      

       A4: (v . tf) = 0 & (v . (p => q)) = ((v . p) => (v . q)) by LTLAXIO1:def 15;

      (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      hence (v . ((p => q) => ((p => ( 'not' r)) => (p => ( 'not' (q => r)))))) = 1 by A1, A2, A4, LTLAXIO1:def 15, A3;

    end;

    theorem :: LTLAXIO2:48

    

     Th48: ((p => (q 'or' r)) => ((r => s) => (p => (q 'or' s)))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

       A4: (v . ((r => s) => (p => (q 'or' s)))) = ((v . (r => s)) => (v . (p => (q 'or' s)))) by LTLAXIO1:def 15

      .= (((v . r) => (v . s)) => (v . (p => (q 'or' s)))) by LTLAXIO1:def 15

      .= (((v . r) => (v . s)) => ((v . p) => (v . (q 'or' s)))) by LTLAXIO1:def 15

      .= (((v . r) => (v . s)) => ((v . p) => ((v . q) 'or' (v . s)))) by Th5;

      

       A5: (v . s) = 1 or (v . s) = 0 by XBOOLEAN:def 3;

      (v . (p => (q 'or' r))) = ((v . p) => (v . (q 'or' r))) by LTLAXIO1:def 15

      .= ((v . p) => ((v . q) 'or' (v . r))) by Th5;

      

      hence (v . ((p => (q 'or' r)) => ((r => s) => (p => (q 'or' s))))) = (((v . p) => ((v . q) 'or' (v . r))) => (((v . r) => (v . s)) => ((v . p) => ((v . q) 'or' (v . s))))) by LTLAXIO1:def 15, A4

      .= 1 by A1, A2, A5, A3;

    end;

    theorem :: LTLAXIO2:49

    

     Th49: ((p => r) => ((q => r) => ((p 'or' q) => r))) is ctaut

    proof

      let g;

      set v = ( VAL g);

      

       A1: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . (p => r)) = ((v . p) => (v . r)) by LTLAXIO1:def 15;

      

       A4: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      (v . ((q => r) => ((p 'or' q) => r))) = ((v . (q => r)) => (v . ((p 'or' q) => r))) by LTLAXIO1:def 15

      .= (((v . q) => (v . r)) => (v . ((p 'or' q) => r))) by LTLAXIO1:def 15

      .= (((v . q) => (v . r)) => ((v . (p 'or' q)) => (v . r))) by LTLAXIO1:def 15

      .= (((v . q) => (v . r)) => (((v . p) 'or' (v . q)) => (v . r))) by Th5;

      

      hence (v . ((p => r) => ((q => r) => ((p 'or' q) => r)))) = (((v . p) => (v . r)) => (((v . q) => (v . r)) => (((v . p) 'or' (v . q)) => (v . r)))) by LTLAXIO1:def 15, A3

      .= 1 by A1, A2, A4;

    end;

    theorem :: LTLAXIO2:50

    ((r => ( untn (p,q))) => ((r => (( 'not' p) '&&' ( 'not' q))) => ( 'not' r))) is ctaut

    proof

      let g;

      set v = ( VAL g), pq = (p 'U' q), np = ( 'not' p), nq = ( 'not' q), nr = ( 'not' r);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . p) = 1 or (v . p) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((r => (np '&&' nq)) => nr)) = ((v . (r => (np '&&' nq))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (v . (np '&&' nq))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => ((v . np) '&' (v . nq))) => (v . nr)) by LTLAXIO1: 31

      .= (((v . r) => (((v . p) => (v . tf)) '&' (v . nq))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (((v . p) => (v . tf)) '&' ((v . q) => (v . tf)))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (((v . p) => (v . tf)) '&' ((v . q) => (v . tf)))) => ((v . r) => (v . tf))) by LTLAXIO1:def 15;

      

       A4: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      

       A5: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      (v . (r => ( untn (p,q)))) = ((v . r) => (v . ( untn (p,q)))) by LTLAXIO1:def 15

      .= ((v . r) => ((v . q) 'or' (v . (p '&&' pq)))) by Th5

      .= ((v . r) => ((v . q) 'or' ((v . p) '&' (v . pq)))) by LTLAXIO1: 31

      .= ((v . r) => ((v . q) 'or' ((v . p) '&' (g . pq)))) by LTLAXIO1:def 15;

      

      hence (v . ((r => ( untn (p,q))) => ((r => (np '&&' nq)) => nr))) = (((v . r) => ((v . q) 'or' ((v . p) '&' (g . pq)))) => (((v . r) => (((v . p) => (v . tf)) '&' ((v . q) => (v . tf)))) => ((v . r) => (v . tf)))) by LTLAXIO1:def 15, A3

      .= 1 by A2, A5, A4, A1;

    end;

    theorem :: LTLAXIO2:51

    ((r => ( untn (p,q))) => ((r => (( 'not' q) '&&' ( 'not' (p 'U' q)))) => ( 'not' r))) is ctaut

    proof

      let g;

      set v = ( VAL g), pq = (p 'U' q), nq = ( 'not' q), nr = ( 'not' r);

      

       A1: (v . tf) = 0 by LTLAXIO1:def 15;

      

       A2: (v . r) = 1 or (v . r) = 0 by XBOOLEAN:def 3;

      

       A3: (v . ((r => (nq '&&' ( 'not' pq))) => nr)) = ((v . (r => (nq '&&' ( 'not' pq)))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (v . (nq '&&' ( 'not' pq)))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => ((v . nq) '&' (v . ( 'not' pq)))) => (v . nr)) by LTLAXIO1: 31

      .= (((v . r) => (((v . q) => (v . tf)) '&' (v . ( 'not' pq)))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (((v . q) => (v . tf)) '&' ((v . pq) => (v . tf)))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (((v . q) => (v . tf)) '&' ((g . pq) => (v . tf)))) => (v . nr)) by LTLAXIO1:def 15

      .= (((v . r) => (((v . q) => (v . tf)) '&' ((g . pq) => (v . tf)))) => ((v . r) => (v . tf))) by LTLAXIO1:def 15;

      

       A4: (g . pq) = 1 or (g . pq) = 0 by XBOOLEAN:def 3;

      

       A5: (v . q) = 1 or (v . q) = 0 by XBOOLEAN:def 3;

      (v . (r => ( untn (p,q)))) = ((v . r) => (v . ( untn (p,q)))) by LTLAXIO1:def 15

      .= ((v . r) => ((v . q) 'or' (v . (p '&&' pq)))) by Th5

      .= ((v . r) => ((v . q) 'or' ((v . p) '&' (v . pq)))) by LTLAXIO1: 31

      .= ((v . r) => ((v . q) 'or' ((v . p) '&' (g . pq)))) by LTLAXIO1:def 15;

      

      hence (v . ((r => ( untn (p,q))) => ((r => (nq '&&' ( 'not' pq))) => nr))) = (((v . r) => ((v . q) 'or' ((v . p) '&' (g . pq)))) => (((v . r) => (((v . q) => (v . tf)) '&' ((g . pq) => (v . tf)))) => ((v . r) => (v . tf)))) by LTLAXIO1:def 15, A3

      .= 1 by A2, A5, A1, A4;

    end;

    begin

    theorem :: LTLAXIO2:52

    X |- (p => q) & X |- (p => r) implies X |- (p => (q '&&' r))

    proof

      assume that

       A1: X |- (p => q) and

       A2: X |- (p => r);

      set qr = (q '&&' r);

      ((p => q) => ((p => r) => (p => qr))) is ctaut by Th40;

      then ((p => q) => ((p => r) => (p => qr))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- ((p => q) => ((p => r) => (p => qr))) by LTLAXIO1: 42;

      then X |- ((p => r) => (p => qr)) by LTLAXIO1: 43, A1;

      hence X |- (p => qr) by LTLAXIO1: 43, A2;

    end;

    theorem :: LTLAXIO2:53

    

     Th53: X |- (p => q) & X |- (r => s) implies X |- ((p '&&' r) => (q '&&' s))

    proof

      assume that

       A1: X |- (p => q) and

       A2: X |- (r => s);

      ((p => q) => ((r => s) => ((p '&&' r) => (q '&&' s)))) is ctaut by Th45;

      then ((p => q) => ((r => s) => ((p '&&' r) => (q '&&' s)))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- ((p => q) => ((r => s) => ((p '&&' r) => (q '&&' s)))) by LTLAXIO1: 42;

      then X |- ((r => s) => ((p '&&' r) => (q '&&' s))) by LTLAXIO1: 43, A1;

      hence X |- ((p '&&' r) => (q '&&' s)) by LTLAXIO1: 43, A2;

    end;

    theorem :: LTLAXIO2:54

    

     Th54: X |- (p => q) & X |- (p => r) & X |- (r => p) implies X |- (r => q)

    proof

      assume that

       A1: X |- (p => q) and

       A2: X |- (p => r) and

       A3: X |- (r => p);

      ((p => q) => ((p => r) => ((r => p) => (r => q)))) is ctaut by Th46;

      then ((p => q) => ((p => r) => ((r => p) => (r => q)))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- ((p => q) => ((p => r) => ((r => p) => (r => q)))) by LTLAXIO1: 42;

      then X |- ((p => r) => ((r => p) => (r => q))) by LTLAXIO1: 43, A1;

      then X |- ((r => p) => (r => q)) by LTLAXIO1: 43, A2;

      hence thesis by LTLAXIO1: 43, A3;

    end;

    theorem :: LTLAXIO2:55

    X |- (p => (q '&&' ( 'not' q))) implies X |- ( 'not' p)

    proof

      ((p => (q '&&' ( 'not' q))) => ( 'not' p)) is ctaut by Th43;

      then ((p => (q '&&' ( 'not' q))) => ( 'not' p)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A1: X |- ((p => (q '&&' ( 'not' q))) => ( 'not' p)) by LTLAXIO1: 42;

      assume X |- (p => (q '&&' ( 'not' q)));

      hence X |- ( 'not' p) by A1, LTLAXIO1: 43;

    end;

    theorem :: LTLAXIO2:56

    (for i be Nat st i in ( dom f) holds ( {} LTLB_WFF ) |- (p => (f /. i))) implies ( {} LTLB_WFF ) |- (p => (( con f) /. ( len ( con f))))

    proof

      assume

       A1: for i be Nat st i in ( dom f) holds ( {} l) |- (p => (f /. i));

      per cases ;

        suppose

         A2: ( len f) = 0 ;

        (p => TVERUM ) is ctaut by Th22;

        then

         A3: (p => TVERUM ) in LTL_axioms by LTLAXIO1:def 17;

        f = {} by A2;

        hence thesis by A3, Th10, LTLAXIO1: 42;

      end;

        suppose

         A4: ( len f) > 0 ;

        defpred P3[ Nat] means $1 <= ( len f) implies ( {} l) |- (p => (( con f) /. $1));

         A5:

        now

          let k be non zero Nat such that

           A6: P3[k];

          thus P3[(k + 1)]

          proof

            set a = (( con f) /. k), b = (f /. (k + 1));

            assume

             A7: (k + 1) <= ( len f);

            1 <= k by NAT_1: 25;

            then

             A8: (( con f) /. (k + 1)) = ((( con f) /. k) '&&' (f /. (k + 1))) by A7, NAT_1: 13, Th7;

            1 <= (k + 1) by NAT_1: 25;

            then

             A9: ( {} l) |- (p => (f /. (k + 1))) by FINSEQ_3: 25, A7, A1;

            ((p => a) => ((p => b) => (p => (a '&&' b)))) is ctaut by Th40;

            then ((p => a) => ((p => b) => (p => (a '&&' b)))) in LTL_axioms by LTLAXIO1:def 17;

            then ( {} l) |- ((p => a) => ((p => b) => (p => (a '&&' b)))) by LTLAXIO1: 42;

            then ( {} l) |- ((p => b) => (p => (a '&&' b))) by LTLAXIO1: 43, A6, A7, NAT_1: 13;

            hence ( {} l) |- (p => (( con f) /. (k + 1))) by LTLAXIO1: 43, A9, A8;

          end;

        end;

        

         A10: P3[1]

        proof

          assume

           A11: 1 <= ( len f);

          then ( {} l) |- (p => (f /. 1)) by FINSEQ_3: 25, A1;

          hence thesis by A11, Th6;

        end;

        

         A12: for k be non zero Nat holds P3[k] from NAT_1:sch 10( A10, A5);

        ( len f) = ( len ( con f)) by A4, Def2;

        hence ( {} l) |- (p => kon(f)) by A12, A4;

      end;

    end;

    theorem :: LTLAXIO2:57

    (for i be Nat st i in ( dom f) holds ( {} LTLB_WFF ) |- ((f /. i) => p)) implies ( {} LTLB_WFF ) |- (( 'not' (( con ( nega f)) /. ( len ( con ( nega f))))) => p)

    proof

      set nt = ( 'not' TVERUM );

      assume

       A1: for i be Nat st i in ( dom f) holds ( {} l) |- ((f /. i) => p);

      per cases ;

        suppose

         A2: ( len f) = 0 ;

        (nt => p) is ctaut by Th23;

        then

         A3: (nt => p) in LTL_axioms by LTLAXIO1:def 17;

        ( len ( nega f)) = 0 by A2, Def4;

        then ( nega f) = {} ;

        hence thesis by A3, Th10, LTLAXIO1: 42;

      end;

        suppose

         A4: ( len f) > 0 ;

        defpred P3[ Nat] means $1 <= ( len f) implies ( {} l) |- (( 'not' (( con ( nega f)) /. $1)) => p);

         A5:

        now

          let k be non zero Nat such that

           A6: P3[k];

          thus P3[(k + 1)]

          proof

            set a = ( 'not' (( con ( nega f)) /. (k + 1))), b = (f /. (k + 1)), c = (( con ( nega f)) /. k), d = (( nega f) /. (k + 1)), nc = ( 'not' c), nd = ( 'not' d);

            ((a => (nc 'or' nd)) => ((nd => b) => (a => (nc 'or' b)))) is ctaut by Th48;

            then ((a => (nc 'or' nd)) => ((nd => b) => (a => (nc 'or' b)))) in LTL_axioms by LTLAXIO1:def 17;

            then

             A7: ( {} l) |- ((a => (nc 'or' nd)) => ((nd => b) => (a => (nc 'or' b)))) by LTLAXIO1: 42;

            assume

             A8: (k + 1) <= ( len f);

            then k < ( len f) by NAT_1: 13;

            then 1 <= k & k < ( len ( nega f)) by NAT_1: 25, Def4;

            then

             A9: a = ( 'not' (c '&&' d)) by Th7;

            ((nc => p) => ((b => p) => ((nc 'or' b) => p))) is ctaut by Th49;

            then ((nc => p) => ((b => p) => ((nc 'or' b) => p))) in LTL_axioms by LTLAXIO1:def 17;

            then ( {} l) |- ((nc => p) => ((b => p) => ((nc 'or' b) => p))) by LTLAXIO1: 42;

            then

             A10: ( {} l) |- ((b => p) => ((nc 'or' b) => p)) by LTLAXIO1: 43, A6, A8, NAT_1: 13;

            

             A11: 1 <= (k + 1) by NAT_1: 25;

            then ( {} l) |- (b => p) by FINSEQ_3: 25, A8, A1;

            then

             A12: ( {} l) |- ((nc 'or' b) => p) by A10, LTLAXIO1: 43;

            (k + 1) in ( dom f) by A11, FINSEQ_3: 25, A8;

            then nd = ( 'not' ( 'not' b)) by Th8;

            then (nd => b) is ctaut by Th25;

            then (nd => b) in LTL_axioms by LTLAXIO1:def 17;

            then

             A13: ( {} l) |- (nd => b) by LTLAXIO1: 42;

            (( 'not' (c '&&' d)) => (nc 'or' nd)) is ctaut by Th35;

            then (( 'not' (c '&&' d)) => (nc 'or' nd)) in LTL_axioms by LTLAXIO1:def 17;

            then ( {} l) |- (a => (nc 'or' nd)) by LTLAXIO1: 42, A9;

            then ( {} l) |- ((nd => b) => (a => (nc 'or' b))) by A7, LTLAXIO1: 43;

            then ( {} l) |- (a => (nc 'or' b)) by LTLAXIO1: 43, A13;

            hence ( {} l) |- (a => p) by A12, LTLAXIO1: 47;

          end;

        end;

        

         A14: ( len ( nega f)) > 0 by A4, Def4;

        

         A15: P3[1]

        proof

          set nnf = ( 'not' ( 'not' (f /. 1)));

          assume

           A16: 1 <= ( len f);

          then

           A17: 1 in ( dom f) by FINSEQ_3: 25;

          (nnf => (f /. 1)) is ctaut by Th25;

          then (nnf => (f /. 1)) in LTL_axioms by LTLAXIO1:def 17;

          then

           A18: ( {} l) |- (nnf => (f /. 1)) by LTLAXIO1: 42;

          

           A19: ( {} l) |- ((f /. 1) => p) by A16, FINSEQ_3: 25, A1;

          ( 'not' (( con ( nega f)) /. 1)) = ( 'not' (( nega f) /. 1)) by A14, Th6

          .= nnf by Th8, A17;

          hence thesis by A18, A19, LTLAXIO1: 47;

        end;

        

         A20: for k be non zero Nat holds P3[k] from NAT_1:sch 10( A15, A5);

        ( len f) = ( len ( nega f)) by Def4

        .= ( len ( con ( nega f))) by A14, Def2;

        hence ( {} l) |- ( alt(f) => p) by A20, A4;

      end;

    end;

    begin

    theorem :: LTLAXIO2:58

    

     Th58: X |- ((( 'X' p) => ( 'X' q)) => ( 'X' (p => q)))

    proof

      set pq = (p => q), npq = ( 'not' pq), nq = ( 'not' q), xnq = ( 'X' nq), xq = ( 'X' q), xnpq = ( 'X' npq), xpq = ( 'X' pq), nxpq = ( 'not' xpq), xp = ( 'X' p), nxq = ( 'not' xq);

      (nxpq => xnpq) in LTL_axioms by LTLAXIO1:def 17;

      then

       A1: X |- (nxpq => xnpq) by LTLAXIO1: 42;

      (npq => p) is ctaut by Th31;

      then (npq => p) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (npq => p) by LTLAXIO1: 42;

      then

       A2: X |- ( 'X' (npq => p)) by LTLAXIO1: 44;

      ((nxpq => xp) => ((nxpq => nxq) => (nxpq => ( 'not' (xp => xq))))) is ctaut by Th47;

      then ((nxpq => xp) => ((nxpq => nxq) => (nxpq => ( 'not' (xp => xq))))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A3: X |- ((nxpq => xp) => ((nxpq => nxq) => (nxpq => ( 'not' (xp => xq))))) by LTLAXIO1: 42;

      (xnq => nxq) in LTL_axioms by LTLAXIO1:def 17;

      then

       A4: X |- (xnq => nxq) by LTLAXIO1: 42;

      (npq => nq) is ctaut by Th32;

      then (npq => nq) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (npq => nq) by LTLAXIO1: 42;

      then

       A5: X |- ( 'X' (npq => nq)) by LTLAXIO1: 44;

      (xnpq => nxpq) in LTL_axioms by LTLAXIO1:def 17;

      then

       A6: X |- (xnpq => nxpq) by LTLAXIO1: 42;

      (( 'X' (npq => nq)) => (( 'X' npq) => xnq)) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'X' (npq => nq)) => (xnpq => xnq)) by LTLAXIO1: 42;

      then X |- (xnpq => xnq) by LTLAXIO1: 43, A5;

      then X |- (nxpq => xnq) by A1, A6, Th54;

      then

       A7: X |- (nxpq => nxq) by A4, LTLAXIO1: 47;

      (( 'X' (npq => p)) => (xnpq => xp)) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'X' (npq => p)) => (xnpq => xp)) by LTLAXIO1: 42;

      then X |- (xnpq => xp) by A2, LTLAXIO1: 43;

      then X |- (nxpq => xp) by A6, Th54, A1;

      then X |- ((nxpq => nxq) => (nxpq => ( 'not' (xp => xq)))) by A3, LTLAXIO1: 43;

      then X |- (nxpq => ( 'not' (xp => xq))) by LTLAXIO1: 43, A7;

      then

       A8: X |- (( 'not' ( 'not' (xp => xq))) => ( 'not' nxpq)) by LTLAXIO1: 52;

      ((xp => xq) => ( 'not' ( 'not' (xp => xq)))) is ctaut by Th26;

      then ((xp => xq) => ( 'not' ( 'not' (xp => xq)))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A9: X |- ((xp => xq) => ( 'not' ( 'not' (xp => xq)))) by LTLAXIO1: 42;

      (( 'not' ( 'not' (xp => xq))) => (xp => xq)) is ctaut by Th25;

      then (( 'not' ( 'not' (xp => xq))) => (xp => xq)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A10: X |- (( 'not' ( 'not' (xp => xq))) => (xp => xq)) by LTLAXIO1: 42;

      (( 'not' nxpq) => xpq) is ctaut by Th25;

      then (( 'not' nxpq) => xpq) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'not' nxpq) => xpq) by LTLAXIO1: 42;

      then X |- (( 'not' ( 'not' (xp => xq))) => xpq) by LTLAXIO1: 47, A8;

      hence thesis by A9, A10, Th54;

    end;

    theorem :: LTLAXIO2:59

    

     Th59: X |- (( 'X' (p '&&' q)) => (( 'X' p) '&&' ( 'X' q)))

    proof

      set xp = ( 'X' p), xq = ( 'X' q), np = ( 'not' p), nq = ( 'not' q), xnp = ( 'X' ( 'not' p)), xnq = ( 'X' ( 'not' q)), nxp = ( 'not' ( 'X' p)), nxq = ( 'not' ( 'X' q)), npq = (np '&&' nq);

      

       A1: X |- ((xp => xnq) => ( 'X' (p => nq))) by Th58;

      ((xp => nxq) => (xp => nxq)) is ctaut by Th24;

      then ((xp => nxq) => (xp => nxq)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A2: X |- ((xp => nxq) => (xp => nxq)) by LTLAXIO1: 42;

      (nxq => xnq) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (nxq => xnq) by LTLAXIO1: 42;

      then X |- ((xp => nxq) => (xp => xnq)) by A2, LTLAXIO1: 51;

      then

       A3: X |- ((xp => nxq) => ( 'X' (p => nq))) by A1, LTLAXIO1: 47;

      (( 'X' ( 'not' (p => nq))) => ( 'not' ( 'X' (p => nq)))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'X' ( 'not' (p => nq))) => ( 'not' ( 'X' (p => nq)))) by LTLAXIO1: 42;

      then

       A4: X |- (( 'not' ( 'not' ( 'X' (p => nq)))) => ( 'not' ( 'X' ( 'not' (p => nq))))) by LTLAXIO1: 52;

      (( 'X' ( 'not' (p => nq))) => ( 'not' ( 'not' ( 'X' ( 'not' (p => nq)))))) is ctaut by Th26;

      then (( 'X' ( 'not' (p => nq))) => ( 'not' ( 'not' ( 'X' ( 'not' (p => nq)))))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A5: X |- (( 'X' ( 'not' (p => nq))) => ( 'not' ( 'not' ( 'X' ( 'not' (p => nq)))))) by LTLAXIO1: 42;

      (( 'X' (p => nq)) => ( 'not' ( 'not' ( 'X' (p => nq))))) is ctaut by Th26;

      then (( 'X' (p => nq)) => ( 'not' ( 'not' ( 'X' (p => nq))))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'X' (p => nq)) => ( 'not' ( 'not' ( 'X' (p => nq))))) by LTLAXIO1: 42;

      then X |- ((xp => nxq) => ( 'not' ( 'not' ( 'X' (p => nq))))) by A3, LTLAXIO1: 47;

      then X |- ((xp => nxq) => ( 'not' ( 'X' ( 'not' (p => nq))))) by A4, LTLAXIO1: 47;

      then X |- (( 'not' ( 'not' ( 'X' ( 'not' (p => nq))))) => ( 'not' (xp => nxq))) by LTLAXIO1: 52;

      hence thesis by A5, LTLAXIO1: 47;

    end;

    theorem :: LTLAXIO2:60

    ( {} LTLB_WFF ) |- ((( con ( nex f)) /. ( len ( con ( nex f)))) => ( 'X' (( con f) /. ( len ( con f)))))

    proof

      set t = TVERUM ;

      per cases ;

        suppose

         A1: ( len f) = 0 ;

        then ( len ( nex f)) = 0 by Def5;

        then

         A2: ( nex f) = {} ;

        t is ctaut by Th4;

        then t in LTL_axioms by LTLAXIO1:def 17;

        then

         A3: ( {} l) |- t by LTLAXIO1: 42;

        then

         A4: ( {} l) |- ( 'X' t) by LTLAXIO1: 44;

        (t => (( 'X' t) => (t => ( 'X' t)))) is ctaut by Th34;

        then (t => (( 'X' t) => (t => ( 'X' t)))) in LTL_axioms by LTLAXIO1:def 17;

        then ( {} l) |- (t => (( 'X' t) => (t => ( 'X' t)))) by LTLAXIO1: 42;

        then

         A5: ( {} l) |- (( 'X' t) => (t => ( 'X' t))) by LTLAXIO1: 43, A3;

        f = {} by A1;

        hence thesis by A5, LTLAXIO1: 43, A4, Th10, A2;

      end;

        suppose

         A6: 0 < ( len f);

        defpred P[ Nat] means $1 <= ( len f) implies ( {} l) |- ((( con ( nex f)) /. $1) => ( 'X' (( con f) /. $1)));

         A7:

        now

          let k be non zero Nat;

          set p = (( con ( nex f)) /. k), q = (( con ( nex f)) /. (k + 1)), r = (( nex f) /. (k + 1)), s = (( con f) /. (k + 1)), t = (( con f) /. k);

          assume

           A8: P[k];

          thus P[(k + 1)]

          proof

            ((q => (p '&&' r)) => ((p => ( 'X' t)) => (q => (( 'X' t) '&&' r)))) is ctaut by Th44;

            then ((q => (p '&&' r)) => ((p => ( 'X' t)) => (q => (( 'X' t) '&&' r)))) in LTL_axioms by LTLAXIO1:def 17;

            then

             A9: ( {} l) |- ((q => (p '&&' r)) => ((p => ( 'X' t)) => (q => (( 'X' t) '&&' r)))) by LTLAXIO1: 42;

            reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

            

             A10: 1 <= k1 by NAT_1: 25;

            assume

             A11: (k + 1) <= ( len f);

            then

             A12: (k1 + 1) <= ( len ( con f)) by Def2;

            

             A13: (k1 + 1) <= ( len ( nex f)) by A11, Def5;

            

            then r = (( nex f) . (k1 + 1)) by NAT_1: 12, FINSEQ_4: 15

            .= ( 'X' (f /. (k + 1))) by Def5, NAT_1: 12, A11;

            then

             A14: ( {} l) |- ((( 'X' t) '&&' r) => ( 'X' (t '&&' (f /. (k + 1))))) by LTLAXIO1: 53;

            

             A15: k < ( len f) by A11, NAT_1: 13;

            then

             A16: k1 < ( len ( nex f)) by Def5;

            (k1 + 1) <= ( len ( con ( nex f))) by A13, Def2;

            

            then q = (( con ( nex f)) . (k1 + 1)) by NAT_1: 12, FINSEQ_4: 15

            .= (p '&&' r) by Def2, A16, A10;

            then (q => (p '&&' r)) is ctaut by Th24;

            then (q => (p '&&' r)) in LTL_axioms by LTLAXIO1:def 17;

            then ( {} l) |- (q => (p '&&' r)) by LTLAXIO1: 42;

            then ( {} l) |- ((p => ( 'X' t)) => (q => (( 'X' t) '&&' r))) by A9, LTLAXIO1: 43;

            then

             A17: ( {} l) |- (q => (( 'X' t) '&&' r)) by LTLAXIO1: 43, A11, NAT_1: 13, A8;

            (t '&&' (f /. (k + 1))) = (( con f) . (k1 + 1)) by Def2, A10, A15

            .= s by NAT_1: 12, A12, FINSEQ_4: 15;

            hence ( {} l) |- (q => ( 'X' s)) by A14, A17, LTLAXIO1: 47;

          end;

        end;

        

         A18: 0 < ( len ( nex f)) by A6, Def5;

        

         A19: P[1]

        proof

          assume

           A20: 1 <= ( len f);

          then 1 <= ( len ( nex f)) by Def5;

          then 1 <= ( len ( con ( nex f))) by Def2;

          

          then

           A21: (( con ( nex f)) /. 1) = (( con ( nex f)) . 1) by FINSEQ_4: 15

          .= (( nex f) . 1) by Def2, A18

          .= ( 'X' (f /. 1)) by Def5, A20;

          (( 'X' (f /. 1)) => ( 'X' (f /. 1))) is ctaut by Th24;

          then

           A22: (( 'X' (f /. 1)) => ( 'X' (f /. 1))) in LTL_axioms by LTLAXIO1:def 17;

          ( 'X' (( con f) /. 1)) = ( 'X' (f /. 1)) by Th6, A20;

          hence thesis by A22, LTLAXIO1: 42, A21;

        end;

        for k be non zero Nat holds P[k] from NAT_1:sch 10( A19, A7);

        then

         A23: ( {} l) |- ((( con ( nex f)) /. ( len f)) => ( 'X' (( con f) /. ( len f)))) by A6;

        

         A24: ( len ( nex f)) > 0 by A6, Def5;

        ( len f) = ( len ( nex f)) by Def5

        .= ( len ( con ( nex f))) by Def2, A24;

        hence thesis by Def2, A6, A23;

      end;

    end;

    theorem :: LTLAXIO2:61

    X |- ((( 'X' p) 'or' ( 'X' q)) => ( 'X' (p 'or' q)))

    proof

      set xp = ( 'X' p), xq = ( 'X' q), np = ( 'not' p), nq = ( 'not' q), xnp = ( 'X' ( 'not' p)), xnq = ( 'X' ( 'not' q)), nxp = ( 'not' ( 'X' p)), nxq = ( 'not' ( 'X' q)), npq = (np '&&' nq);

      (( 'not' ( 'X' ( 'not' npq))) => ( 'X' ( 'not' ( 'not' npq)))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A1: X |- (( 'not' ( 'X' ( 'not' npq))) => ( 'X' ( 'not' ( 'not' npq)))) by LTLAXIO1: 42;

      (( 'not' ( 'not' npq)) => npq) is ctaut by Th25;

      then (( 'not' ( 'not' npq)) => npq) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'not' ( 'not' npq)) => npq) by LTLAXIO1: 42;

      then

       A2: X |- ( 'X' (( 'not' ( 'not' npq)) => npq)) by LTLAXIO1: 44;

      (( 'X' (( 'not' ( 'not' npq)) => npq)) => (( 'X' ( 'not' ( 'not' npq))) => ( 'X' npq))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'X' (( 'not' ( 'not' npq)) => npq)) => (( 'X' ( 'not' ( 'not' npq))) => ( 'X' npq))) by LTLAXIO1: 42;

      then X |- (( 'X' ( 'not' ( 'not' npq))) => ( 'X' npq)) by LTLAXIO1: 43, A2;

      then

       A3: X |- (( 'not' ( 'X' ( 'not' npq))) => ( 'X' npq)) by LTLAXIO1: 47, A1;

      X |- (( 'X' npq) => (xnp '&&' xnq)) by Th59;

      then

       A4: X |- (( 'not' ( 'X' ( 'not' npq))) => (xnp '&&' xnq)) by LTLAXIO1: 47, A3;

      (xnq => nxq) in LTL_axioms by LTLAXIO1:def 17;

      then

       A5: X |- (xnq => nxq) by LTLAXIO1: 42;

      (( 'not' ( 'not' ( 'X' ( 'not' npq)))) => ( 'X' ( 'not' npq))) is ctaut by Th25;

      then (( 'not' ( 'not' ( 'X' ( 'not' npq)))) => ( 'X' ( 'not' npq))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A6: X |- (( 'not' ( 'not' ( 'X' ( 'not' npq)))) => ( 'X' ( 'not' npq))) by LTLAXIO1: 42;

      (xnp => nxp) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (xnp => nxp) by LTLAXIO1: 42;

      then X |- ((xnp '&&' xnq) => (nxp '&&' nxq)) by A5, Th53;

      then X |- (( 'not' ( 'X' ( 'not' npq))) => (nxp '&&' nxq)) by LTLAXIO1: 47, A4;

      then X |- (( 'not' (nxp '&&' nxq)) => ( 'not' ( 'not' ( 'X' ( 'not' npq))))) by LTLAXIO1: 52;

      hence thesis by A6, LTLAXIO1: 47;

    end;

    theorem :: LTLAXIO2:62

    

     Th62: X |- (( 'X' (p 'or' q)) => (( 'X' p) 'or' ( 'X' q)))

    proof

      set xp = ( 'X' p), xq = ( 'X' q), np = ( 'not' p), nq = ( 'not' q), xnp = ( 'X' ( 'not' p)), xnq = ( 'X' ( 'not' q)), nxp = ( 'not' ( 'X' p)), nxq = ( 'not' ( 'X' q));

      X |- ((xnp '&&' xnq) => ( 'X' (np '&&' nq))) by LTLAXIO1: 53;

      then

       A1: X |- (( 'not' ( 'X' (np '&&' nq))) => ( 'not' (xnp '&&' xnq))) by LTLAXIO1: 52;

      (nxq => xnq) in LTL_axioms by LTLAXIO1:def 17;

      then

       A2: X |- (nxq => xnq) by LTLAXIO1: 42;

      (nxp => xnp) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (nxp => xnp) by LTLAXIO1: 42;

      then X |- ((nxp '&&' nxq) => (xnp '&&' xnq)) by A2, Th53;

      then

       A3: X |- (( 'not' (xnp '&&' xnq)) => ( 'not' (nxp '&&' nxq))) by LTLAXIO1: 52;

      (( 'X' (p 'or' q)) => ( 'not' ( 'X' (np '&&' nq)))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'X' (p 'or' q)) => ( 'not' ( 'X' (np '&&' nq)))) by LTLAXIO1: 42;

      then X |- (( 'X' (p 'or' q)) => ( 'not' (xnp '&&' xnq))) by A1, LTLAXIO1: 47;

      hence thesis by A3, LTLAXIO1: 47;

    end;

    theorem :: LTLAXIO2:63

    X |- (( 'not' (A 'U' B)) => ( 'X' ( 'not' ( untn (A,B)))))

    proof

      set p = (A 'U' B), q = ( 'X' B), r = ( 'X' (A '&&' (A 'U' B)));

      ((q 'or' r) => p) in LTL_axioms by LTLAXIO1:def 17;

      then

       A1: X |- ((q 'or' r) => p) by LTLAXIO1: 42;

      X |- (( 'X' ( untn (A,B))) => (q 'or' r)) by Th62;

      then X |- (( 'X' ( untn (A,B))) => p) by LTLAXIO1: 47, A1;

      then

       A2: X |- (( 'not' p) => ( 'not' ( 'X' ( untn (A,B))))) by LTLAXIO1: 52;

      (( 'not' ( 'X' ( untn (A,B)))) => ( 'X' ( 'not' ( untn (A,B))))) in LTL_axioms by LTLAXIO1:def 17;

      then X |- (( 'not' ( 'X' ( untn (A,B)))) => ( 'X' ( 'not' ( untn (A,B))))) by LTLAXIO1: 42;

      hence thesis by LTLAXIO1: 47, A2;

    end;