ltlaxio4.miz



    begin

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

M for LTLModel,

j,k,n for Element of NAT ,

i for Nat,

X for Subset of LTLB_WFF ,

F for finite Subset of LTLB_WFF ,

f for FinSequence of LTLB_WFF ,

g for Function of LTLB_WFF , BOOLEAN ,

x,y,z for set,

P,Q,R for PNPair;

    set l = LTLB_WFF , pairs = [:(l ** ), (l ** ):];

    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 X be finite set;

      :: original: Enumeration

      redefine

      mode Enumeration of X -> one-to-one FinSequence of X ;

      coherence

      proof

        let E be Enumeration of X;

        ( rng E) = X by RLAFFIN3:def 1;

        hence E is one-to-one FinSequence of X by FINSEQ_1:def 4;

      end;

    end

    definition

      let E be set, F be finite Subset of E;

      :: original: Enumeration

      redefine

      mode Enumeration of F -> one-to-one FinSequence of E ;

      coherence

      proof

        let f be Enumeration of F;

        ( rng f) = F by RLAFFIN3:def 1;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    registration

      let D be set;

      cluster non empty finite for FinSequenceSet of D;

      existence

      proof

         {( <*> D)} is FinSequenceSet of D

        proof

          let a be object;

          thus a in {( <*> D)} implies a is FinSequence of D by TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: LTLAXIO4:1

    

     Th1: for X be set, G be non empty finite FinSequenceSet of X holds ex A be FinSequence st A in G & for B be FinSequence st B in G holds ( len B) <= ( len A)

    proof

      let X be set, G be non empty finite FinSequenceSet of X;

      set g = the Enumeration of G;

      deffunc F1( Nat) = ( len (g /. $1));

      consider f be FinSequence of NAT such that

       A1: ( len f) = ( len g) & for n be Nat st n in ( dom f) holds (f . n) = F1(n) from FINSEQ_2:sch 1;

      ( rng f) c= REAL by NUMBERS: 19;

      then

      reconsider f1 = f as FinSequence of REAL by FINSEQ_1:def 4;

      set m = ( max_p f1), A = (g /. m);

      

       A2: g <> {} by RLAFFIN3:def 1, RELAT_1: 38;

      for B be FinSequence st B in G holds ( len B) <= ( len A)

      proof

        let B be FinSequence;

        set m1 = (B .. g);

        m in ( dom f) by A2, A1, RFINSEQ2:def 1;

        then

         A3: ( len A) = (f1 . m) by A1;

        assume B in G;

        then

         A4: B in ( rng g) by RLAFFIN3:def 1;

        then

         A5: m1 in ( dom g) by FINSEQ_4: 20;

        then

         A6: m1 in ( dom f) by A1, FINSEQ_3: 29;

        (g /. m1) = (g . m1) by A5, PARTFUN1:def 6

        .= B by FINSEQ_4: 19, A4;

        then ( len B) = (f1 . m1) by A6, A1;

        hence ( len B) <= ( len A) by A6, RFINSEQ2:def 1, A2, A1, A3;

      end;

      hence thesis;

    end;

    definition

      let T be DecoratedTree;

      let n;

      let t be Node of T;

      :: original: |

      redefine

      func t | n -> Node of T ;

      correctness

      proof

        set tn = (t | n);

        ex p be FinSequence st t = (tn ^ p) by FINSEQ_1: 80;

        hence tn is Node of T by TREES_1: 21;

      end;

    end

    theorem :: LTLAXIO4:2

    

     Th2: p is FinSequence of NAT

    proof

      l c= ( NAT * ) by HILBERT1:def 5;

      then p in ( NAT * );

      hence thesis by FINSEQ_1:def 11;

    end;

    notation

      let A;

      synonym A is s-until for A is conjunctive;

    end

    definition

      let A;

      assume

       A1: A is s-until;

      :: LTLAXIO4:def1

      func rarg A -> Element of LTLB_WFF means

      : Def1: ex p st (p 'U' it ) = A;

      existence

      proof

        ex p, q st (p 'U' q) = A by A1, HILBERT2:def 6;

        hence thesis;

      end;

      uniqueness by HILBERT2: 19;

    end

    definition

      let A;

      :: LTLAXIO4:def2

      attr A is satisfiable means ex M, n st (( SAT M) . [n, A]) = 1;

    end

    theorem :: LTLAXIO4:3

    

     Th3: ( {} LTLB_WFF ) |= A iff not ( 'not' A) is satisfiable

    proof

      hereby

        assume

         A1: ( {} l) |= A;

        assume ( 'not' A) is satisfiable;

        then

        consider M, n such that

         A2: (( SAT M) . [n, ( 'not' A)]) = 1;

        

         A3: M |= ( {} l);

        (( SAT M) . [n, A]) = 0 by A2, LTLAXIO1: 5;

        hence contradiction by A3, A1, LTLAXIO1:def 12;

      end;

      assume

       A4: not ( 'not' A) is satisfiable;

      assume not ( {} l) |= A;

      then

      consider M such that M |= ( {} l) and

       A5: not M |= A;

      consider n such that

       A6: not (( SAT M) . [n, A]) = 1 by A5;

      (( SAT M) . [n, ( 'not' A)]) = 1 by A6, XBOOLEAN:def 3, LTLAXIO1: 5;

      hence contradiction by A4;

    end;

    theorem :: LTLAXIO4:4

    

     Th4: ( TVERUM '&&' A) is satisfiable implies A is satisfiable

    proof

      assume ( TVERUM '&&' A) is satisfiable;

      then

      consider M, n such that

       A1: (( SAT M) . [n, ( TVERUM '&&' A)]) = 1;

      (( SAT M) . [n, A]) = 1 by LTLAXIO1: 7, A1;

      hence A is satisfiable;

    end;

    theorem :: LTLAXIO4:5

    

     Th5: for i be Element of NAT holds (( SAT M) . [i, (p 'U' q)]) = 1 iff ex j st j > i & (( SAT M) . [j, q]) = 1 & for k st i < k & k < j holds (( SAT M) . [k, p]) = 1

    proof

      let i be Element of NAT ;

      set s = ( SAT M);

      hereby

        assume (s . [i, (p 'U' q)]) = 1;

        then

        consider j be Element of NAT such that

         A1: 0 < j & (s . [(i + j), q]) = 1 and

         A2: for k st 1 <= k & k < j holds (s . [(i + k), p]) = 1 by LTLAXIO1:def 11;

        set m = (i + j);

        now

          let k;

          assume that

           A3: i < k and

           A4: k < m;

          reconsider k1 = (k - i) as Element of NAT by A3, NAT_1: 21;

          (i + ( - i)) < (k + ( - i)) by A3, XREAL_1: 8;

          then

           A5: 1 <= k1 by NAT_1: 25;

          (k + ( - i)) < (m + ( - i)) by A4, XREAL_1: 8;

          then (s . [(i + k1), p]) = 1 by A5, A2;

          hence (s . [k, p]) = 1;

        end;

        hence ex j st j > i & (s . [j, q]) = 1 & for k st i < k & k < j holds (s . [k, p]) = 1 by A1, NAT_1: 16;

      end;

      given j such that

       A6: j > i and

       A7: (s . [j, q]) = 1 and

       A8: for k st i < k & k < j holds (s . [k, p]) = 1;

      reconsider n = (j - i) as Element of NAT by A6, NAT_1: 21;

       A9:

      now

        let k;

        assume 1 <= k & k < n;

        then (k + i) < (n + i) & i < (i + k) by XREAL_1: 8, NAT_1: 16;

        hence (s . [(i + k), p]) = 1 by A8;

      end;

      (j + ( - i)) > (i + ( - i)) & (s . [(i + n), q]) = 1 by A6, XREAL_1: 8, A7;

      hence (s . [i, (p 'U' q)]) = 1 by A9, LTLAXIO1:def 11;

    end;

    theorem :: LTLAXIO4:6

    

     Th6: (( SAT M) . [n, (( con f) /. ( len ( con f)))]) = 1 iff for i st i in ( dom f) holds (( SAT M) . [n, (f /. i)]) = 1

    proof

      set s = ( SAT M);

      defpred P[ Nat] means for f st ( len f) = $1 holds (s . [n, kon(f)]) = 1 iff (for i st i in ( dom f) holds (s . [n, (f /. i)]) = 1);

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        thus P[(k + 1)]

        proof

          let f;

          

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

          set fk = (f | k);

          assume

           A4: ( len f) = (k + 1);

          

           A5: ( dom fk) c= ( dom f) by RELAT_1: 60;

          per cases ;

            suppose

             A6: k > 0 ;

            then

             A7: 1 <= k by NAT_1: 25;

            

             A8: kon(f) = (( con f) /. (k + 1)) by LTLAXIO2:def 2, A4

            .= ((( con f) /. k) '&&' (f /. (k + 1))) by LTLAXIO2: 7, A7, NAT_1: 16, A4;

            

             A9: k < ( len f) by NAT_1: 16, A4;

            then

             A10: ( len fk) = k by FINSEQ_1: 59;

            

             A11: (( con f) /. k) = (( con (f | k)) /. k) by A7, A9, LTLAXIO2: 13

            .= kon(fk) by A10, LTLAXIO2:def 2, A6;

            hereby

              assume

               A12: (s . [n, kon(f)]) = 1;

              then

               A13: (s . [n, kon(fk)]) = 1 by A8, LTLAXIO1: 7, A11;

              let i;

              assume

               A14: i in ( dom f);

              then

               A15: 1 <= i by FINSEQ_3: 25;

              

               A16: i <= ( len f) by A14, FINSEQ_3: 25;

              per cases by A16, XXREAL_0: 1;

                suppose i < ( len f);

                then i <= k by A4, NAT_1: 13;

                then

                 A17: i in ( dom fk) by A10, FINSEQ_3: 25, A15;

                then (s . [n, (fk /. i)]) = 1 by A2, A10, A13;

                hence (s . [n, (f /. i)]) = 1 by FINSEQ_4: 70, A17;

              end;

                suppose i = ( len f);

                hence (s . [n, (f /. i)]) = 1 by A4, A12, A8, LTLAXIO1: 7;

              end;

            end;

            assume

             A18: for i st i in ( dom f) holds (s . [n, (f /. i)]) = 1;

            now

              let i;

              assume

               A19: i in ( dom fk);

              then (s . [n, (f /. i)]) = 1 by A5, A18;

              hence (s . [n, (fk /. i)]) = 1 by FINSEQ_4: 70, A19;

            end;

            then

             A20: (s . [n, (( con f) /. k)]) = 1 by A2, A10, A11;

            (s . [n, (f /. (k + 1))]) = 1 by A18, FINSEQ_3: 25, A4, A3;

            hence (s . [n, kon(f)]) = 1 by LTLAXIO1: 7, A20, A8;

          end;

            suppose

             A21: k = 0 ;

            

            then

             A22: kon(f) = (( con f) /. 1) by A4, LTLAXIO2:def 2

            .= (f /. 1) by LTLAXIO2: 6, A4;

            hereby

              assume

               A23: (s . [n, kon(f)]) = 1;

              let i;

              assume i in ( dom f);

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

              hence (s . [n, (f /. i)]) = 1 by NAT_1: 25, A21, A4, A23, A22;

            end;

            assume for i st i in ( dom f) holds (s . [n, (f /. i)]) = 1;

            hence (s . [n, kon(f)]) = 1 by A21, A4, FINSEQ_3: 25, A22;

          end;

        end;

      end;

      

       A24: P[ 0 ]

      proof

        let f;

        assume ( len f) = 0 ;

        then f = {} ;

        hence thesis by LTLAXIO1: 6, LTLAXIO2: 10;

      end;

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

      then P[( len f)];

      hence thesis;

    end;

    theorem :: LTLAXIO4:7

    

     Th7: ( [( <*> LTLB_WFF ), <*A*>] ^ ) = ( TVERUM '&&' ( 'not' A))

    proof

      ( nega <*A*>) = <*( 'not' A)*> & ( [( <*> l), <*A*>] `1 ) = ( <*> l) by LTLAXIO2: 14;

      hence thesis by LTLAXIO2: 10, LTLAXIO2: 11;

    end;

    theorem :: LTLAXIO4:8

    

     Th8: for P be complete PNPair st ( untn (A,B)) in ( rng P) holds A in ( rng P) & B in ( rng P) & (A 'U' B) in ( rng P)

    proof

      let P be complete PNPair;

      assume

       A1: ( untn (A,B)) in ( rng P);

      ( tau ( rng P)) = ( rng P) by LTLAXIO3:def 11;

      hence A in ( rng P) & B in ( rng P) & (A 'U' B) in ( rng P) by A1, LTLAXIO3: 22;

    end;

    theorem :: LTLAXIO4:9

    

     Th9: ( rng P) c= ( union ( Subt ( rng P)))

    proof

      let x be object;

      assume

       A1: x in ( rng P);

      then

      reconsider x1 = x as Element of l;

      

       A2: x in ( tau1 . x1) & ( tau1 . x1) c= ( Sub . x1) by LTLAXIO3: 6, LTLAXIO3: 25;

      ( Sub . x1) in ( Subt ( rng P)) by A1;

      hence thesis by A2, TARSKI:def 4;

    end;

    begin

    definition

      let F be Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):];

      :: LTLAXIO4:def3

      func F ^ -> Subset of LTLB_WFF equals { (P ^ ) where P be Element of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] : P in F };

      coherence

      proof

        set b = { (P ^ ) where P be Element of [:(l ** ), (l ** ):] : P in F };

        b c= l

        proof

          let x be object;

          assume x in b;

          then ex P be PNPair st x = (P ^ ) & P in F;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let F be non empty Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):];

      cluster (F ^ ) -> non empty;

      coherence

      proof

        consider x be object such that

         A1: x in F by XBOOLE_0:def 1;

        reconsider x1 = x as PNPair by A1;

        (x1 ^ ) in (F ^ ) by A1;

        hence thesis;

      end;

    end

    registration

      let F be finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):];

      cluster (F ^ ) -> finite;

      coherence

      proof

        set f = the Enumeration of F;

        deffunc d( Nat) = ((f /. $1) ^ );

        consider g be FinSequence of l such that

         A1: ( len g) = ( len f) & for j be Nat st j in ( dom g) holds (g . j) = d(j) from FINSEQ_2:sch 1;

        (F ^ ) c= ( rng g)

        proof

          let x be object;

          assume x in (F ^ );

          then

          consider P such that

           A2: (P ^ ) = x and

           A3: P in F;

          

           A4: P in ( rng f) by RLAFFIN3:def 1, A3;

          then

           A5: (P .. f) in ( dom f) by FINSEQ_4: 20;

          

          then

           A6: (f /. (P .. f)) = (f . (P .. f)) by PARTFUN1:def 6

          .= P by FINSEQ_4: 19, A4;

          

           A7: (P .. f) in ( dom g) by A5, A1, FINSEQ_3: 29;

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

          hence thesis by A1, A7, A6, A2;

        end;

        hence (F ^ ) is finite;

      end;

    end

    theorem :: LTLAXIO4:10

    

     Th10: for F,G be Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] holds ((F \/ G) ^ ) = ((F ^ ) \/ (G ^ ))

    proof

      let F,G be Subset of [:(l ** ), (l ** ):];

      hereby

        let x be object;

        assume x in ((F \/ G) ^ );

        then

        consider P such that

         A1: x = (P ^ ) and

         A2: P in (F \/ G);

        P in F or P in G by A2, XBOOLE_0:def 3;

        then x in (F ^ ) or x in (G ^ ) by A1;

        hence x in ((F ^ ) \/ (G ^ )) by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A3: x in ((F ^ ) \/ (G ^ ));

      per cases by A3, XBOOLE_0:def 3;

        suppose x in (F ^ );

        then

        consider P such that

         A4: x = (P ^ ) and

         A5: P in F;

        P in (F \/ G) by A5, XBOOLE_0:def 3;

        hence x in ((F \/ G) ^ ) by A4;

      end;

        suppose x in (G ^ );

        then

        consider P such that

         A6: x = (P ^ ) and

         A7: P in G;

        P in (F \/ G) by A7, XBOOLE_0:def 3;

        hence x in ((F \/ G) ^ ) by A6;

      end;

    end;

    theorem :: LTLAXIO4:11

    

     Th11: ( { [( <*> LTLB_WFF ), ( <*> LTLB_WFF )]} ^ ) = {( TVERUM '&&' TVERUM )}

    proof

      set Q = [( <*> l), ( <*> l)], t = TVERUM ;

      hereby

        let x be object;

        assume x in ( {Q} ^ );

        then

        consider P such that

         A1: x = (P ^ ) and

         A2: P in {Q};

        (P ^ ) = (t '&&' t) by A2, TARSKI:def 1, LTLAXIO3: 27;

        hence x in {(t '&&' t)} by A1, TARSKI:def 1;

      end;

      let x be object;

      assume x in {(t '&&' t)};

      then

       A3: x = (t '&&' t) by TARSKI:def 1;

      Q in {Q} by TARSKI:def 1;

      hence x in ( {Q} ^ ) by LTLAXIO3: 27, A3;

    end;

    definition

      let F be finite Subset of LTLB_WFF ;

      :: LTLAXIO4:def4

      func comp F -> non empty finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] equals { Q where Q be PNPair : ( rng Q) = ( tau F) & ( rng (Q `1 )) misses ( rng (Q `2 )) };

      coherence

      proof

        set c = { Q where Q be PNPair : ( rng Q) = ( tau F) & ( rng (Q `1 )) misses ( rng (Q `2 )) }, tf = ( tau F), f = the Enumeration of tf, x = [f, ( <*> l)];

        

         A1: c c= [:(tf ** ), (tf ** ):]

        proof

          let x be object;

          assume x in c;

          then

          consider Q such that

           A2: x = Q and

           A3: ( rng Q) = ( tau F) and ( rng (Q `1 )) misses ( rng (Q `2 ));

          consider y,z be object such that

           A4: y in (l ** ) & z in (l ** ) and

           A5: Q = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as one-to-one FinSequence of l by A4, LTLAXIO3:def 2;

          ( rng y) = ( rng (Q `1 )) by A5;

          then

          reconsider y as one-to-one FinSequence of tf by XBOOLE_1: 7, A3, FINSEQ_1:def 4;

          ( rng z) = ( rng (Q `2 )) by A5;

          then

          reconsider z as one-to-one FinSequence of tf by XBOOLE_1: 7, A3, FINSEQ_1:def 4;

          y in (tf ** ) & z in (tf ** ) by LTLAXIO3:def 2;

          hence thesis by ZFMISC_1:def 2, A5, A2;

        end;

        ( rng (x `2 )) = {} ;

        then

         A6: ( rng (x `1 )) misses ( rng (x `2 ));

        ( rng x) = (tf \/ ( rng ( <*> l))) by RLAFFIN3:def 1

        .= tf;

        then x in c by A6;

        hence c is non empty finite Subset of [:(l ** ), (l ** ):] by A1, XBOOLE_1: 1;

      end;

    end

    registration

      let F be finite Subset of LTLB_WFF ;

      cluster -> complete for Element of ( comp F);

      coherence

      proof

        let x be Element of ( comp F);

        x in ( comp F);

        then ex Q st Q = x & ( rng Q) = ( tau F) & ( rng (Q `1 )) misses ( rng (Q `2 ));

        then ( tau ( rng x)) = ( rng x) by LTLAXIO3: 17;

        hence x is complete;

      end;

    end

    theorem :: LTLAXIO4:12

    

     Th12: ( comp ( {} LTLB_WFF )) = { [( <*> LTLB_WFF ), ( <*> LTLB_WFF )]}

    proof

      hereby

        let x be object;

        assume x in ( comp ( {} l));

        then

        consider Q such that

         A1: Q = x and

         A2: ( rng Q) = ( tau ( {} l)) and ( rng (Q `1 )) misses ( rng (Q `2 ));

        ( rng (Q `1 )) = ( {} l) by A2;

        then

         A3: (Q `1 ) = ( <*> l) by RELAT_1: 41;

        ( rng (Q `2 )) = ( {} l) by A2;

        then

         A4: (Q `2 ) = ( <*> l) by RELAT_1: 41;

        ex z,y be object st z in (l ** ) & y in (l ** ) & Q = [z, y] by ZFMISC_1:def 2;

        then x = [( <*> l), ( <*> l)] by A1, A3, A4;

        hence x in { [( <*> l), ( <*> l)]} by TARSKI:def 1;

      end;

      let x be object;

      set Q = [( <*> l), ( <*> l)];

      assume x in {Q};

      then

       A5: x = Q by TARSKI:def 1;

      

       A6: ( rng (Q `1 )) misses ( rng (Q `2 ));

      ( rng Q) = ( tau ( {} l));

      hence x in ( comp ( {} l)) by A6, A5;

    end;

    definition

      let P, Q;

      :: LTLAXIO4:def5

      pred Q is_completion_of P means ( rng (P `1 )) c= ( rng (Q `1 )) & ( rng (P `2 )) c= ( rng (Q `2 )) & ( tau ( rng P)) = ( rng Q);

    end

    theorem :: LTLAXIO4:13

    

     Th13: Q is_completion_of P implies Q is complete by LTLAXIO3: 17;

    definition

      let P;

      :: LTLAXIO4:def6

      func comp P -> finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] equals { Q where Q be consistent PNPair : Q is_completion_of P };

      coherence

      proof

        set c = { Q where Q be consistent PNPair : Q is_completion_of P }, F = ( tau ( rng P));

        

         A1: c c= [:(F ** ), (F ** ):]

        proof

          let x be object;

          assume x in c;

          then

          consider Q be consistent PNPair such that

           A2: x = Q and

           A3: Q is_completion_of P;

          consider y,z be object such that

           A4: y in (l ** ) & z in (l ** ) and

           A5: Q = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as one-to-one FinSequence of l by A4, LTLAXIO3:def 2;

          

           A6: F = ( rng Q) by A3

          .= (( rng y) \/ ( rng z)) by A5;

          then z is one-to-one FinSequence of F by XBOOLE_1: 7, FINSEQ_1:def 4;

          then

           A7: z in (F ** ) by LTLAXIO3:def 2;

          y is one-to-one FinSequence of F by A6, XBOOLE_1: 7, FINSEQ_1:def 4;

          then y in (F ** ) by LTLAXIO3:def 2;

          hence x in [:(F ** ), (F ** ):] by A7, ZFMISC_1:def 2, A5, A2;

        end;

        c c= [:(l ** ), (l ** ):]

        proof

          let x be object;

          assume x in c;

          then ex Q be consistent PNPair st x = Q & Q is_completion_of P;

          hence x in [:(l ** ), (l ** ):];

        end;

        hence thesis by A1;

      end;

    end

    registration

      let P be consistent PNPair;

      cluster ( comp P) -> non empty;

      coherence

      proof

        consider Q be consistent PNPair such that

         A1: ( rng (P `1 )) c= ( rng (Q `1 )) & ( rng (P `2 )) c= ( rng (Q `2 )) & ( tau ( rng P)) = ( rng Q) by LTLAXIO3: 34;

        Q is_completion_of P by A1;

        then Q in { R where R be consistent PNPair : R is_completion_of P };

        hence thesis;

      end;

    end

    registration

      let P be consistent PNPair;

      cluster -> consistent for Element of ( comp P);

      coherence

      proof

        let x be Element of ( comp P);

        x in ( comp P);

        then ex Q be consistent PNPair st x = Q & Q is_completion_of P;

        hence x is consistent;

      end;

    end

    definition

      let X be Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):];

      :: LTLAXIO4:def7

      func comp X -> Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] equals ( union { ( comp P) where P be Element of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] : P in X });

      coherence

      proof

        set a = { ( comp P) where P be Element of pairs : P in X };

        a c= ( bool pairs)

        proof

          let x be object;

          assume x in a;

          then ex P st x = ( comp P) & P in X;

          hence thesis;

        end;

        then

        reconsider a1 = a as Subset-Family of pairs;

        ( union a1) is Subset of pairs;

        hence ( union a) is Subset of pairs;

      end;

    end

    registration

      let X be finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):];

      cluster ( comp X) -> finite;

      coherence

      proof

        deffunc F( PNPair) = ( comp $1);

        set a = { F(P) where P be Element of pairs : P in X };

        

         A1: a is finite-membered

        proof

          let x;

          assume x in a;

          then ex P st x = F(P) & P in X;

          hence x is finite;

        end;

        

         A2: a c= ( bool pairs)

        proof

          let x be object;

          assume x in a;

          then ex P st x = ( comp P) & P in X;

          hence thesis;

        end;

        

         A3: X is finite;

        a is finite from FRAENKEL:sch 21( A3);

        then

        reconsider a1 = a as finite finite-membered Subset-Family of pairs by A2, A1;

        ( union a1) is finite;

        hence thesis;

      end;

    end

    theorem :: LTLAXIO4:14

    

     Th14: for X be non empty Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] st Q in X holds ( comp Q) c= ( comp X)

    proof

      let X be non empty Subset of pairs;

      assume Q in X;

      then

       A1: ( comp Q) in { ( comp T) where T be PNPair : T in X };

      let x be object;

      assume x in ( comp Q);

      hence thesis by A1, TARSKI:def 4;

    end;

    theorem :: LTLAXIO4:15

    

     Th15: for F be non empty finite Subset of LTLB_WFF holds ex p st p in ( tau F) & ( tau (( tau F) \ {p})) = (( tau F) \ {p})

    proof

      let F be non empty finite Subset of l;

      set G = { A where A be Element of l : A in ( tau F) & A is conditional };

      

       A1: G c= ( tau F)

      proof

        let x be object;

        assume x in G;

        then ex A st A = x & A in ( tau F) & A is conditional;

        hence thesis;

      end;

      

       A2: G is FinSequenceSet of NAT

      proof

        let x be object;

        assume x in G;

        then ex A st A = x & A in ( tau F) & A is conditional;

        hence thesis by Th2;

      end;

      per cases ;

        suppose

         A3: G = {} ;

        

         A4: F is without_implication

        proof

          assume not F is without_implication;

          then

          consider p such that

           A5: p in F & p is conditional;

          F c= ( tau F) by LTLAXIO3: 16;

          then p in G by A5;

          hence contradiction by A3;

        end;

        consider p be object such that

         A6: p in F by XBOOLE_0:def 1;

        reconsider p as Element of l by A6;

        set Fp = (( tau F) \ {p});

        Fp c= ( tau F) by XBOOLE_1: 36;

        then

         A7: Fp c= F by LTLAXIO3: 18, A4;

        

         A8: ( tau Fp) c= Fp

        proof

          let x be object;

          assume x in ( tau Fp);

          then

          consider A such that

           A9: A in Fp and

           A10: x in ( tau1 . A) by LTLAXIO3:def 5;

          x in {A} by A7, A9, A4, A10, LTLAXIO3: 5;

          hence thesis by TARSKI:def 1, A9;

        end;

        Fp c= ( tau Fp) & p in ( tau F) by LTLAXIO3: 16, A4, A6, LTLAXIO3: 18;

        hence thesis by A8, XBOOLE_0:def 10;

      end;

        suppose G <> {} ;

        then

        reconsider G as non empty finite FinSequenceSet of NAT by A2, A1;

        consider A be FinSequence such that

         A11: A in G and

         A12: for B be FinSequence st B in G holds ( len B) <= ( len A) by Th1;

        set Fp = (( tau F) \ {A});

        

         A13: Fp c= ( tau F) by XBOOLE_1: 36;

        

         A14: ( tau Fp) c= Fp

        proof

          let x be object;

          assume x in ( tau Fp);

          then

          consider p such that

           A15: p in Fp and

           A16: x in ( tau1 . p) by LTLAXIO3:def 5;

          

           A17: not p in {A} by XBOOLE_0:def 5, A15;

          then

           A18: p <> A by TARSKI:def 1;

          x <> A

          proof

            per cases ;

              suppose p is conditional;

              then p in G by A15, A13;

              then

               A19: ( len A) >= ( len p) by A12;

              per cases ;

                suppose x = p;

                hence thesis by A17, TARSKI:def 1;

              end;

                suppose x <> p;

                hence thesis by LTLAXIO3: 11, A16, A19;

              end;

            end;

              suppose not p is conditional;

              then x in {p} by LTLAXIO3: 5, A16;

              hence thesis by TARSKI:def 1, A18;

            end;

          end;

          then

           A20: not x in {A} by TARSKI:def 1;

          ( tau1 . p) c= ( tau F) by LTLAXIO3: 23, A15, A13;

          hence thesis by A20, XBOOLE_0:def 5, A16;

          reconsider x1 = x as Element of l by A16;

        end;

        Fp c= ( tau Fp) & ex q st q = A & q in ( tau F) & q is conditional by LTLAXIO3: 16, A11;

        hence thesis by A14, XBOOLE_0:def 10;

      end;

    end;

    theorem :: LTLAXIO4:16

    

     Th16: for F be finite Subset of LTLB_WFF , f be FinSequence of LTLB_WFF st ( rng f) = (( comp F) ^ ) holds ( {} LTLB_WFF ) |- ( 'not' (( con ( nega f)) /. ( len ( con ( nega f)))))

    proof

      let F be finite Subset of l, f be FinSequence of l;

      defpred P[ Nat] means for F be finite Subset of l st ( card ( tau F)) = $1 holds (for f be FinSequence of l st ( rng f) = (( comp F) ^ ) holds ( {} l) |- alt(f));

      assume

       A1: ( rng f) = (( comp F) ^ );

      

       A2: ( card ( tau F)) = ( card ( tau F));

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        thus P[(k + 1)]

        proof

          let G be finite Subset of l;

          assume

           A5: ( card ( tau G)) = (k + 1);

          then

          reconsider H = G as non empty finite Subset of l;

          let g be FinSequence of l;

          consider A such that

           A6: A in ( tau H) and

           A7: ( tau (( tau H) \ {A})) = (( tau H) \ {A}) by Th15;

          set Fp = (( tau H) \ {A});

          consider ff be FinSequence such that

           A8: ( rng ff) = ( comp Fp) and ff is one-to-one by FINSEQ_4: 58;

          reconsider ff as FinSequence of [:(l ** ), (l ** ):] by A8, FINSEQ_1:def 4;

          deffunc form1( Nat) = ( [(((ff /. $1) `1 ) ^^ <*A*>), ((ff /. $1) `2 )] ^ );

          deffunc form2( Nat) = ( [((ff /. $1) `1 ), (((ff /. $1) `2 ) ^^ <*A*>)] ^ );

          consider ff1 be FinSequence of l such that

           A9: ( len ff1) = ( len ff) & for i be Nat st i in ( dom ff1) holds (ff1 /. i) = form1(i) from FINSEQ_4:sch 2;

          consider ff2 be FinSequence of l such that

           A10: ( len ff2) = ( len ff) & for i be Nat st i in ( dom ff2) holds (ff2 /. i) = form2(i) from FINSEQ_4:sch 2;

          set fl = (ff1 ^ ff2);

           A11:

          now

            let i be Nat;

            set Q = (ff /. i);

            assume i in ( dom ff1) or i in ( dom ff2);

            then i in ( dom ff) by A9, A10, FINSEQ_3: 29;

            then Q in ( comp Fp) by PARTFUN2: 2, A8;

            then ex R st R = Q & ( rng R) = ( tau Fp) & ( rng (R `1 )) misses ( rng (R `2 ));

            hence ( rng Q) = ( tau Fp) & ( rng (Q `1 )) misses ( rng (Q `2 ));

          end;

          ( tau Fp) misses {A} by XBOOLE_1: 79, A7;

          then

           A12: ( tau Fp) misses ( rng <*A*>) by FINSEQ_1: 38;

           A13:

          now

            let i be Nat;

            set Q = (ff /. i);

            assume i in ( dom ff1);

            then

             A14: ( rng Q) misses ( rng <*A*>) by A12, A11;

            hence ( rng (Q `1 )) misses ( rng <*A*>) by XBOOLE_1: 7, XBOOLE_1: 63;

            thus ( rng (Q `2 )) misses ( rng <*A*>) by XBOOLE_1: 7, A14, XBOOLE_1: 63;

          end;

           A15:

          now

            let i be Nat;

            set Q = (ff /. i);

            assume i in ( dom ff2);

            then

             A16: ( rng Q) misses ( rng <*A*>) by A12, A11;

            hence ( rng (Q `2 )) misses ( rng <*A*>) by XBOOLE_1: 7, XBOOLE_1: 63;

            thus ( rng (Q `1 )) misses ( rng <*A*>) by XBOOLE_1: 7, A16, XBOOLE_1: 63;

          end;

          

           A17: ( rng fl) c= (( comp G) ^ )

          proof

            let x be object;

            assume x in ( rng fl);

            then

             A18: x in (( rng ff1) \/ ( rng ff2)) by FINSEQ_1: 31;

            per cases by A18, XBOOLE_0:def 3;

              suppose

               A19: x in ( rng ff1);

              set i = (x .. ff1), Q = (ff /. i), P1 = [((Q `1 ) ^^ <*A*>), (Q `2 )];

              

               A20: i in ( dom ff1) by A19, FINSEQ_4: 20;

              then

               A21: ( rng (Q `1 )) misses ( rng <*A*>) by A13;

              ( rng (Q `2 )) misses ( rng <*A*>) by A13, A20;

              then

               A22: ( rng (P1 `2 )) misses {A} by FINSEQ_1: 38;

              

               A23: ( rng (P1 `1 )) = ( rng ((Q `1 ) ^ <*A*>)) by LTLAXIO3:def 3, A21

              .= (( rng (Q `1 )) \/ ( rng <*A*>)) by FINSEQ_1: 31

              .= (( rng (Q `1 )) \/ {A}) by FINSEQ_1: 38;

              ( rng (Q `1 )) misses ( rng (Q `2 )) by A11, A20;

              then

               A24: ( rng (P1 `1 )) misses ( rng (P1 `2 )) by XBOOLE_1: 70, A22, A23;

              ( rng P1) = ( {A} \/ ( rng Q)) by XBOOLE_1: 4, A23

              .= ( {A} \/ ( tau Fp)) by A11, A20

              .= ( tau G) by XBOOLE_1: 45, ZFMISC_1: 31, A6, A7;

              then

               A25: P1 in ( comp G) by A24;

              x = (ff1 /. i) by FINSEQ_5: 38, A19

              .= (P1 ^ ) by A9, A19, FINSEQ_4: 20;

              hence x in (( comp G) ^ ) by A25;

            end;

              suppose

               A26: x in ( rng ff2);

              set i = (x .. ff2), Q = (ff /. i), P1 = [(Q `1 ), ((Q `2 ) ^^ <*A*>)];

              

               A27: i in ( dom ff2) by A26, FINSEQ_4: 20;

              then

               A28: ( rng (Q `2 )) misses ( rng <*A*>) by A15;

              ( rng (Q `1 )) misses ( rng <*A*>) by A15, A27;

              then

               A29: ( rng (P1 `1 )) misses {A} by FINSEQ_1: 38;

              

               A30: ( rng (P1 `2 )) = ( rng ((Q `2 ) ^ <*A*>)) by LTLAXIO3:def 3, A28

              .= (( rng (Q `2 )) \/ ( rng <*A*>)) by FINSEQ_1: 31

              .= (( rng (Q `2 )) \/ {A}) by FINSEQ_1: 38;

              ( rng (Q `2 )) misses ( rng (Q `1 )) by A11, A27;

              then

               A31: ( rng (P1 `1 )) misses ( rng (P1 `2 )) by XBOOLE_1: 70, A29, A30;

              ( rng P1) = ( {A} \/ ( rng Q)) by XBOOLE_1: 4, A30

              .= ( {A} \/ ( tau Fp)) by A11, A27

              .= ( tau G) by XBOOLE_1: 45, ZFMISC_1: 31, A6, A7;

              then

               A32: P1 in ( comp G) by A31;

              x = (ff2 /. i) by FINSEQ_5: 38, A26

              .= (P1 ^ ) by A10, A26, FINSEQ_4: 20;

              hence x in (( comp G) ^ ) by A32;

            end;

          end;

          assume

           A33: ( rng g) = (( comp G) ^ );

          ( alt(fl) => alt(g)) is ctaut

          proof

            let h be Function of l, BOOLEAN ;

            set v = ( VAL h);

            

             A34: (v . alt(g)) = 1 or (v . alt(g)) = 0 by XBOOLEAN:def 3;

             A35:

            now

              assume that

               A36: (v . alt(fl)) = 1 and

               A37: (v . alt(g)) = 0 ;

              per cases ;

                suppose ( len fl) = 0 ;

                then ( len ( nega fl)) = 0 by LTLAXIO2:def 4;

                then ( con ( nega fl)) = <* TVERUM *> by LTLAXIO2:def 2;

                

                then alt(fl) = ( 'not' ( <* TVERUM *> /. 1)) by FINSEQ_1: 39

                .= ( 'not' TVERUM ) by FINSEQ_4: 16;

                

                then (v . alt(fl)) = ((v . TVERUM ) => (v . TFALSUM )) by LTLAXIO1:def 15

                .= ( TRUE => (v . TFALSUM )) by LTLAXIO2: 4;

                hence contradiction by A36, LTLAXIO1:def 15;

              end;

                suppose ( len fl) > 0 ;

                ((v . kon(nega)) => (v . TFALSUM )) = 1 by A36, LTLAXIO1:def 15;

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

                then

                consider i be Nat such that

                 A38: i in ( dom ( nega fl)) and

                 A39: not (v . (( nega fl) /. i)) = 1 by LTLAXIO2: 19;

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

                ( len fl) = ( len ( nega fl)) by LTLAXIO2:def 4;

                then

                 A40: i1 in ( dom fl) by FINSEQ_3: 29, A38;

                then

                 A41: not (v . ( 'not' (fl /. i1))) = 1 by LTLAXIO2: 8, A39;

                set j = ((fl /. i1) .. g);

                ((v . kon(nega)) => (v . TFALSUM )) = 0 by A37, LTLAXIO1:def 15;

                then

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

                

                 A43: (fl /. i1) in ( rng fl) by PARTFUN2: 2, A40;

                then

                 A44: j in ( dom g) by A17, A33, FINSEQ_4: 20;

                then j <= ( len g) by FINSEQ_3: 25;

                then

                 A45: j <= ( len ( nega g)) by LTLAXIO2:def 4;

                1 <= j by A44, FINSEQ_3: 25;

                then

                 A46: j in ( dom ( nega g)) by A45, FINSEQ_3: 25;

                (( nega g) /. j) = ( 'not' (g /. j)) by LTLAXIO2: 8, A44

                .= ( 'not' (fl /. i1)) by FINSEQ_5: 38, A43, A17, A33;

                hence contradiction by A42, A46, LTLAXIO2: 19, A41;

              end;

            end;

            

            thus (v . ( alt(fl) => alt(g))) = ((v . alt(fl)) => (v . alt(g))) by LTLAXIO1:def 15

            .= 1 by A35, A34, XBOOLEAN:def 3;

          end;

          then ( alt(fl) => alt(g)) in LTL_axioms by LTLAXIO1:def 17;

          then

           A47: ( {} l) |- ( alt(fl) => alt(g)) by LTLAXIO1: 42;

          deffunc dash( Nat) = ((ff /. $1) ^ );

          consider fk be FinSequence of l such that

           A48: ( len fk) = ( len ff) & for i be Nat st i in ( dom fk) holds (fk /. i) = dash(i) from FINSEQ_4:sch 2;

           A49:

          now

            let g;

            set v = ( VAL g);

            assume (v . alt(fk)) = 1;

            then ((v . kon(nega)) => (v . TFALSUM )) = 1 by LTLAXIO1:def 15;

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

            then

            consider i be Nat such that

             A50: i in ( dom ( nega fk)) and

             A51: not (v . (( nega fk) /. i)) = 1 by LTLAXIO2: 19;

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

            

             A52: 1 <= i1 by FINSEQ_3: 25, A50;

            i1 <= ( len ( nega fk)) by FINSEQ_3: 25, A50;

            then

             A53: i1 <= ( len fk) by LTLAXIO2:def 4;

            (( nega fk) /. i) = (( nega fk) . i1) by A50, PARTFUN1:def 6

            .= ( 'not' (fk /. i1)) by LTLAXIO2:def 4, A53, A52;

            

            then

             A54: (v . (( nega fk) /. i)) = ((v . (fk /. i1)) => (v . TFALSUM )) by LTLAXIO1:def 15

            .= ((v . (fk /. i1)) => FALSE ) by LTLAXIO1:def 15;

            

             A55: (v . (fk /. i1)) = (v . ((ff /. i1) ^ )) by A53, FINSEQ_3: 25, A52, A48

            .= ((v . kon(`1)) '&' (v . kon(nega))) by LTLAXIO1: 31;

            now

              ( dom ( nega ff1)) c= ( dom (( nega ff1) ^ ( nega ff2))) by FINSEQ_1: 26;

              then

               A56: ( dom ( nega ff1)) c= ( dom ( nega fl)) by LTLAXIO2: 16;

              assume (v . alt(fl)) = 0 ;

              then ((v . kon(nega)) => (v . TFALSUM )) = 0 by LTLAXIO1:def 15;

              then

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

              per cases by XBOOLEAN:def 3;

                suppose

                 A58: (v . A) = 1;

                i1 <= ( len ( nega ff1)) by A9, A48, A53, LTLAXIO2:def 4;

                then

                 A59: i in ( dom ( nega ff1)) by A52, FINSEQ_3: 25;

                set a = (((ff /. i1) `1 ) ^^ <*A*>), b = ((ff /. i1) `2 );

                i1 in ( dom ff1) by A52, A9, A48, A53, FINSEQ_3: 25;

                then ( rng ((ff /. i1) `1 )) misses ( rng <*A*>) by A13;

                then

                 A60: a = (((ff /. i1) `1 ) ^ <*A*>) by LTLAXIO3:def 3;

                

                 A61: (( nega fl) /. i1) = ((( nega ff1) ^ ( nega ff2)) /. i) by LTLAXIO2: 16

                .= (( nega ff1) /. i) by FINSEQ_4: 68, A59

                .= (( nega ff1) . i1) by PARTFUN1:def 6, A59

                .= ( 'not' (ff1 /. i1)) by LTLAXIO2:def 4, A52, A9, A48, A53;

                

                 A62: 1 = (v . (( nega fl) /. i1)) by A57, A59, A56, LTLAXIO2: 19

                .= ((v . (ff1 /. i1)) => (v . TFALSUM )) by LTLAXIO1:def 15, A61

                .= ((v . (ff1 /. i1)) => FALSE ) by LTLAXIO1:def 15;

                (v . (ff1 /. i1)) = (v . ( [a, b] ^ )) by A9, A52, A48, A53, FINSEQ_3: 25

                .= ((v . kon(a)) '&' (v . kon(nega))) by LTLAXIO1: 31

                .= (((v . kon(`1)) '&' (v . kon(<*))) '&' (v . kon(nega))) by LTLAXIO2: 17, A60

                .= (((v . kon(`1)) '&' (v . A)) '&' (v . kon(nega))) by LTLAXIO2: 11

                .= 1 by A54, A51, XBOOLEAN:def 3, A58, A55;

                hence contradiction by A62;

              end;

                suppose

                 A63: (v . A) = 0 ;

                set b = (((ff /. i1) `2 ) ^^ <*A*>), a = ((ff /. i1) `1 );

                i1 in ( dom ff2) by A52, A53, A10, A48, FINSEQ_3: 25;

                then ( rng ((ff /. i1) `2 )) misses ( rng <*A*>) by A15;

                then

                 A64: ( nega (((ff /. i1) `2 ) ^ <*A*>)) = (( nega ((ff /. i1) `2 )) ^ ( nega <*A*>)) & b = (((ff /. i1) `2 ) ^ <*A*>) by LTLAXIO2: 16, LTLAXIO3:def 3;

                ( nega <*A*>) = <*( 'not' A)*> by LTLAXIO2: 14;

                

                then (v . kon(nega)) = (v . ( 'not' A)) by LTLAXIO2: 11

                .= ((v . A) => (v . TFALSUM )) by LTLAXIO1:def 15

                .= 1 by A63;

                then

                 A65: (v . kon(nega)) = ((v . kon(nega)) '&' TRUE ) by A64, LTLAXIO2: 17;

                reconsider j = (( len ff1) + i1) as Element of NAT ;

                

                 A66: j = (( len ( nega ff1)) + i1) by LTLAXIO2:def 4;

                i1 <= ( len ( nega ff2)) by A53, A10, A48, LTLAXIO2:def 4;

                then

                 A67: i1 in ( dom ( nega ff2)) by FINSEQ_3: 25, A52;

                

                 A68: j in ( dom fl) by FINSEQ_1: 28, A52, A53, A10, A48, FINSEQ_3: 25;

                then j <= ( len fl) by FINSEQ_3: 25;

                then

                 A69: j <= ( len ( nega fl)) by LTLAXIO2:def 4;

                

                 A70: (( nega fl) /. j) = ((( nega ff1) ^ ( nega ff2)) /. j) by LTLAXIO2: 16

                .= (( nega ff2) /. i1) by FINSEQ_4: 69, A67, A66

                .= (( nega ff2) . i1) by PARTFUN1:def 6, A67

                .= ( 'not' (ff2 /. i1)) by LTLAXIO2:def 4, A52, A53, A10, A48;

                1 <= j by A68, FINSEQ_3: 25;

                then j in ( dom ( nega fl)) by A69, FINSEQ_3: 25;

                

                then

                 A71: 1 = (v . (( nega fl) /. j)) by A57, LTLAXIO2: 19

                .= ((v . (ff2 /. i1)) => (v . TFALSUM )) by LTLAXIO1:def 15, A70

                .= ((v . (ff2 /. i1)) => FALSE ) by LTLAXIO1:def 15;

                (v . (ff2 /. i1)) = (v . ( [a, b] ^ )) by A10, A52, A53, A48, FINSEQ_3: 25

                .= ((v . kon(a)) '&' (v . kon(nega))) by LTLAXIO1: 31

                .= 1 by A54, A51, XBOOLEAN:def 3, A55, A65;

                hence contradiction by A71;

              end;

            end;

            hence (v . alt(fl)) = 1 by XBOOLEAN:def 3;

          end;

          ( alt(fk) => alt(fl)) is ctaut

          proof

            let g;

            set v = ( VAL g);

            now

              assume (v . ( alt(fk) => alt(fl))) = 0 ;

              then

               A72: ((v . alt(fk)) => (v . alt(fl))) = 0 by LTLAXIO1:def 15;

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

              hence contradiction by A72, A49;

            end;

            hence (v . ( alt(fk) => alt(fl))) = 1 by XBOOLEAN:def 3;

          end;

          then ( alt(fk) => alt(fl)) in LTL_axioms by LTLAXIO1:def 17;

          then

           A73: ( {} l) |- ( alt(fk) => alt(fl)) by LTLAXIO1: 42;

          

           A74: ( rng fk) = (( comp Fp) ^ )

          proof

            hereby

              let x be object;

              assume

               A75: x in ( rng fk);

              then

              reconsider x1 = x as Element of l;

              set i = (x1 .. fk);

              i in ( dom fk) by A75, FINSEQ_4: 20;

              then i in ( dom ff) by A48, FINSEQ_3: 29;

              then

               A76: (ff /. i) in ( comp Fp) by A8, PARTFUN2: 2;

              x1 = (fk /. i) by A75, FINSEQ_5: 38

              .= ((ff /. i) ^ ) by A48, A75, FINSEQ_4: 20;

              hence x in (( comp Fp) ^ ) by A76;

            end;

            let x be object;

            assume x in (( comp Fp) ^ );

            then

            consider P1 be PNPair such that

             A77: x = (P1 ^ ) and

             A78: P1 in ( comp Fp);

            set i = (P1 .. ff);

            i in ( dom ff) by FINSEQ_4: 20, A8, A78;

            then

             A79: i in ( dom fk) by FINSEQ_3: 29, A48;

            

            then (fk /. i) = ((ff /. i) ^ ) by A48

            .= x by A77, FINSEQ_5: 38, A8, A78;

            hence x in ( rng fk) by PARTFUN2: 2, A79;

          end;

          ( card ( tau Fp)) = k by STIRL2_1: 55, A6, A7, A5;

          then ( {} l) |- alt(fk) by A74, A4;

          then ( {} l) |- alt(fl) by A73, LTLAXIO1: 43;

          hence ( {} l) |- alt(g) by A47, LTLAXIO1: 43;

        end;

      end;

      

       A80: P[ 0 ]

      proof

        let F be finite Subset of l;

        assume ( card ( tau F)) = 0 ;

        then

         A81: F = ( {} l);

        let f be FinSequence of l;

        assume

         A82: ( rng f) = (( comp F) ^ );

        then

         A83: (f /. 1) in ( rng f) by FINSEQ_6: 42, RELAT_1: 38;

        

         A84: 1 in ( dom f) by A82, FINSEQ_3: 32;

         alt(f) is ctaut

        proof

          let g;

          set v = ( VAL g);

          (v . (f /. 1)) = (v . ( TVERUM '&&' TVERUM )) by TARSKI:def 1, Th11, A82, Th12, A81, A83

          .= ((v . TVERUM ) '&' (v . TVERUM )) by LTLAXIO1: 31

          .= 1 by LTLAXIO2: 4;

          hence (v . alt(f)) = 1 by XBOOLEAN:def 3, LTLAXIO2: 20, A84;

        end;

        then alt(f) in LTL_axioms by LTLAXIO1:def 17;

        hence ( {} l) |- alt(f) by LTLAXIO1: 42;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A80, A3);

      hence ( {} l) |- alt(f) by A2, A1;

    end;

    theorem :: LTLAXIO4:17

    

     Th17: for P be consistent PNPair, f be FinSequence of LTLB_WFF st ( rng f) = (( comp P) ^ ) holds ( {} LTLB_WFF ) |- ((P ^ ) => ( 'not' (( con ( nega f)) /. ( len ( con ( nega f))))))

    proof

      let P be consistent PNPair, f be FinSequence of l;

      set c = ( comp ( rng P));

      defpred P1a[ PNPair] means ( rng (P `1 )) c= ( rng ($1 `1 )) & ( rng (P `2 )) c= ( rng ($1 `2 ));

      defpred P1[ PNPair] means $1 is consistent & P1a[$1];

      defpred P2[ PNPair] means not ( rng (P `1 )) misses ( rng ($1 `2 )) or not ( rng (P `2 )) misses ( rng ($1 `1 ));

      set c1 = { Pg where Pg be Element of c : P1[Pg] }, c2 = (c \ c1);

      

       A1: c1 c= c from FRAENKEL:sch 10;

      

       A2: c1 = ( comp P)

      proof

        hereby

          let x be object;

          assume x in c1;

          then

          consider Pg be Element of c such that

           A3: Pg = x and

           A4: P1[Pg];

          reconsider Pg as consistent PNPair by A4;

          Pg in c;

          then ex Q st Q = Pg & ( rng Q) = ( tau ( rng P)) & ( rng (Q `1 )) misses ( rng (Q `2 ));

          then Pg is_completion_of P by A4;

          hence x in ( comp P) by A3;

        end;

        let x be object;

        assume x in ( comp P);

        then

        consider Q be consistent PNPair such that

         A5: Q = x and

         A6: Q is_completion_of P;

        ( rng (Q `1 )) misses ( rng (Q `2 )) & ( rng Q) = ( tau ( rng P)) by LTLAXIO3: 30, A6;

        then Q in c;

        then

        reconsider Q as Element of c;

         P1[Q] by A6;

        hence x in c1 by A5;

      end;

      reconsider c1 as finite Subset of [:(l ** ), (l ** ):] by A1, XBOOLE_1: 1;

      

       A7: c = (c1 \/ c2) by XBOOLE_1: 45, A1;

      consider f2 be FinSequence such that

       A8: ( rng f2) = (c2 ^ ) and f2 is one-to-one by FINSEQ_4: 58;

      reconsider f2 as FinSequence of l by A8, FINSEQ_1:def 4;

      set r = kon(nega), s = kon(nega), t = kon(nega);

      assume

       A9: ( rng f) = (( comp P) ^ );

       A10:

      now

        let x be PNPair;

        assume

         A11: x in c2;

        then

        reconsider x1 = x as Element of c by XBOOLE_0:def 5;

        assume P1[x];

        then x1 in c1;

        hence contradiction by A11, XBOOLE_0:def 5;

      end;

       A12:

      now

        let pi be PNPair;

        assume

         A13: pi in c2;

        then pi in ( comp ( rng P)) by XBOOLE_0:def 5;

        then

         A14: ex Q st Q = pi & ( rng Q) = ( tau ( rng P)) & ( rng (Q `1 )) misses ( rng (Q `2 ));

        per cases by A10, A13;

          suppose

           A15: pi is Inconsistent;

          (( 'not' (pi ^ )) => ((P ^ ) => ( 'not' (pi ^ )))) is ctaut by LTLAXIO2: 33;

          then (( 'not' (pi ^ )) => ((P ^ ) => ( 'not' (pi ^ )))) in LTL_axioms by LTLAXIO1:def 17;

          then

           A16: ( {} l) |- (( 'not' (pi ^ )) => ((P ^ ) => ( 'not' (pi ^ )))) by LTLAXIO1: 42;

          ( {} l) |- ( 'not' (pi ^ )) by A15;

          hence ( {} l) |- ((P ^ ) => ( 'not' (pi ^ ))) by A16, LTLAXIO1: 43;

        end;

          suppose

           A17: not P1a[pi];

           A18:

          now

            per cases by A17;

              suppose not ( rng (P `1 )) c= ( rng (pi `1 ));

              then

              consider x be object such that

               A19: x in ( rng (P `1 )) and

               A20: not x in ( rng (pi `1 ));

              ( rng (P `1 )) c= ( rng P) by XBOOLE_1: 7;

              then ( rng P) c= ( tau ( rng P)) & x in ( rng P) by LTLAXIO3: 16, A19;

              then x in ( rng (pi `2 )) by A14, XBOOLE_0:def 3, A20;

              then x in (( rng (P `1 )) /\ ( rng (pi `2 ))) by XBOOLE_0:def 4, A19;

              hence P2[pi] by XBOOLE_0:def 7;

            end;

              suppose not ( rng (P `2 )) c= ( rng (pi `2 ));

              then

              consider x be object such that

               A21: x in ( rng (P `2 )) and

               A22: not x in ( rng (pi `2 ));

              ( rng (P `2 )) c= ( rng P) by XBOOLE_1: 7;

              then ( rng P) c= ( tau ( rng P)) & x in ( rng P) by LTLAXIO3: 16, A21;

              then x in ( rng (pi `1 )) by A14, XBOOLE_0:def 3, A22;

              then x in (( rng (P `2 )) /\ ( rng (pi `1 ))) by XBOOLE_0:def 4, A21;

              hence P2[pi] by XBOOLE_0:def 7;

            end;

          end;

           A23:

          now

            per cases by A18;

              suppose

               A24: not ( rng (P `1 )) misses ( rng (pi `2 ));

              set Q1 = [(P `1 ), (pi `2 )], p = kon(`1), q = kon(nega);

               not ( rng (Q1 `1 )) misses ( rng (Q1 `2 )) by A24;

              then Q1 is Inconsistent by LTLAXIO3: 30;

              then

               A25: ( {} l) |- ( 'not' (Q1 ^ ));

              

               A26: (( 'not' ( kon(`1) '&&' kon(nega))) => ( 'not' ((P ^ ) '&&' (pi ^ )))) is ctaut by LTLAXIO2: 42;

              (( 'not' (Q1 ^ )) => ( 'not' ((P ^ ) '&&' (pi ^ )))) in LTL_axioms by A26, LTLAXIO1:def 17;

              then ( {} l) |- (( 'not' (Q1 ^ )) => ( 'not' ((P ^ ) '&&' (pi ^ )))) by LTLAXIO1: 42;

              hence ( {} l) |- ( 'not' ((P ^ ) '&&' (pi ^ ))) by LTLAXIO1: 43, A25;

            end;

              suppose

               A27: not ( rng (P `2 )) misses ( rng (pi `1 ));

              set Q2 = [(pi `1 ), (P `2 )], p = kon(`1), q = kon(nega);

               not ( rng (Q2 `2 )) misses ( rng (Q2 `1 )) by A27;

              then Q2 is Inconsistent by LTLAXIO3: 30;

              then

               A28: ( {} l) |- ( 'not' (Q2 ^ ));

              

               A29: (( 'not' ( kon(`1) '&&' kon(nega))) => ( 'not' ((P ^ ) '&&' (pi ^ )))) is ctaut by LTLAXIO2: 41;

              (( 'not' (Q2 ^ )) => ( 'not' ((P ^ ) '&&' (pi ^ )))) in LTL_axioms by A29, LTLAXIO1:def 17;

              then ( {} l) |- (( 'not' (Q2 ^ )) => ( 'not' ((P ^ ) '&&' (pi ^ )))) by LTLAXIO1: 42;

              hence ( {} l) |- ( 'not' ((P ^ ) '&&' (pi ^ ))) by LTLAXIO1: 43, A28;

            end;

          end;

          (( 'not' ((P ^ ) '&&' (pi ^ ))) => ((P ^ ) => ( 'not' (pi ^ )))) is ctaut by LTLAXIO2: 37;

          then (( 'not' ((P ^ ) '&&' (pi ^ ))) => ((P ^ ) => ( 'not' (pi ^ )))) in LTL_axioms by LTLAXIO1:def 17;

          then ( {} l) |- (( 'not' ((P ^ ) '&&' (pi ^ ))) => ((P ^ ) => ( 'not' (pi ^ )))) by LTLAXIO1: 42;

          hence ( {} l) |- ((P ^ ) => ( 'not' (pi ^ ))) by LTLAXIO1: 43, A23;

        end;

      end;

      

       A30: for p st p in (c2 ^ ) holds ( {} l) |- ((P ^ ) => ( 'not' p))

      proof

        let p;

        assume p in (c2 ^ );

        then ex Q st p = (Q ^ ) & Q in c2;

        hence ( {} l) |- ((P ^ ) => ( 'not' p)) by A12;

      end;

       A31:

      now

        per cases ;

          suppose

           A32: ( len f2) = 0 ;

          ((P ^ ) => TVERUM ) is ctaut

          proof

            let g;

            set v = ( VAL g);

            

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

            .= ((v . (P ^ )) => TRUE ) by LTLAXIO2: 4

            .= 1;

          end;

          then

           A33: ((P ^ ) => TVERUM ) in LTL_axioms by LTLAXIO1:def 17;

          ( len ( nega f2)) = 0 by A32, LTLAXIO2:def 4;

          then ( nega f2) = {} ;

          hence ( {} l) |- ((P ^ ) => t) by A33, LTLAXIO1: 42, LTLAXIO2: 10;

        end;

          suppose

           A34: ( len f2) > 0 ;

          set t1 = ( con ( nega f2));

          

           A35: ( len ( nega f2)) > 0 by A34, LTLAXIO2:def 4;

          then

          reconsider lt1 = ( len t1) as non zero Nat by LTLAXIO2:def 2;

          defpred P3[ Nat] means $1 <= ( len t1) implies ( {} l) |- ((P ^ ) => (t1 /. $1));

           A36:

          now

            let k be non zero Nat such that

             A37: P3[k];

            thus P3[(k + 1)]

            proof

              set a = (t1 /. k), b = (( nega f2) /. (k + 1));

              reconsider k1 = k as non empty Element of NAT by ORDINAL1:def 12;

              assume

               A38: (k + 1) <= ( len t1);

              (((P ^ ) => a) => (((P ^ ) => b) => ((P ^ ) => (a '&&' b)))) is ctaut by LTLAXIO2: 40;

              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

               A39: ( {} l) |- (((P ^ ) => b) => ((P ^ ) => (a '&&' b))) by LTLAXIO1: 43, A38, NAT_1: 13, A37;

              

               A40: (k + 1) <= ( len ( nega f2)) by A38, LTLAXIO2:def 2, A35;

              then (k + 1) <= ( len f2) by LTLAXIO2:def 4;

              then

               A41: (k1 + 1) in ( dom f2) by NAT_1: 12, FINSEQ_3: 25;

              then ( {} l) |- ((P ^ ) => ( 'not' (f2 /. (k + 1)))) by PARTFUN2: 2, A8, A30;

              then ( {} l) |- ((P ^ ) => b) by LTLAXIO2: 8, A41;

              then 1 <= k1 & ( {} l) |- ((P ^ ) => (a '&&' b)) by NAT_1: 25, A39, LTLAXIO1: 43;

              hence ( {} l) |- ((P ^ ) => (t1 /. (k + 1))) by LTLAXIO2: 7, NAT_1: 13, A40;

            end;

          end;

          

           A42: P3[1]

          proof

            assume 1 <= ( len t1);

            1 <= ( len f2) by A34, NAT_1: 25;

            then

             A43: 1 in ( dom f2) by FINSEQ_3: 25;

            (t1 /. 1) = (( nega f2) /. 1) by A35, LTLAXIO2: 6

            .= ( 'not' (f2 /. 1)) by LTLAXIO2: 8, A43;

            hence thesis by PARTFUN2: 2, A43, A8, A30;

          end;

          for k be non zero Nat holds P3[k] from NAT_1:sch 10( A42, A36);

          then ( {} l) |- ((P ^ ) => (t1 /. lt1));

          hence ( {} l) |- ((P ^ ) => t);

        end;

      end;

      

       A44: ( nega (f ^ f2)) = (( nega f) ^ ( nega f2)) by LTLAXIO2: 16;

      now

        let g;

        set v = ( VAL g);

        

         A45: (v . r) = FALSE or (v . r) = TRUE by XBOOLEAN:def 3;

        

         A46: (v . r) = ((v . s) '&' (v . t)) by LTLAXIO2: 17, A44;

        

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

        .= (((v . r) => (v . TFALSUM )) => (v . ( 'not' (s '&&' t)))) by LTLAXIO1:def 15

        .= (((v . r) => FALSE ) => (v . ( 'not' (s '&&' t)))) by LTLAXIO1:def 15

        .= (((v . r) => FALSE ) => ((v . (s '&&' t)) => (v . TFALSUM ))) by LTLAXIO1:def 15

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

        .= 1 by A45, A46, LTLAXIO1: 31;

      end;

      then (( 'not' r) => ( 'not' (s '&&' t))) is ctaut;

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

      then

       A47: ( {} l) |- (( 'not' r) => ( 'not' (s '&&' t))) by LTLAXIO1: 42;

      (( 'not' (s '&&' t)) => (((P ^ ) => t) => ((P ^ ) => ( 'not' s)))) is ctaut by LTLAXIO2: 39;

      then (( 'not' (s '&&' t)) => (((P ^ ) => t) => ((P ^ ) => ( 'not' s)))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A48: ( {} l) |- (( 'not' (s '&&' t)) => (((P ^ ) => t) => ((P ^ ) => ( 'not' s)))) by LTLAXIO1: 42;

      ( rng (f ^ f2)) = (( rng f) \/ ( rng f2)) by FINSEQ_1: 31

      .= (c ^ ) by A7, Th10, A9, A2, A8;

      then ( {} l) |- ( 'not' r) by Th16;

      then ( {} l) |- ( 'not' (s '&&' t)) by A47, LTLAXIO1: 43;

      then ( {} l) |- (((P ^ ) => t) => ((P ^ ) => ( 'not' s))) by A48, LTLAXIO1: 43;

      hence ( {} l) |- ((P ^ ) => ( 'not' s)) by LTLAXIO1: 43, A31;

    end;

    begin

    definition

      let X;

      :: LTLAXIO4:def8

      func untn X -> Subset of LTLB_WFF equals { ( untn (A,B)) where A be Element of LTLB_WFF , B be Element of LTLB_WFF : (A 'U' B) in X };

      coherence

      proof

        set c = { ( untn (A,B)) where A be Element of l, B be Element of l : (A 'U' B) in X };

        c c= l

        proof

          let x be object;

          assume x in c;

          then ex A,B be Element of l st x = ( untn (A,B)) & (A 'U' B) in X;

          hence x in l;

        end;

        hence thesis;

      end;

    end

    registration

      let X be finite Subset of LTLB_WFF ;

      cluster ( untn X) -> finite;

      coherence

      proof

        defpred P[ Element of l, Element of l] means ex p, q st $1 = (p 'U' q) & $2 = ( untn (p,q));

        set c = { A where A be Element of l : ex B st P[B, A] & B in X };

        

         A1: ( untn X) = c

        proof

          hereby

            let x be object;

            assume x in ( untn X);

            then ex A, B st x = ( untn (A,B)) & (A 'U' B) in X;

            hence x in c;

          end;

          let x be object;

          assume x in c;

          then ex A st x = A & ex B be Element of l st P[B, A] & B in X;

          hence x in ( untn X);

        end;

         A2:

        now

          let w be Element of l, x,y be Element of l;

          assume that

           A3: P[w, x] and

           A4: P[w, y];

          consider p, q such that

           A5: w = (p 'U' q) and

           A6: x = ( untn (p,q)) by A3;

          consider A, B such that

           A7: w = (A 'U' B) and

           A8: y = ( untn (A,B)) by A4;

          p = A by A5, A7, HILBERT2: 19;

          hence x = y by A5, A7, HILBERT2: 19, A6, A8;

        end;

        

         A9: X is finite;

        c is finite from FRAENKEL:sch 28( A9, A2);

        hence thesis by A1;

      end;

    end

    definition

      let P;

      :: LTLAXIO4:def9

      func untn P -> non empty finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] equals { Q where Q be PNPair : ( rng (Q `1 )) = ( untn ( rng (P `1 ))) & ( rng (Q `2 )) = ( untn ( rng (P `2 ))) };

      coherence

      proof

        defpred P[ PNPair] means ( rng ($1 `1 )) = ( untn ( rng (P `1 ))) & ( rng ($1 `2 )) = ( untn ( rng (P `2 )));

        set s = (( untn ( rng (P `1 ))) \/ ( untn ( rng (P `2 ))));

        consider f be FinSequence such that

         A1: ( rng f) = ( untn ( rng (P `1 ))) and

         A2: f is one-to-one by FINSEQ_4: 58;

        reconsider f as one-to-one FinSequence of l by A1, A2, FINSEQ_1:def 4;

        consider g be FinSequence such that

         A3: ( rng g) = ( untn ( rng (P `2 ))) and

         A4: g is one-to-one by FINSEQ_4: 58;

        reconsider g as one-to-one FinSequence of l by A3, A4, FINSEQ_1:def 4;

        

         A5: ( rng ( [f, g] `1 )) = ( untn ( rng (P `1 ))) by A1;

        

         A6: { A where A be PNPair : P[A] } c= [:(s ** ), (s ** ):]

        proof

          let x be object;

          assume x in { A where A be PNPair : P[A] };

          then

          consider Q such that

           A7: x = Q and

           A8: ( rng (Q `1 )) = ( untn ( rng (P `1 ))) and

           A9: ( rng (Q `2 )) = ( untn ( rng (P `2 )));

          consider y,z be object such that

           A10: y in (l ** ) & z in (l ** ) and

           A11: Q = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as one-to-one FinSequence of l by A10, LTLAXIO3:def 2;

          ( rng (Q `1 )) c= s by A8, XBOOLE_1: 7;

          then

           A12: ( rng y) c= s by A11;

          ( rng (Q `2 )) c= s by A9, XBOOLE_1: 7;

          then

           A13: ( rng z) c= s by A11;

          reconsider y as one-to-one FinSequence of s by A12, FINSEQ_1:def 4;

          reconsider z as one-to-one FinSequence of s by A13, FINSEQ_1:def 4;

          y in (s ** ) & z in (s ** ) by LTLAXIO3:def 2;

          hence thesis by ZFMISC_1:def 2, A11, A7;

        end;

        ( rng ( [f, g] `2 )) = ( untn ( rng (P `2 ))) by A3;

        then

         A14: [f, g] in { A where A be PNPair : P[A] } by A5;

        { A where A be PNPair : P[A] } c= [:(l ** ), (l ** ):] from FRAENKEL:sch 10;

        hence thesis by A14, A6;

      end;

    end

    theorem :: LTLAXIO4:18

    

     Th18: for Q be Element of ( untn P) holds ( {} LTLB_WFF ) |- ((P ^ ) => ( 'X' (Q ^ )))

    proof

      let Q be Element of ( untn P);

      set p = ( 'X' kon(`1)), q = ( 'X' kon(nega));

      Q in ( untn P);

      then

       A1: ex Q1 be PNPair st Q = Q1 & ( rng (Q1 `1 )) = ( untn ( rng (P `1 ))) & ( rng (Q1 `2 )) = ( untn ( rng (P `2 )));

      now

        let i be Nat;

        assume

         A2: i in ( dom ( nex ( nega (Q `2 ))));

        

         A3: ( len ( nex ( nega (Q `2 )))) = ( len ( nega (Q `2 ))) by LTLAXIO2:def 5;

        then ( len ( nex ( nega (Q `2 )))) = ( len (Q `2 )) by LTLAXIO2:def 4;

        then

         A4: i in ( dom (Q `2 )) by FINSEQ_3: 29, A2;

        then ((Q `2 ) /. i) in ( untn ( rng (P `2 ))) by PARTFUN2: 2, A1;

        then

        consider A, B such that

         A5: ((Q `2 ) /. i) = ( untn (A,B)) and

         A6: (A 'U' B) in ( rng (P `2 ));

        i in ( dom ( nega (Q `2 ))) by A3, A2, FINSEQ_3: 29;

        

        then

         A7: (( nex ( nega (Q `2 ))) /. i) = ( 'X' (( nega (Q `2 )) /. i)) by LTLAXIO2: 9

        .= ( 'X' ( 'not' ((Q `2 ) /. i))) by LTLAXIO2: 8, A4;

        ( {} l) |- (( 'not' (A 'U' B)) => ( 'X' ( 'not' ( untn (A,B))))) & ( {} l) |- ((P ^ ) => ( 'not' (A 'U' B))) by LTLAXIO2: 63, LTLAXIO3: 29, A6;

        hence ( {} l) |- ((P ^ ) => (( nex ( nega (Q `2 ))) /. i)) by A7, LTLAXIO1: 47, A5;

      end;

      then ( {} l) |- ( kon(nex) => q) & ( {} l) |- ((P ^ ) => kon(nex)) by LTLAXIO2: 60, LTLAXIO2: 56;

      then

       A8: ( {} l) |- ((P ^ ) => q) by LTLAXIO1: 47;

      now

        let i be Nat;

        assume

         A9: i in ( dom ( nex (Q `1 )));

        ( len (Q `1 )) = ( len ( nex (Q `1 ))) by LTLAXIO2:def 5;

        then

         A10: i in ( dom (Q `1 )) by A9, FINSEQ_3: 29;

        then ((Q `1 ) /. i) in ( untn ( rng (P `1 ))) by PARTFUN2: 2, A1;

        then

        consider A, B such that

         A11: ((Q `1 ) /. i) = ( untn (A,B)) and

         A12: (A 'U' B) in ( rng (P `1 ));

        

         A13: ( {} l) |- ((P ^ ) => (A 'U' B)) by LTLAXIO3: 28, A12;

        ((A 'U' B) => (( 'X' B) 'or' ( 'X' (A '&&' (A 'U' B))))) in LTL_axioms by LTLAXIO1:def 17;

        then

         A14: ( {} l) |- ((A 'U' B) => (( 'X' B) 'or' ( 'X' (A '&&' (A 'U' B))))) by LTLAXIO1: 42;

        ( {} l) |- ((( 'X' B) 'or' ( 'X' (A '&&' (A 'U' B)))) => ( 'X' ( untn (A,B)))) by LTLAXIO2: 61;

        then

         A15: ( {} l) |- ((A 'U' B) => ( 'X' ( untn (A,B)))) by LTLAXIO1: 47, A14;

        (( nex (Q `1 )) /. i) = ( 'X' ( untn (A,B))) by A11, LTLAXIO2: 9, A10;

        hence ( {} l) |- ((P ^ ) => (( nex (Q `1 )) /. i)) by A15, LTLAXIO1: 47, A13;

      end;

      then ( {} l) |- ( kon(nex) => p) & ( {} l) |- ((P ^ ) => kon(nex)) by LTLAXIO2: 60, LTLAXIO2: 56;

      then

       A16: ( {} l) |- ((P ^ ) => p) by LTLAXIO1: 47;

      (((P ^ ) => p) => (((P ^ ) => q) => ((P ^ ) => (p '&&' q)))) is ctaut by LTLAXIO2: 40;

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

      then ( {} l) |- (((P ^ ) => p) => (((P ^ ) => q) => ((P ^ ) => (p '&&' q)))) by LTLAXIO1: 42;

      then ( {} l) |- (((P ^ ) => q) => ((P ^ ) => (p '&&' q))) by LTLAXIO1: 43, A16;

      then

       A17: ( {} l) |- ((P ^ ) => (p '&&' q)) by LTLAXIO1: 43, A8;

      ( {} l) |- ((( 'X' kon(`1)) '&&' ( 'X' kon(nega))) => ( 'X' (Q ^ ))) by LTLAXIO1: 53;

      hence ( {} l) |- ((P ^ ) => ( 'X' (Q ^ ))) by LTLAXIO1: 47, A17;

    end;

    registration

      let P be consistent PNPair;

      cluster -> consistent for Element of ( untn P);

      coherence

      proof

        let Q be Element of ( untn P);

        assume not Q is consistent;

        then

         A1: ( {} l) |- ( 'X' ( 'not' (Q ^ ))) by LTLAXIO1: 44;

        ( {} l) |- ((P ^ ) => ( 'X' (Q ^ ))) by Th18;

        then

         A2: ( {} l) |- (( 'not' ( 'X' (Q ^ ))) => ( 'not' (P ^ ))) by LTLAXIO1: 52;

        (( 'X' ( 'not' (Q ^ ))) => ( 'not' ( 'X' (Q ^ )))) in LTL_axioms by LTLAXIO1:def 17;

        then ( {} l) |- (( 'X' ( 'not' (Q ^ ))) => ( 'not' ( 'X' (Q ^ )))) by LTLAXIO1: 42;

        then ( {} l) |- ( 'not' ( 'X' (Q ^ ))) by A1, LTLAXIO1: 43;

        hence contradiction by A2, LTLAXIO1: 43, LTLAXIO3:def 10;

      end;

    end

    definition

      let P;

      :: LTLAXIO4:def10

      func compn P -> finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] equals { Q where Q be Element of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] : Q in ( comp ( untn P)) };

      coherence

      proof

        defpred P1[ PNPair] means $1 in ( comp ( untn P));

        deffunc F1( PNPair) = $1;

        

         A1: ( comp ( untn P)) is finite;

        

         A2: { F1(Q) where Q be Element of pairs : Q in ( comp ( untn P)) } is finite from FRAENKEL:sch 21( A1);

        { Q where Q be PNPair : P1[Q] } c= [:(l ** ), (l ** ):] from FRAENKEL:sch 10;

        hence thesis by A2;

      end;

    end

    registration

      let P be consistent PNPair;

      cluster ( compn P) -> non empty;

      coherence

      proof

        consider x be object such that

         A1: x in ( untn P) by XBOOLE_0:def 1;

        reconsider x as consistent PNPair by A1;

        consider y be object such that

         A2: y in ( comp x) by XBOOLE_0:def 1;

        reconsider y as PNPair by A2;

        ( comp x) in { ( comp Q) where Q be Element of pairs : Q in ( untn P) } by A1;

        then y in ( comp ( untn P)) by A2, TARSKI:def 4;

        then y in { Q where Q be PNPair : Q in ( comp ( untn P)) };

        hence thesis;

      end;

    end

    registration

      let P be consistent PNPair;

      cluster -> consistent for Element of ( compn P);

      coherence

      proof

        let Q be Element of ( compn P);

        Q in ( compn P);

        then

        consider R be PNPair such that

         A1: R = Q and

         A2: R in ( comp ( untn P));

        consider x such that

         A3: R in x and

         A4: x in { ( comp S) where S be Element of pairs : S in ( untn P) } by TARSKI:def 4, A2;

        consider S be PNPair such that

         A5: x = ( comp S) and

         A6: S in ( untn P) by A4;

        reconsider S as Element of ( untn P) by A6;

        reconsider R as Element of ( comp S) by A3, A5;

        R is consistent;

        hence Q is consistent by A1;

      end;

    end

    theorem :: LTLAXIO4:19

    

     Th19: Q in ( compn P) & R in ( untn P) implies Q is_completion_of R

    proof

      assume that

       A1: Q in ( compn P) and

       A2: R in ( untn P);

      consider Q1 be PNPair such that

       A3: Q1 = Q and

       A4: Q1 in ( comp ( untn P)) by A1;

      

       A5: ex R1 be PNPair st R1 = R & ( rng (R1 `1 )) = ( untn ( rng (P `1 ))) & ( rng (R1 `2 )) = ( untn ( rng (P `2 ))) by A2;

      consider x such that

       A6: Q1 in x and

       A7: x in { ( comp S) where S be PNPair : S in ( untn P) } by A4, TARSKI:def 4;

      consider S be PNPair such that

       A8: x = ( comp S) and

       A9: S in ( untn P) by A7;

      consider Q2 be consistent PNPair such that

       A10: Q2 = Q1 and

       A11: Q2 is_completion_of S by A6, A8;

      

       A12: ex S1 be PNPair st S1 = S & ( rng (S1 `1 )) = ( untn ( rng (P `1 ))) & ( rng (S1 `2 )) = ( untn ( rng (P `2 ))) by A9;

      ( tau ( rng S)) = ( rng Q2) by A11;

      then

       A13: ( tau ( rng R)) = ( rng Q) by A3, A10, A12, A5;

      ( rng (R `1 )) c= ( rng (Q `1 )) & ( rng (R `2 )) c= ( rng (Q `2 )) by A11, A3, A10, A12, A5;

      hence Q is_completion_of R by A13;

    end;

    theorem :: LTLAXIO4:20

    

     Th20: Q in ( compn P) implies Q is complete

    proof

      assume

       A1: Q in ( compn P);

      then

      consider Q1 be PNPair such that Q1 = Q and

       A2: Q1 in ( comp ( untn P));

      consider x such that Q1 in x and

       A3: x in { ( comp R) where R be PNPair : R in ( untn P) } by A2, TARSKI:def 4;

      ex R be PNPair st x = ( comp R) & R in ( untn P) by A3;

      hence Q is complete by Th19, A1, Th13;

    end;

    registration

      let P be consistent PNPair;

      cluster -> complete for Element of ( compn P);

      coherence by Th20;

    end

    theorem :: LTLAXIO4:21

    

     Th21: (A 'U' B) in ( rng (P `2 )) & Q in ( compn P) implies ( untn (A,B)) in ( rng (Q `2 ))

    proof

      assume that

       A1: (A 'U' B) in ( rng (P `2 )) and

       A2: Q in ( compn P);

      consider Q1 be Element of pairs such that Q = Q1 and

       A3: Q1 in ( comp ( untn P)) by A2;

      consider x such that Q1 in x and

       A4: x in { ( comp R) where R be Element of pairs : R in ( untn P) } by TARSKI:def 4, A3;

      consider R be PNPair such that x = ( comp R) and

       A5: R in ( untn P) by A4;

      ex R1 be PNPair st R1 = R & ( rng (R1 `1 )) = ( untn ( rng (P `1 ))) & ( rng (R1 `2 )) = ( untn ( rng (P `2 ))) by A5;

      then

       A6: ( untn (A,B)) in ( rng (R `2 )) by A1;

      Q is_completion_of R by A5, A2, Th19;

      then ( rng (R `2 )) c= ( rng (Q `2 ));

      hence ( untn (A,B)) in ( rng (Q `2 )) by A6;

    end;

    theorem :: LTLAXIO4:22

    

     Th22: (A 'U' B) in ( rng (P `1 )) & Q in ( compn P) implies ( untn (A,B)) in ( rng (Q `1 ))

    proof

      assume that

       A1: (A 'U' B) in ( rng (P `1 )) and

       A2: Q in ( compn P);

      consider Q1 be Element of pairs such that Q = Q1 and

       A3: Q1 in ( comp ( untn P)) by A2;

      consider x such that Q1 in x and

       A4: x in { ( comp R) where R be Element of pairs : R in ( untn P) } by TARSKI:def 4, A3;

      consider R be PNPair such that x = ( comp R) and

       A5: R in ( untn P) by A4;

      ex R1 be PNPair st R1 = R & ( rng (R1 `1 )) = ( untn ( rng (P `1 ))) & ( rng (R1 `2 )) = ( untn ( rng (P `2 ))) by A5;

      then

       A6: ( untn (A,B)) in ( rng (R `1 )) by A1;

      Q is_completion_of R by A5, A2, Th19;

      then ( rng (R `1 )) c= ( rng (Q `1 ));

      hence ( untn (A,B)) in ( rng (Q `1 )) by A6;

    end;

    theorem :: LTLAXIO4:23

    

     Th23: R in ( compn Q) & ( rng Q) c= ( union ( Subt ( rng P))) implies ( rng R) c= ( union ( Subt ( rng P)))

    proof

      assume that

       A1: R in ( compn Q) and

       A2: ( rng Q) c= ( union ( Subt ( rng P)));

      consider R1 be PNPair such that

       A3: R1 = R and

       A4: R1 in ( comp ( untn Q)) by A1;

      consider z such that

       A5: R1 in z and

       A6: z in { ( comp S) where S be PNPair : S in ( untn Q) } by A4, TARSKI:def 4;

      consider T be PNPair such that

       A7: z = ( comp T) and

       A8: T in ( untn Q) by A6;

      

       A9: ex T1 be PNPair st T1 = T & ( rng (T1 `1 )) = ( untn ( rng (Q `1 ))) & ( rng (T1 `2 )) = ( untn ( rng (Q `2 ))) by A8;

      let x be object;

      assume

       A10: x in ( rng R);

      ex R2 be consistent PNPair st R2 = R1 & R2 is_completion_of T by A7, A5;

      then x in ( tau ( rng T)) by A3, A10;

      then

      consider p such that

       A11: p in ( rng T) and

       A12: x in ( tau1 . p) by LTLAXIO3:def 5;

      per cases by XBOOLE_0:def 3, A9, A11;

        suppose p in ( untn ( rng (Q `1 )));

        then

        consider A, B such that

         A13: p = ( untn (A,B)) and

         A14: (A 'U' B) in ( rng (Q `1 ));

        set aub = (A 'U' B);

        ( rng (Q `1 )) c= ( rng Q) by XBOOLE_1: 7;

        then aub in ( rng Q) by A14;

        then

        consider y such that

         A15: aub in y and

         A16: y in ( Subt ( rng P)) by A2, TARSKI:def 4;

        consider q be Element of l such that

         A17: y = ( Sub . q) and q in ( rng P) by A16;

        ( tau1 . ( untn (A,B))) c= (( tau1 . ( untn (A,B))) \/ (( Sub . A) \/ ( Sub . B))) by XBOOLE_1: 7;

        then ( tau1 . ( untn (A,B))) c= ((( tau1 . ( untn (A,B))) \/ ( Sub . A)) \/ ( Sub . B)) by XBOOLE_1: 4;

        then ( tau1 . ( untn (A,B))) c= ( Sub . aub) by LTLAXIO3:def 6;

        then x in ( Sub . q) by A17, A15, LTLAXIO3: 26, A13, A12;

        hence x in ( union ( Subt ( rng P))) by A17, A16, TARSKI:def 4;

      end;

        suppose p in ( untn ( rng (Q `2 )));

        then

        consider A, B such that

         A18: p = ( untn (A,B)) and

         A19: (A 'U' B) in ( rng (Q `2 ));

        set aub = (A 'U' B);

        ( rng (Q `2 )) c= ( rng Q) by XBOOLE_1: 7;

        then aub in ( rng Q) by A19;

        then

        consider y such that

         A20: aub in y and

         A21: y in ( Subt ( rng P)) by A2, TARSKI:def 4;

        consider q be Element of l such that

         A22: y = ( Sub . q) and q in ( rng P) by A21;

        ( tau1 . ( untn (A,B))) c= (( tau1 . ( untn (A,B))) \/ (( Sub . A) \/ ( Sub . B))) by XBOOLE_1: 7;

        then ( tau1 . ( untn (A,B))) c= ((( tau1 . ( untn (A,B))) \/ ( Sub . A)) \/ ( Sub . B)) by XBOOLE_1: 4;

        then ( tau1 . ( untn (A,B))) c= ( Sub . aub) by LTLAXIO3:def 6;

        then x in ( Sub . q) by A22, A20, LTLAXIO3: 26, A18, A12;

        hence x in ( union ( Subt ( rng P))) by A22, A21, TARSKI:def 4;

      end;

    end;

    theorem :: LTLAXIO4:24

    

     Th24: for P be consistent complete PNPair, Q be Element of ( compn P) st (A 'U' B) in ( rng (P `2 )) holds B in ( rng (Q `2 )) & (A in ( rng (Q `2 )) or (A 'U' B) in ( rng (Q `2 )))

    proof

      let P be consistent complete PNPair, Q be Element of ( compn P);

      set aub = (A 'U' B), nb = ( 'not' B), na = ( 'not' A), au = (A '&&' aub);

      (( 'not' ( untn (A,B))) => (nb '&&' ( 'not' au))) is ctaut by LTLAXIO2: 36;

      then (( 'not' ( untn (A,B))) => (nb '&&' ( 'not' au))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A1: ( {} l) |- (( 'not' ( untn (A,B))) => (nb '&&' ( 'not' au))) by LTLAXIO1: 42;

      assume aub in ( rng (P `2 ));

      then

       A2: ( untn (A,B)) in ( rng (Q `2 )) by Th21;

      then

       A3: ( untn (A,B)) in ( rng Q) by XBOOLE_0:def 3;

      then

       A4: A in ( rng Q) by Th8;

      ( {} l) |- ((Q ^ ) => ( 'not' ( untn (A,B)))) by LTLAXIO3: 29, A2;

      then

       A5: ( {} l) |- ((Q ^ ) => (nb '&&' ( 'not' au))) by A1, LTLAXIO1: 47;

      ((nb '&&' ( 'not' au)) => nb) is ctaut by LTLAXIO2: 27;

      then ((nb '&&' ( 'not' au)) => nb) in LTL_axioms by LTLAXIO1:def 17;

      then ( {} l) |- ((nb '&&' ( 'not' au)) => nb) by LTLAXIO1: 42;

      then

       A6: ( {} l) |- ((Q ^ ) => nb) by LTLAXIO1: 47, A5;

      ((nb '&&' ( 'not' au)) => ( 'not' au)) is ctaut by LTLAXIO2: 28;

      then ((nb '&&' ( 'not' au)) => ( 'not' au)) in LTL_axioms by LTLAXIO1:def 17;

      then ( {} l) |- ((nb '&&' ( 'not' au)) => ( 'not' au)) by LTLAXIO1: 42;

      then

       A7: ( {} l) |- ((Q ^ ) => ( 'not' au)) by LTLAXIO1: 47, A5;

      

       A8: B in ( rng Q) by A3, Th8;

      

       A9: aub in ( rng Q) by A3, Th8;

      assume

       A10: not B in ( rng (Q `2 )) or not (A in ( rng (Q `2 )) or aub in ( rng (Q `2 )));

      per cases by A10;

        suppose not B in ( rng (Q `2 ));

        then B in ( rng (Q `1 )) by A8, XBOOLE_0:def 3;

        then ( {} l) |- ((Q ^ ) => B) by LTLAXIO3: 28;

        then ( {} l) |- ((Q ^ ) => (B '&&' nb)) by LTLAXIO2: 52, A6;

        then ( {} l) |- ( 'not' (Q ^ )) by LTLAXIO2: 55;

        hence contradiction by LTLAXIO3:def 10;

      end;

        suppose

         A11: not A in ( rng (Q `2 )) & not aub in ( rng (Q `2 ));

        then A in ( rng (Q `1 )) by XBOOLE_0:def 3, A4;

        then

         A12: ( {} l) |- ((Q ^ ) => A) by LTLAXIO3: 28;

        aub in ( rng (Q `1 )) by A11, XBOOLE_0:def 3, A9;

        then ( {} l) |- ((Q ^ ) => aub) by LTLAXIO3: 28;

        then ( {} l) |- ((Q ^ ) => au) by A12, LTLAXIO2: 52;

        then ( {} l) |- ((Q ^ ) => (au '&&' ( 'not' au))) by LTLAXIO2: 52, A7;

        then ( {} l) |- ( 'not' (Q ^ )) by LTLAXIO2: 55;

        hence contradiction by LTLAXIO3:def 10;

      end;

    end;

    theorem :: LTLAXIO4:25

    

     Th25: for P be consistent complete PNPair, Q be Element of ( compn P) st (A 'U' B) in ( rng (P `1 )) holds (B in ( rng (Q `1 )) or A in ( rng (Q `1 )) & (A 'U' B) in ( rng (Q `1 )))

    proof

      let P be consistent complete PNPair, Q be Element of ( compn P);

      set aub = (A 'U' B), nb = ( 'not' B), na = ( 'not' A), nu = ( 'not' aub);

      assume aub in ( rng (P `1 ));

      then

       A1: ( untn (A,B)) in ( rng (Q `1 )) by Th22;

      then

       A2: ( untn (A,B)) in ( rng Q) by XBOOLE_0:def 3;

      then

       A3: A in ( rng Q) by Th8;

      

       A4: aub in ( rng Q) by A2, Th8;

      

       A5: ( {} l) |- ((Q ^ ) => ( untn (A,B))) by LTLAXIO3: 28, A1;

      (((Q ^ ) => ( untn (A,B))) => (((Q ^ ) => (na '&&' nb)) => ( 'not' (Q ^ )))) is ctaut by LTLAXIO2: 50;

      then (((Q ^ ) => ( untn (A,B))) => (((Q ^ ) => (na '&&' nb)) => ( 'not' (Q ^ )))) in LTL_axioms by LTLAXIO1:def 17;

      then ( {} l) |- (((Q ^ ) => ( untn (A,B))) => (((Q ^ ) => (na '&&' nb)) => ( 'not' (Q ^ )))) by LTLAXIO1: 42;

      then

       A6: ( {} l) |- (((Q ^ ) => (na '&&' nb)) => ( 'not' (Q ^ ))) by LTLAXIO1: 43, A5;

      (((Q ^ ) => ( untn (A,B))) => (((Q ^ ) => (nb '&&' nu)) => ( 'not' (Q ^ )))) is ctaut by LTLAXIO2: 51;

      then (((Q ^ ) => ( untn (A,B))) => (((Q ^ ) => (nb '&&' nu)) => ( 'not' (Q ^ )))) in LTL_axioms by LTLAXIO1:def 17;

      then ( {} l) |- (((Q ^ ) => ( untn (A,B))) => (((Q ^ ) => (nb '&&' nu)) => ( 'not' (Q ^ )))) by LTLAXIO1: 42;

      then

       A7: ( {} l) |- (((Q ^ ) => (nb '&&' nu)) => ( 'not' (Q ^ ))) by LTLAXIO1: 43, A5;

      assume that

       A8: not B in ( rng (Q `1 )) and

       A9: not A in ( rng (Q `1 )) or not aub in ( rng (Q `1 ));

      B in ( rng Q) by A2, Th8;

      then B in ( rng (Q `2 )) by A8, XBOOLE_0:def 3;

      then

       A10: ( {} l) |- ((Q ^ ) => nb) by LTLAXIO3: 29;

      per cases by A9;

        suppose not A in ( rng (Q `1 ));

        then A in ( rng (Q `2 )) by A3, XBOOLE_0:def 3;

        then ( {} l) |- ((Q ^ ) => na) by LTLAXIO3: 29;

        then ( {} l) |- ((Q ^ ) => (na '&&' nb)) by LTLAXIO2: 52, A10;

        hence contradiction by LTLAXIO1: 43, A6, LTLAXIO3:def 10;

      end;

        suppose not aub in ( rng (Q `1 ));

        then aub in ( rng (Q `2 )) by XBOOLE_0:def 3, A4;

        then ( {} l) |- ((Q ^ ) => nu) by LTLAXIO3: 29;

        then ( {} l) |- ((Q ^ ) => (nb '&&' nu)) by LTLAXIO2: 52, A10;

        hence contradiction by LTLAXIO1: 43, A7, LTLAXIO3:def 10;

      end;

    end;

    begin

    definition

      let P;

      :: LTLAXIO4:def11

      mode pnptree of P -> finite-branching DecoratedTree of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] means

      : Def11: (it . {} ) = P & for t be Element of ( dom it ) holds for w be Element of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] st w = (it . t) holds ( succ (it ,t)) = the Enumeration of ( compn w);

      correctness

      proof

        deffunc F3( Element of pairs) = the Enumeration of ( compn $1);

        ex T be finite-branching DecoratedTree of pairs st (T . {} ) = P & for t be Element of ( dom T) holds for w be Element of pairs st w = (T . t) holds ( succ (T,t)) = F3(w) from TREES_9:sch 2;

        hence thesis;

      end;

    end

    reserve T for pnptree of P,

t for Node of T;

    definition

      let P, T, t;

      :: original: |

      redefine

      func T | t -> pnptree of (T . t) ;

      correctness

      proof

        set k = (T | t);

        

         A1: ( dom k) = (( dom T) | t) by TREES_2:def 10;

         A2:

        now

          let u be Element of ( dom k);

          reconsider tu = (t ^ u) as Element of ( dom T) by A1, TREES_1:def 6;

          let w be Element of pairs;

          assume w = (k . u);

          then

           A3: w = (T . (t ^ u)) by A1, TREES_2:def 10;

          

          thus ( succ (k,u)) = ( succ (T,tu)) by TREES_9: 31

          .= the Enumeration of ( compn w) by Def11, A3;

        end;

        (k . {} ) = (T . t) by TREES_9: 35;

        hence thesis by A2, Def11;

      end;

    end

    theorem :: LTLAXIO4:26

    

     Th26: for n be Nat st (t ^ <*n*>) in ( dom T) holds (T . (t ^ <*n*>)) in ( compn (T . t))

    proof

      let n be Nat;

      set tn = (t ^ <*n*>);

      assume

       A1: (t ^ <*n*>) in ( dom T);

      ( dom ( succ (T,t))) = ( dom (t succ )) by TREES_9: 38;

      then

       A2: (( succ (T,t)) . (n + 1)) in ( rng ( succ (T,t))) by TREES_9: 39, A1, FUNCT_1: 3;

      

       A3: ( succ (T,t)) = the Enumeration of ( compn (T . t)) by Def11;

      (T . tn) = (( succ (T,t)) . (n + 1)) by A1, TREES_9: 40;

      hence (T . tn) in ( compn (T . t)) by A3, A2, RLAFFIN3:def 1;

    end;

    theorem :: LTLAXIO4:27

    

     Th27: Q in ( rng T) implies ( rng Q) c= ( union ( Subt ( rng P)))

    proof

      deffunc F( PNPair) = { ( Sub . A) where A be Element of l : A in ( rng $1) };

      defpred P1[ set] means for Q st Q = (T . $1) & $1 in ( dom T) holds ( rng Q) c= ( union ( Subt ( rng P)));

      assume Q in ( rng T);

      then

      consider x be object such that

       A1: x in ( dom T) and

       A2: (T . x) = Q by FUNCT_1:def 3;

      reconsider x as Element of ( dom T) by A1;

       A3:

      now

        let t be Element of ( dom T), n be Nat;

        assume that

         A4: P1[t] and (t ^ <*n*>) in ( dom T);

        

         A5: ( rng (T . t)) c= ( union ( Subt ( rng P))) by A4;

        thus P1[(t ^ <*n*>)]

        proof

          let Q;

          assume Q = (T . (t ^ <*n*>)) & (t ^ <*n*>) in ( dom T);

          then Q in ( compn (T . t)) by Th26;

          hence ( rng Q) c= ( union ( Subt ( rng P))) by Th23, A5;

        end;

      end;

      

       A6: P1[ {} ]

      proof

        let Q;

        assume that

         A7: Q = (T . {} ) and {} in ( dom T);

        Q = P by A7, Def11;

        hence thesis by Th9;

      end;

      for t be Element of ( dom T) holds P1[t] from TREES_2:sch 1( A6, A3);

      then ( rng (T . x)) c= ( union ( Subt ( rng P)));

      hence thesis by A2;

    end;

    registration

      let P, T;

      cluster ( rng T) -> non empty finite;

      coherence

      proof

        set a = ( union ( Subt ( rng P)));

         {} in ( dom T) by TREES_1: 22;

        hence ( rng T) is non empty by FUNCT_1: 3;

        ( rng T) c= [:(a ** ), (a ** ):]

        proof

          let x be object;

          assume

           A1: x in ( rng T);

          then

          reconsider x1 = x as PNPair;

          

           A2: ( rng x1) c= a by Th27, A1;

          ( rng (x1 `1 )) c= ( rng x1) by XBOOLE_1: 7;

          then (x1 `1 ) is one-to-one FinSequence of a by XBOOLE_1: 1, A2, FINSEQ_1:def 4;

          then

           A3: (x1 `1 ) in (a ** ) by LTLAXIO3:def 2;

          ( rng (x1 `2 )) c= ( rng x1) by XBOOLE_1: 7;

          then (x1 `2 ) is one-to-one FinSequence of a by XBOOLE_1: 1, A2, FINSEQ_1:def 4;

          then

           A4: (x1 `2 ) in (a ** ) by LTLAXIO3:def 2;

          consider y,z be object such that

           A5: y in (l ** ) & z in (l ** ) and

           A6: x1 = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as one-to-one FinSequence of l by A5, LTLAXIO3:def 2;

          thus thesis by A3, A4, ZFMISC_1:def 2, A6;

        end;

        hence thesis;

      end;

    end

    registration

      let P be consistent PNPair;

      let T be pnptree of P;

      cluster -> consistent for Element of ( rng T);

      coherence

      proof

        let y be Element of ( rng T);

        defpred P1[ set] means for Q st Q = (T . $1) & $1 in ( dom T) holds Q is consistent;

        

         A1: ex x be object st x in ( dom T) & (T . x) = y by FUNCT_1:def 3;

         A2:

        now

          let t be Element of ( dom T), n be Nat;

          assume that

           A3: P1[t] and (t ^ <*n*>) in ( dom T);

          reconsider pQ = (T . t) as consistent PNPair by A3;

          thus P1[(t ^ <*n*>)]

          proof

            let Q;

            assume Q = (T . (t ^ <*n*>)) & (t ^ <*n*>) in ( dom T);

            then

            reconsider Q1 = Q as Element of ( compn pQ) by Th26;

            Q1 is consistent;

            hence thesis;

          end;

        end;

        

         A4: P1[ {} ] by Def11;

        for t be Element of ( dom T) holds P1[t] from TREES_2:sch 1( A4, A2);

        hence thesis by A1;

      end;

    end

    registration

      let P be consistent complete PNPair;

      let T be pnptree of P;

      cluster -> complete for Element of ( rng T);

      coherence

      proof

        let y be Element of ( rng T);

        defpred P1[ set] means for Q st Q = (T . $1) & $1 in ( dom T) holds Q is complete;

        

         A1: ex x be object st x in ( dom T) & (T . x) = y by FUNCT_1:def 3;

         A2:

        now

          let t be Element of ( dom T), n be Nat;

          assume that

           A3: P1[t] and (t ^ <*n*>) in ( dom T);

          reconsider Tt = (T . t) as Element of ( rng T) by FUNCT_1:def 3;

          reconsider pQ = Tt as consistent complete PNPair by A3;

          thus P1[(t ^ <*n*>)]

          proof

            let Q;

            assume Q = (T . (t ^ <*n*>)) & (t ^ <*n*>) in ( dom T);

            then

            reconsider Q1 = Q as Element of ( compn pQ) by Th26;

            Q1 is consistent;

            hence thesis;

          end;

        end;

        

         A4: P1[ {} ] by Def11;

        for t be Element of ( dom T) holds P1[t] from TREES_2:sch 1( A4, A2);

        hence thesis by A1;

      end;

    end

    registration

      let P be consistent complete PNPair, T be pnptree of P, t be Node of T;

      cluster (T . t) -> consistent complete;

      coherence

      proof

        reconsider Tt = (T . t) as Element of ( rng T) by FUNCT_1: 3;

        Tt is consistent;

        hence thesis;

      end;

    end

    registration

      let P be consistent PNPair, T be pnptree of P;

      let t be Element of ( dom T);

      cluster ( succ t) -> non empty;

      coherence

      proof

        reconsider w = (T . t) as Element of ( rng T) by FUNCT_1:def 3;

        reconsider w as consistent PNPair;

        ( succ (T,t)) = the Enumeration of ( compn w) by Def11;

        then ( rng ( succ (T,t))) = ( compn w) by RLAFFIN3:def 1;

        then

        consider y be object such that

         A1: y in ( rng ( succ (T,t))) by XBOOLE_0:def 1;

        ex x be Element of ( dom T) st y = (T . x) & x in ( succ t) by TREES_9: 42, A1;

        hence thesis;

      end;

    end

    definition

      let P, T;

      :: LTLAXIO4:def12

      func rngr T -> finite Subset of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):] equals { (T . t) where t be Node of T : t <> {} };

      correctness

      proof

        set r = { (T . t) where t be Node of T : t <> {} };

        r c= ( rng T)

        proof

          let x be object;

          assume x in r;

          then ex t be Node of T st x = (T . t) & t <> {} ;

          hence thesis by FUNCT_1: 3;

        end;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    registration

      let P be consistent PNPair, T be pnptree of P;

      cluster ( rngr T) -> non empty;

      coherence

      proof

        reconsider e = {} as Element of ( dom T) by TREES_1: 22;

        consider x be object such that

         A1: x in ( succ e) by XBOOLE_0:def 1;

        reconsider x as Element of ( dom T) by A1;

        ex n be Nat st x = (e ^ <*n*>) & (e ^ <*n*>) in ( dom T) by A1;

        then (T . x) in ( rngr T);

        hence thesis;

      end;

    end

    theorem :: LTLAXIO4:28

    

     Th28: R in ( rng T) & Q in ( untn R) implies ( comp Q) c= ( rngr T)

    proof

      assume that

       A1: R in ( rng T) and

       A2: Q in ( untn R);

      let S be object;

      assume

       A3: S in ( comp Q);

      ( comp Q) c= ( comp ( untn R)) by Th14, A2;

      then

       A4: S in ( compn R) by A3;

      consider t be object such that

       A5: t in ( dom T) and

       A6: (T . t) = R by FUNCT_1:def 3, A1;

      reconsider t as Element of ( dom T) by A5;

      ( succ (T,t)) = the Enumeration of ( compn R) by Def11, A6;

      then S in ( rng ( succ (T,t))) by RLAFFIN3:def 1, A4;

      then

      consider t1 be Element of ( dom T) such that

       A7: S = (T . t1) and

       A8: t1 in ( succ t) by TREES_9: 42;

      ex n be Nat st t1 = (t ^ <*n*>) & (t ^ <*n*>) in ( dom T) by A8;

      hence S in ( rngr T) by A7;

    end;

    theorem :: LTLAXIO4:29

    

     Th29: for P be consistent complete PNPair, T be pnptree of P, f be FinSequence of LTLB_WFF st ( rng f) = (( rngr T) ^ ) holds ( {} LTLB_WFF ) |- (( 'not' (( con ( nega f)) /. ( len ( con ( nega f))))) => ( 'X' ( 'not' (( con ( nega f)) /. ( len ( con ( nega f)))))))

    proof

      let P be consistent complete PNPair, T be pnptree of P, f be FinSequence of l;

      assume

       A1: ( rng f) = (( rngr T) ^ );

       A2:

      now

        let R be Element of ( rng T);

        consider Q be object such that

         A3: Q in ( untn R) by XBOOLE_0:def 1;

        reconsider Q as Element of ( untn R) by A3;

        consider g be FinSequence such that

         A4: ( rng g) = (( comp Q) ^ ) and g is one-to-one by FINSEQ_4: 58;

        reconsider g as FinSequence of l by A4, FINSEQ_1:def 4;

        

         A5: ( {} l) |- ((R ^ ) => ( 'X' (Q ^ ))) by Th18;

        reconsider Q as consistent PNPair;

        now

          let j be Nat;

          assume j in ( dom g);

          then (g /. j) in (( comp Q) ^ ) by PARTFUN2: 2, A4;

          then

          consider S be PNPair such that

           A6: (g /. j) = (S ^ ) and

           A7: S in ( comp Q);

          ( comp Q) c= ( rngr T) by Th28;

          then (S ^ ) in (( rngr T) ^ ) by A7;

          then

          consider k such that

           A8: k in ( dom f) and

           A9: (f /. k) = (g /. j) by A6, A1, PARTFUN2: 2;

          ((f /. k) => alt(f)) is ctaut by LTLAXIO2: 29, A8;

          then ((f /. k) => alt(f)) in LTL_axioms by LTLAXIO1:def 17;

          hence ( {} l) |- ((g /. j) => alt(f)) by LTLAXIO1: 42, A9;

        end;

        then

         A10: ( {} l) |- ( alt(g) => alt(f)) by LTLAXIO2: 57;

        (( 'X' ((Q ^ ) => alt(f))) => (( 'X' (Q ^ )) => ( 'X' alt(f)))) in LTL_axioms by LTLAXIO1:def 17;

        then

         A11: ( {} l) |- (( 'X' ((Q ^ ) => alt(f))) => (( 'X' (Q ^ )) => ( 'X' alt(f)))) by LTLAXIO1: 42;

        ( {} l) |- ((Q ^ ) => alt(g)) by Th17, A4;

        then ( {} l) |- ( 'X' ((Q ^ ) => alt(f))) by A10, LTLAXIO1: 47, LTLAXIO1: 44;

        then ( {} l) |- (( 'X' (Q ^ )) => ( 'X' alt(f))) by A11, LTLAXIO1: 43;

        hence ( {} l) |- ((R ^ ) => ( 'X' alt(f))) by LTLAXIO1: 47, A5;

      end;

      now

        let i be Nat;

        assume i in ( dom f);

        then (f /. i) in (( rngr T) ^ ) by PARTFUN2: 2, A1;

        then

        consider R such that

         A12: (f /. i) = (R ^ ) and

         A13: R in ( rngr T);

        ex t be Node of T st R = (T . t) & t <> {} by A13;

        then R in ( rng T) by FUNCT_1: 3;

        hence ( {} l) |- ((f /. i) => ( 'X' alt(f))) by A2, A12;

      end;

      hence ( {} l) |- ( alt(f) => ( 'X' alt(f))) by LTLAXIO2: 57;

    end;

    begin

    definition

      let P be consistent PNPair;

      let T be pnptree of P;

      :: LTLAXIO4:def13

      mode path of T -> sequence of ( dom T) means

      : Def13: (it . 0 ) = {} & for k be Nat holds (it . (k + 1)) in ( succ (it . k));

      existence

      proof

        set F1 = ( dom T);

        reconsider F2 = {} as Element of F1 by TREES_1: 22;

        defpred P1[ Nat, Element of F1, Element of F1] means $3 in ( succ $2);

         A1:

        now

          let n be Nat;

          let x be Element of F1;

          consider y be object such that

           A2: y in ( succ x) by XBOOLE_0:def 1;

          reconsider y as Element of F1 by A2;

          thus ex y be Element of F1 st P1[n, x, y] by A2;

        end;

        consider f be sequence of F1 such that

         A3: (f . 0 ) = F2 & for n be Nat holds P1[n, (f . n) qua Element of F1, (f . (n + 1)) qua Element of F1] from RECDEF_1:sch 2( A1);

        thus thesis by A3;

      end;

    end

    definition

      let P be consistent complete PNPair, T be pnptree of P, t be path of T, i;

      :: original: .

      redefine

      func t . i -> Node of T ;

      coherence

      proof

        (t . i) is Element of ( dom T);

        hence thesis;

      end;

    end

    theorem :: LTLAXIO4:30

    

     Th30: for P be consistent complete PNPair, T be pnptree of P, t be path of T st (A 'U' B) in ( rng ((T . (t . i)) `2 )) holds for j st j > i holds (B in ( rng ((T . (t . j)) `2 )) or ex k st i < k & k < j & A in ( rng ((T . (t . k)) `2 )))

    proof

      set aub = (A 'U' B);

      let P be consistent complete PNPair, T be pnptree of P, t be path of T;

      assume

       A1: aub in ( rng ((T . (t . i)) `2 ));

      given j such that

       A2: j > i and

       A3: not B in ( rng ((T . (t . j)) `2 )) and

       A4: for k st i < k & k < j holds not A in ( rng ((T . (t . k)) `2 ));

      

       A5: j >= (i + 1) by A2, NAT_1: 13;

      per cases by A5, XXREAL_0: 1;

        suppose j = (i + 1);

        then (t . j) in ( succ (t . i)) by Def13;

        then ex n be Nat st (t . j) = ((t . i) ^ <*n*>) & ((t . i) ^ <*n*>) in ( dom T);

        then (T . (t . j)) in ( compn (T . (t . i))) by Th26;

        hence contradiction by Th24, A1, A3;

      end;

        suppose

         A6: j > (i + 1);

        (i + 1) >= 1 by NAT_1: 11;

        then

        reconsider j1 = (j - 1) as Element of NAT by XXREAL_0: 2, A6, NAT_1: 21;

        defpred P[ Nat] means i < $1 & $1 < j implies aub in ( rng ((T . (t . $1)) `2 ));

        j = (j1 + 1);

        then (t . j) in ( succ (t . j1)) by Def13;

        then ex n be Nat st (t . j) = ((t . j1) ^ <*n*>) & ((t . j1) ^ <*n*>) in ( dom T);

        then

         A7: (T . (t . j)) in ( compn (T . (t . j1))) by Th26;

         A8:

        now

          let k be Nat;

          set k1 = (k + 1);

          assume

           A9: P[k];

          thus P[k1]

          proof

            assume that

             A10: i < k1 and

             A11: k1 < j;

            

             A12: i <= k by NAT_1: 13, A10;

            per cases by A12, XXREAL_0: 1;

              suppose

               A13: i < k;

              set Pk1 = (T . (t . k1));

              (t . k1) in ( succ (t . k)) by Def13;

              then ex n be Nat st (t . k1) = ((t . k) ^ <*n*>) & ((t . k) ^ <*n*>) in ( dom T);

              then Pk1 in ( compn (T . (t . k))) by Th26;

              then A in ( rng (Pk1 `2 )) or aub in ( rng (Pk1 `2 )) by Th24, A11, NAT_1: 16, XXREAL_0: 2, A13, A9;

              hence aub in ( rng ((T . (t . k1)) `2 )) by A4, A10, A11;

            end;

              suppose

               A14: i = k;

              set Pk1 = (T . (t . k1));

              (t . k1) in ( succ (t . i)) by A14, Def13;

              then ex n be Nat st (t . k1) = ((t . i) ^ <*n*>) & ((t . i) ^ <*n*>) in ( dom T);

              then Pk1 in ( compn (T . (t . i))) by Th26;

              then A in ( rng (Pk1 `2 )) or aub in ( rng (Pk1 `2 )) by Th24, A1;

              hence aub in ( rng ((T . (t . k1)) `2 )) by A4, A10, A11;

            end;

          end;

        end;

        

         A15: (j + ( - 1)) < j & (j + ( - 1)) > ((i + 1) + ( - 1)) by XREAL_1: 30, A6, XREAL_1: 8;

        

         A16: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A16, A8);

        then aub in ( rng ((T . (t . j1)) `2 )) by A15;

        hence contradiction by Th24, A7, A3;

      end;

    end;

    theorem :: LTLAXIO4:31

    

     Th31: for P be consistent complete PNPair, T be pnptree of P st (A 'U' B) in ( rng (P `1 )) & (for Q be Element of ( rngr T) holds not B in ( rng (Q `1 ))) holds for Q be Element of ( rngr T) holds B in ( rng (Q `2 )) & (A 'U' B) in ( rng (Q `1 ))

    proof

      set aub = (A 'U' B);

      let P be consistent complete PNPair, T be pnptree of P;

      assume that

       A1: aub in ( rng (P `1 )) and

       A2: for Q be Element of ( rngr T) holds not B in ( rng (Q `1 ));

      defpred P[ set] means for t be Element of ( dom T) st t = $1 & t <> 0 holds B in ( rng ((T . t) `2 )) & aub in ( rng ((T . t) `1 ));

       A3:

      now

        let t be Element of ( dom T), n be Nat;

        assume that

         A4: P[t] and (t ^ <*n*>) in ( dom T);

        thus P[(t ^ <*n*>)]

        proof

          let u be Element of ( dom T);

          assume that

           A5: u = (t ^ <*n*>) and u <> 0 ;

          

           A6: (T . u) in ( rngr T) by A5;

          per cases ;

            suppose t = 0 ;

            then (T . t) = P by Def11;

            then

            reconsider Tu = (T . u) as Element of ( compn P) by Th26, A5;

            ( untn (A,B)) in ( rng (Tu `1 )) & ( rng (Tu `1 )) c= ( rng Tu) by Th22, A1, XBOOLE_1: 7;

            then

             A7: B in ( rng Tu) by Th8;

             not B in ( rng (Tu `1 )) by A2, A6;

            hence B in ( rng ((T . u) `2 )) & aub in ( rng ((T . u) `1 )) by Th25, A1, A7, XBOOLE_0:def 3;

          end;

            suppose

             A8: not t = 0 ;

            reconsider Tu = (T . u) as Element of ( compn (T . t)) by Th26, A5;

            ( rng (Tu `1 )) c= ( rng Tu) & ( untn (A,B)) in ( rng (Tu `1 )) by XBOOLE_1: 7, A8, A4, Th22;

            then

             A9: B in ( rng Tu) by Th8;

            

             A10: aub in ( rng ((T . t) `1 )) by A8, A4;

             not B in ( rng (Tu `1 )) by A2, A6;

            hence B in ( rng ((T . u) `2 )) & aub in ( rng ((T . u) `1 )) by A10, A9, Th25, XBOOLE_0:def 3;

          end;

        end;

      end;

      let Q be Element of ( rngr T);

      Q in ( rngr T);

      then

       A11: ex t be Element of ( dom T) st Q = (T . t) & t <> 0 ;

      

       A12: P[ {} ];

      for t be Element of ( dom T) holds P[t] from TREES_2:sch 1( A12, A3);

      hence B in ( rng (Q `2 )) & (A 'U' B) in ( rng (Q `1 )) by A11;

    end;

    theorem :: LTLAXIO4:32

    

     Th32: for P be consistent complete PNPair, T be pnptree of P st (A 'U' B) in ( rng (P `1 )) holds ex R be Element of ( rngr T) st B in ( rng (R `1 ))

    proof

      let P be consistent complete PNPair, T be pnptree of P;

      set nb = ( 'not' B), gnb = ( 'G' nb), xgnb = ( 'X' gnb), aub = (A 'U' B);

      set f = the Enumeration of (( rngr T) ^ );

      set xaf = ( 'X' alt(f));

      

       A1: ( rng f) = (( rngr T) ^ ) by RLAFFIN3:def 1;

       {} in ( dom T) by TREES_1: 22;

      then (T . {} ) in ( rng T) by FUNCT_1: 3;

      then

       A2: P in ( rng T) by Def11;

      reconsider f as FinSequence of l;

      assume

       A3: aub in ( rng (P `1 ));

      assume

       A4: for R be Element of ( rngr T) holds not B in ( rng (R `1 ));

      now

        let i be Nat;

        assume i in ( dom f);

        then (f /. i) in (( rngr T) ^ ) by PARTFUN2: 2, A1;

        then

        consider R such that

         A5: (f /. i) = (R ^ ) and

         A6: R in ( rngr T);

        B in ( rng (R `2 )) by Th31, A3, A4, A6;

        hence ( {} l) |- ((f /. i) => nb) by LTLAXIO3: 29, A5;

      end;

      then

       A7: ( {} l) |- ( alt(f) => nb) by LTLAXIO2: 57;

      (( 'X' ( alt(f) => gnb)) => (xaf => xgnb)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A8: ( {} l) |- (( 'X' ( alt(f) => gnb)) => (xaf => xgnb)) by LTLAXIO1: 42;

      ( {} l) |- ( alt(f) => xaf) by Th29, A1;

      then ( {} l) |- ( 'X' ( alt(f) => gnb)) by LTLAXIO1: 45, A7, LTLAXIO1: 44;

      then

       A9: ( {} l) |- (xaf => xgnb) by A8, LTLAXIO1: 43;

      consider R be object such that

       A10: R in ( untn P) by XBOOLE_0:def 1;

      reconsider R as Element of ( untn P) by A10;

      set xr = ( 'X' (R ^ ));

      set g = the Enumeration of (( comp R) ^ );

      reconsider g as FinSequence of l;

      

       A11: ( rng g) = (( comp R) ^ ) by RLAFFIN3:def 1;

      (( rngr T) ^ ) = ((( comp R) \/ ( rngr T)) ^ ) by Th28, XBOOLE_1: 12, A2

      .= ((( comp R) ^ ) \/ (( rngr T) ^ )) by Th10;

      then ( alt(g) => alt(f)) is ctaut by XBOOLE_1: 7, A11, A1, LTLAXIO2: 30;

      then ( alt(g) => alt(f)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A12: ( {} l) |- ( alt(g) => alt(f)) by LTLAXIO1: 42;

      

       A13: ( {} l) |- ((P ^ ) => xr) by Th18;

      (( 'X' ((R ^ ) => alt(f))) => (xr => xaf)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A14: ( {} l) |- (( 'X' ((R ^ ) => alt(f))) => (xr => xaf)) by LTLAXIO1: 42;

      ( {} l) |- ((R ^ ) => alt(g)) by A11, Th17;

      then ( {} l) |- ( 'X' ((R ^ ) => alt(f))) by A12, LTLAXIO1: 47, LTLAXIO1: 44;

      then ( {} l) |- (xr => xaf) by LTLAXIO1: 43, A14;

      then ( {} l) |- ((P ^ ) => xaf) by LTLAXIO1: 47, A13;

      then

       A15: ( {} l) |- ((P ^ ) => xgnb) by LTLAXIO1: 47, A9;

      

       A16: ( {} l) |- ((P ^ ) => aub) by LTLAXIO3: 28, A3;

      (aub => ( 'X' ( 'F' B))) in LTL_axioms by LTLAXIO1:def 17;

      then

       A17: ( {} l) |- (aub => ( 'X' ( 'F' B))) by LTLAXIO1: 42;

      (( 'X' ( 'F' B)) => ( 'not' xgnb)) in LTL_axioms by LTLAXIO1:def 17;

      then ( {} l) |- (( 'X' ( 'F' B)) => ( 'not' xgnb)) by LTLAXIO1: 42;

      then ( {} l) |- (aub => ( 'not' xgnb)) by A17, LTLAXIO1: 47;

      then ( {} l) |- ((P ^ ) => ( 'not' xgnb)) by LTLAXIO1: 47, A16;

      then ( {} l) |- ((P ^ ) => (xgnb '&&' ( 'not' xgnb))) by A15, LTLAXIO2: 52;

      then ( {} l) |- ( 'not' (P ^ )) by LTLAXIO2: 55;

      hence contradiction by LTLAXIO3:def 10;

    end;

    definition

      let P be consistent PNPair, T be pnptree of P;

      let t be path of T;

      :: LTLAXIO4:def14

      attr t is complete means

      : Def14: for i st (A 'U' B) in ( rng ((T . (t . i)) `1 )) holds ex j st j > i & B in ( rng ((T . (t . j)) `1 )) & for k st i < k & k < j holds A in ( rng ((T . (t . k)) `1 ));

    end

    registration

      let P be consistent complete PNPair, T be pnptree of P;

      cluster complete for path of T;

      existence

      proof

        set YN = { ( rng R) where R be Element of pairs : R in ( rng T) };

        

         A1: ( rng T) is finite;

        

         A2: YN is finite from FRAENKEL:sch 21( A1);

        YN is finite-membered

        proof

          let x;

          assume x in YN;

          then

          consider R be Element of pairs such that

           A3: x = ( rng R) & R in ( rng T);

          thus x is finite by A3;

        end;

        then

        reconsider YN as finite finite-membered set by A2;

        now

          let x;

          assume x in YN;

          then

          consider R be Element of pairs such that

           A4: x = ( rng R) & R in ( rng T);

          thus x c= l by A4;

        end;

        then

        reconsider Tforms = ( union YN) as finite Subset of l by ZFMISC_1: 76;

        defpred P1[ Element of l] means $1 in Tforms & $1 is s-until;

        set uns = { p where p be Element of l : P1[p] };

        

         A5: uns c= l from FRAENKEL:sch 10;

        uns c= Tforms

        proof

          let x be object;

          assume x in uns;

          then ex p st p = x & P1[p];

          hence x in Tforms;

        end;

        then

        reconsider uns as finite Subset of l by A5;

        reconsider e = 0 as Element of ( dom T) by TREES_1: 22;

        set f = the Function of NAT , ( dom T);

        set m = ( card uns);

        consider g be FinSequence such that

         A6: ( rng g) = uns and

         A7: g is one-to-one by FINSEQ_4: 58;

        reconsider g as one-to-one FinSequence of l by A6, A7, FINSEQ_1:def 4;

        defpred P[ Nat, Element of ( dom T), Element of ( dom T)] means ( not (g . (($1 mod m) + 1)) in ( rng ((T . $2) `1 )) implies $3 in ( succ $2)) & ((g . (($1 mod m) + 1)) in ( rng ((T . $2) `1 )) implies $2 is_a_proper_prefix_of $3 & ( rarg (g /. (($1 mod m) + 1))) in ( rng ((T . $3) `1 )));

        

         A8: ( card g) = m by A6, PRE_POLY: 19;

         A9:

        now

          let n be Nat;

          let x be Node of T;

          

           A10: ex t be object st t in ( succ x) by XBOOLE_0:def 1;

          set gk = (g . ((n mod m) + 1));

          per cases ;

            suppose not gk in ( rng ((T . x) `1 ));

            hence ex y be Node of T st P[n, x, y] by A10;

          end;

            suppose

             A11: gk in ( rng ((T . x) `1 ));

            

             A12: 1 <= ((n mod m) + 1) by NAT_1: 25;

            per cases ;

              suppose uns = {} ;

              then ( dom g) = {} by A6, RELAT_1: 42;

              then

               A13: gk = 0 by FUNCT_1:def 2;

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

              hence ex y be Node of T st P[n, x, y] by HILBERT2: 10, A13, A11;

            end;

              suppose uns <> {} ;

              then ((n mod m) + 1) <= m by NAT_D: 1, NAT_1: 13;

              then

               A14: ((n mod m) + 1) in ( dom g) by A8, FINSEQ_3: 25, A12;

              then gk in uns by FUNCT_1: 3, A6;

              then

              consider puq be Element of l such that

               A15: gk = puq and puq in Tforms and

               A16: puq is s-until;

              consider p, q such that

               A17: gk = (p 'U' q) by A15, A16, HILBERT2:def 6;

              consider R be Element of ( rngr (T | x)) such that

               A18: q in ( rng (R `1 )) by A11, Th32, A17;

              R in ( rngr (T | x));

              then

              consider t be Node of (T | x) such that

               A19: R = ((T | x) . t) and

               A20: t <> 0 ;

              t in ( dom (T | x));

              then

               A21: t in (( dom T) | x) by TREES_2:def 10;

              then

              reconsider y = (x ^ t) as Node of T by TREES_1:def 6;

              

               A22: x is_a_proper_prefix_of y by TREES_1: 10, A20;

              (g /. ((n mod m) + 1)) = puq by A15, PARTFUN1:def 6, A14;

              then

               A23: ( rarg (g /. ((n mod m) + 1))) = q by Def1, A15, A16, A17;

              ((T . y) `1 ) = (R `1 ) by A19, TREES_2:def 10, A21;

              hence ex y be Node of T st P[n, x, y] by A18, A23, A11, A22;

            end;

          end;

        end;

        consider p be sequence of ( dom T) such that

         A24: (p . 0 ) = e & for n be Nat holds P[n, (p . n) qua Element of ( dom T), (p . (n + 1)) qua Element of ( dom T)] from RECDEF_1:sch 2( A9);

        defpred Q[ Nat] means $1 <= ( len (p . $1) qua Node of T);

         A25:

        now

          let k be Nat;

          defpred P3[ Nat] means ex t be FinSequence st ((p . $1) qua Node of T ^ t) = (p . ($1 + 1)) qua Node of T & t <> {} ;

          reconsider pk = (p . k), pk1 = (p . (k + 1)) as Node of T;

          

           A26: P[k, pk, pk1] by A24;

          per cases ;

            suppose not (g . ((k mod m) + 1)) in ( rng ((T . pk) `1 ));

            then ex n be Nat st pk1 = (pk ^ <*n*>) & (pk ^ <*n*>) in ( dom T) by A26;

            hence P3[k];

          end;

            suppose (g . ((k mod m) + 1)) in ( rng ((T . pk) `1 ));

            then

             A27: pk is_a_proper_prefix_of pk1 by A24;

            then

            consider r be FinSequence such that

             A28: pk1 = (pk ^ r) by TREES_1: 1;

            r <> 0 by FINSEQ_1: 34, A27, A28;

            hence P3[k] by A28;

          end;

        end;

         A29:

        now

          let k be Nat;

          assume

           A30: Q[k];

          reconsider pk = (p . k), pk1 = (p . (k + 1)) as Node of T;

          consider t be FinSequence such that

           A31: pk1 = (pk ^ t) and

           A32: t <> {} by A25;

          ( len t) >= 1 by A32, NAT_1: 25;

          then (( len pk) + ( len t)) >= (k + 1) by A30, XREAL_1: 7;

          hence Q[(k + 1)] by A31, FINSEQ_1: 22;

        end;

        defpred P4[ Nat] means for i st i <= $1 holds (p . i) c= (p . $1);

        deffunc F3( Element of NAT ) = ((p . $1) qua Node of T | $1);

        consider f be sequence of ( dom T) such that

         A33: for n holds (f . n) = F3(n) from FUNCT_2:sch 4;

         A34:

        now

          let k be Nat;

          reconsider pk = (p . k), pk1 = (p . (k + 1)) as Node of T;

          assume

           A35: P4[k];

          thus P4[(k + 1)]

          proof

            let i;

             A36:

            now

              assume i < (k + 1);

              then i <= k by NAT_1: 13;

              then

               A37: (p . i) c= (p . k) by A35;

              ex t be FinSequence st (pk ^ t) = pk1 & t <> 0 by A25;

              then pk c= pk1 by FINSEQ_6: 10;

              hence (p . i) c= (p . (k + 1)) by A37;

            end;

            assume i <= (k + 1);

            hence thesis by A36, XXREAL_0: 1;

          end;

        end;

        

         A38: Q[ 0 ];

        

         A39: for n be Nat holds Q[n] from NAT_1:sch 2( A38, A29);

        

         A40: P4[ 0 ];

        

         A41: for j be Nat holds P4[j] from NAT_1:sch 2( A40, A34);

         A42:

        now

          let k be Nat;

          reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

          reconsider fk = (f . k), fk1 = (f . (k + 1)) as Element of ( dom T);

          reconsider pk = (p . k), pk1 = (p . (k + 1)) as Node of T;

          (k + 1) <= ( len pk1) by A39;

          then

           A43: ( len (pk1 | (k + 1))) = (k + 1) by FINSEQ_1: 59;

          k1 <= ( len pk) by A39;

          then ( len (pk | k)) = k by FINSEQ_1: 59;

          then

           A44: ( len fk) = k by A33;

          

           A45: k1 < (k1 + 1) by NAT_1: 13;

          then pk c= pk1 by A41;

          then (pk | k) c= (pk1 | (k + 1)) by RELAT_1: 77, A45, FINSEQ_1: 5;

          then (f . k1) c= (pk1 | (k + 1)) by A33;

          then fk is_a_prefix_of fk1 by A33;

          then

          consider r be FinSequence such that

           A46: fk1 = (fk ^ r) by TREES_1: 1;

          ( rng r) c= ( rng fk1) by FINSEQ_1: 30, A46;

          then

          reconsider r as FinSequence of NAT by XBOOLE_1: 1, FINSEQ_1:def 4;

          ( len fk1) = (( len fk) + ( len r)) by FINSEQ_1: 22, A46;

          then (k + 1) = (k + ( len r)) by A43, A33, A44;

          then

           Z: r = <*(r . 1)*> by FINSEQ_5: 14;

          then 1 <= ( len r) by FINSEQ_1: 39;

          then 1 in ( dom r) by FINSEQ_3: 25;

          then (r . 1) = (r /. 1) by PARTFUN1:def 6;

          hence (f . (k + 1)) in ( succ (f . k)) by A46, Z;

        end;

        (f . 0 ) = F3(0) by A33

        .= 0 by A24;

        then

        reconsider f as path of T by A42, Def13;

         A47:

        now

          let n;

          reconsider pn = (p . n) as Node of T;

          reconsider pln = (p . ( len pn)) as Node of T;

          pn c= pln by A39, A41;

          then ( Seg ( len pn)) c= ( dom pn) & ex t be FinSequence st pln = (pn ^ t) by FINSEQ_1:def 3, TREES_1: 1;

          

          then (pln | ( len pn)) = (pn | ( len pn)) by FINSEQ_6: 11

          .= pn by FINSEQ_1: 58;

          hence F3(len) = (p . n);

        end;

        f is complete

        proof

          let A, B, i;

          set aub = (A 'U' B);

          assume

           A48: aub in ( rng ((T . (f . i)) `1 ));

          defpred P2[ Nat] means $1 > i implies not B in ( rng ((T . (f . $1)) `1 )) & aub in ( rng ((T . (f . $1)) `1 )) & A in ( rng ((T . (f . $1)) `1 ));

          assume

           A49: for j st j > i holds ( not B in ( rng ((T . (f . j)) `1 )) or ex k st i < k & k < j & not A in ( rng ((T . (f . k)) `1 )));

           A50:

          now

            let k be Nat;

            assume

             A51: for n be Nat st n < k holds P2[n];

            thus P2[k]

            proof

              reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

              set fk = (T . (f . k1));

              assume

               A52: k > i;

              then k1 >= 1 by NAT_1: 25;

              then

              reconsider kk = (k1 - 1) as Element of NAT by NAT_1: 21;

              set fkk = (T . (f . kk));

              

               A53: (kk + 1) = k;

              then

               A54: kk >= i by NAT_1: 13, A52;

              per cases by A54, XXREAL_0: 1;

                suppose

                 A55: kk = i;

                per cases by A49, A52;

                  suppose

                   A56: not B in ( rng (fk `1 ));

                  (f . k) in ( succ (f . kk)) by Def13, A53;

                  then ex n be Nat st (f . k) = ((f . kk) ^ <*n*>) & ((f . kk) ^ <*n*>) in ( dom T);

                  then

                  reconsider fk as Element of ( compn fkk) by Th26;

                  B in ( rng (fk `1 )) or A in ( rng (fk `1 )) & aub in ( rng (fk `1 )) by Th25, A55, A48;

                  hence thesis by A56;

                end;

                  suppose ex m be Element of NAT st i < m & m < k1 & not A in ( rng ((T . (f . m)) `1 ));

                  hence thesis by NAT_1: 13, A55, A53;

                end;

              end;

                suppose

                 A57: kk > i;

                per cases by A49, A52;

                  suppose

                   A58: not B in ( rng (fk `1 ));

                  (f . k) in ( succ (f . kk)) by Def13, A53;

                  then ex n be Nat st (f . k) = ((f . kk) ^ <*n*>) & ((f . kk) ^ <*n*>) in ( dom T);

                  then

                  reconsider fk as Element of ( compn fkk) by Th26;

                  kk < k by XREAL_1: 146;

                  then aub in ( rng (fkk `1 )) by A51, A57;

                  then B in ( rng (fk `1 )) or A in ( rng (fk `1 )) & aub in ( rng (fk `1 )) by Th25;

                  hence thesis by A58;

                end;

                  suppose ex m be Element of NAT st i < m & m < k1 & not A in ( rng ((T . (f . m)) `1 ));

                  hence thesis by A51;

                end;

              end;

            end;

          end;

          

           A59: for j be Nat holds P2[j] from NAT_1:sch 4( A50);

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

          then ( rng (T . (f . i))) in YN & ( rng ((T . (f . i)) `1 )) c= ( rng (T . (f . i))) by XBOOLE_1: 7;

          then (aub is s-until) & aub in Tforms by HILBERT2:def 6, A48, TARSKI:def 4;

          then

           A60: aub in uns;

          then

          consider n be object such that

           A61: n in ( dom g) and

           A62: (g . n) = aub by A6, FUNCT_1:def 3;

          reconsider n as Element of NAT by A61;

          reconsider k = (n - 1) as Element of NAT by A61, FINSEQ_3: 25, NAT_1: 21;

          (k + 1) <= ( len g) by FINSEQ_3: 25, A61;

          then

           A63: k < ( card g) by NAT_1: 13;

          set mnk = ((m * (i + 1)) + k);

          (i + 1) > i & m >= 1 by NAT_1: 13, A60, NAT_1: 25;

          then ((i + 1) * m) > (i * 1) by XREAL_1: 97;

          then

           A64: ((m * (i + 1)) + k) > i by XREAL_1: 40;

          then

           A65: (mnk + 1) > i by NAT_1: 13;

          

           A66: ((mnk mod m) + 1) = ((k mod m) + 1) by NAT_D: 21

          .= (k + 1) by NAT_D: 24, A63, A8;

          reconsider t = (p . mnk), t1 = (p . (mnk + 1)) as Node of T;

          mnk <= ( len t) by A39;

          then

           A67: ( len t) > i by A64, XXREAL_0: 2;

          

           A68: aub is s-until by HILBERT2:def 6;

          (mnk + 1) <= ( len t1) by A39;

          then

           A69: ( len t1) > i by A65, XXREAL_0: 2;

          

           A70: t1 = F3(len) by A47

          .= (f . ( len t1)) by A33;

          t = F3(len) by A47

          .= (f . ( len t)) by A33;

          then (g . (k + 1)) in ( rng ((T . t) `1 )) by A67, A59, A62;

          then

           A71: ( rarg (g /. ((mnk mod m) + 1))) in ( rng ((T . t1) `1 )) by A66, A24;

          ( rarg (g /. ((mnk mod m) + 1))) = ( rarg aub) by A62, A61, PARTFUN1:def 6, A66

          .= B by Def1, A68;

          hence contradiction by A69, A59, A71, A70;

        end;

        hence thesis;

      end;

    end

    registration

      let P be consistent PNPair;

      cluster (P ^ ) -> satisfiable;

      coherence

      proof

        consider Q be object such that

         A1: Q in ( comp P) by XBOOLE_0:def 1;

        consider Pg be consistent PNPair such that Pg = Q and

         A2: Pg is_completion_of P by A1;

        

         A3: ( rng (P `1 )) c= ( rng (Pg `1 )) by A2;

        

         A4: ( rng (P `2 )) c= ( rng (Pg `2 )) by A2;

        reconsider Pg as consistent complete PNPair by A2, Th13;

        set T = the pnptree of Pg;

        set t = the complete path of T;

        defpred P[ Element of NAT , Element of ( bool props )] means $2 = { p where p be Element of l : p is simple & p in ( rng ((T . (t . $1)) `1 )) };

         A5:

        now

          let x be Element of NAT ;

          set y = { p where p be Element of l : p is simple & p in ( rng ((T . (t . x)) `1 )) };

          y c= props

          proof

            let z be object;

            assume z in y;

            then

            consider p be Element of l such that

             A6: p = z and

             A7: p is simple and p in ( rng ((T . (t . x)) `1 ));

            ex n st p = ( prop n) by A7, HILBERT2:def 8;

            hence z in props by LTLAXIO1:def 10, A6;

          end;

          then

          reconsider y as Element of ( bool props );

           P[x, y];

          hence ex y be Element of ( bool props ) st P[x, y];

        end;

        consider M be sequence of ( bool props ) such that

         A8: for n be Element of NAT holds P[n, (M . n) qua Element of ( bool props )] from FUNCT_2:sch 3( A5);

        set s = ( SAT M);

        defpred P1[ Element of l] means for i be Element of NAT st $1 in ( rng (T . (t . i))) holds ((s . [i, $1]) = 1 iff $1 in ( rng ((T . (t . i)) `1 )));

         A9:

        now

          let i be Element of NAT , p;

          assume

           A10: p is simple;

          then

           A11: ex n st p = ( prop n) by HILBERT2:def 8;

          

           A12: (M . i) = { q where q be Element of l : q is simple & q in ( rng ((T . (t . i)) `1 )) } by A8;

          hereby

            assume (s . [i, p]) = 1;

            then p in (M . i) by A11, LTLAXIO1:def 11;

            then ex q be Element of l st p = q & (q is simple) & q in ( rng ((T . (t . i)) `1 )) by A12;

            hence p in ( rng ((T . (t . i)) `1 ));

          end;

          assume p in ( rng ((T . (t . i)) `1 ));

          then p in (M . i) by A12, A10;

          hence (s . [i, p]) = 1 by LTLAXIO1:def 11, A11;

        end;

         A13:

        now

          let n;

          ( prop n) is simple by HILBERT2:def 8;

          hence P1[( prop n)] by A9;

        end;

         A14:

        now

          let r, q;

          set ruq = (r 'U' q);

          assume that

           A15: P1[r] and

           A16: P1[q];

          thus P1[ruq]

          proof

            let i be Element of NAT ;

            defpred P2[ Nat] means not (( SAT M) . [$1, q]) = 1;

            set Q = (T . (t . i));

            defpred P3[ Element of NAT ] means ex k st i < k & k < $1 & not (( SAT M) . [k, r]) = 1;

            assume

             A17: ruq in ( rng Q);

            hereby

              assume

               A18: (s . [i, ruq]) = 1;

              assume not (r 'U' q) in ( rng ((T . (t . i)) `1 ));

              then

               A19: (r 'U' q) in ( rng ((T . (t . i)) `2 )) by A17, XBOOLE_0:def 3;

              consider j such that

               A20: j > i & (s . [j, q]) = 1 & for k st i < k & k < j holds (s . [k, r]) = 1 by A18, Th5;

              per cases by Th30, A19, A20;

                suppose q in ( rng ((T . (t . j)) `2 ));

                then not q in ( rng ((T . (t . j)) `1 )) & q in ( rng (T . (t . j))) by LTLAXIO3: 30, XBOOLE_0: 3, XBOOLE_0:def 3;

                hence contradiction by A16, A20;

              end;

                suppose ex k st i < k & k < j & r in ( rng ((T . (t . k)) `2 ));

                then

                consider k such that

                 A21: i < k & k < j and

                 A22: r in ( rng ((T . (t . k)) `2 ));

                 not r in ( rng ((T . (t . k)) `1 )) & r in ( rng (T . (t . k))) by LTLAXIO3: 30, A22, XBOOLE_0: 3, XBOOLE_0:def 3;

                then not (s . [k, r]) = 1 by A15;

                hence contradiction by A21, A20;

              end;

            end;

            assume ruq in ( rng (Q `1 ));

            then

            consider j such that

             A23: j > i and

             A24: q in ( rng ((T . (t . j)) `1 )) and

             A25: for k st i < k & k < j holds r in ( rng ((T . (t . k)) `1 )) by Def14;

             A26:

            now

              let k;

              assume i < k & k < j;

              then

               A27: r in ( rng ((T . (t . k)) `1 )) by A25;

              then r in ( rng (T . (t . k))) by XBOOLE_0:def 3;

              hence (s . [k, r]) = 1 by A15, A27;

            end;

            q in ( rng (T . (t . j))) by A24, XBOOLE_0:def 3;

            then (s . [j, q]) = 1 by A24, A16;

            hence (s . [i, ruq]) = 1 by A26, Th5, A23;

          end;

          thus P1[(r => q)]

          proof

            let i be Element of NAT ;

            set Q = (T . (t . i));

            assume

             A28: (r => q) in ( rng Q);

            

             A29: ( tau ( rng Q)) = ( rng Q) by LTLAXIO3:def 11;

            then

             A30: r in ( rng Q) by A28, LTLAXIO3: 19;

            

             A31: q in ( rng Q) by A28, LTLAXIO3: 19, A29;

            

             A32: (s . [i, r]) = 1 or (s . [i, r]) = 0 by XBOOLEAN:def 3;

            hereby

              assume (s . [i, (r => q)]) = 1;

              then ((s . [i, r]) => (s . [i, q])) = 1 by LTLAXIO1:def 11;

              then not r in ( rng (Q `1 )) or q in ( rng (Q `1 )) by A32, A15, A16, A30, A31;

              then r in ( rng (Q `2 )) or q in ( rng (Q `1 )) by A30, XBOOLE_0:def 3;

              hence (r => q) in ( rng (Q `1 )) by LTLAXIO3: 33, A28, A30, A31;

            end;

            assume (r => q) in ( rng (Q `1 ));

            then r in ( rng (Q `2 )) or q in ( rng (Q `1 )) by LTLAXIO3: 33, A28, A30, A31;

            then not r in ( rng (Q `1 )) or q in ( rng (Q `1 )) by XBOOLE_0: 3, LTLAXIO3: 30;

            then ((s . [i, r]) => (s . [i, q])) = 1 by A15, A16, A30, A31, A32;

            hence (s . [i, (r => q)]) = 1 by LTLAXIO1:def 11;

          end;

        end;

        

         A33: P1[ TFALSUM ] by LTLAXIO3: 32, LTLAXIO1:def 11;

        

         A34: for A holds P1[A] from HILBERT2:sch 2( A33, A13, A14);

        

         A35: (T . (t . 0 )) = (T . {} ) by Def13

        .= Pg by Def11;

        now

          let i;

          set nA = (( nega (P `2 )) /. i), A = ((P `2 ) /. i);

          assume

           A36: i in ( dom ( nega (P `2 )));

          ( len ( nega (P `2 ))) = ( len (P `2 )) by LTLAXIO2:def 4;

          then

           A37: i in ( dom (P `2 )) by A36, FINSEQ_3: 29;

          then ((P `2 ) . i) in ( rng (P `2 )) by FUNCT_1: 3;

          then A in ( rng (P `2 )) by PARTFUN1:def 6, A37;

          then

           A38: A in ( rng (Pg `2 )) & not A in ( rng (Pg `1 )) by A4, LTLAXIO3: 30, XBOOLE_0: 3;

          ( rng (Pg `2 )) c= ( rng Pg) by XBOOLE_1: 7;

          then

           A39: not (s . [ 0 , A]) = 1 by A38, A35, A34;

          

          thus (s . [ 0 , nA]) = (s . [ 0 , ( 'not' A)]) by LTLAXIO2: 8, A37

          .= 1 by A39, XBOOLEAN:def 3, LTLAXIO1: 5;

        end;

        then

         A40: (s . [ 0 , kon(nega)]) = 1 by Th6;

        now

          let i;

          set A = ((P `1 ) /. i);

          assume i in ( dom (P `1 ));

          then A in ( rng (P `1 )) by PARTFUN2: 2;

          then ( rng (Pg `1 )) c= ( rng Pg) & A in ( rng (Pg `1 )) by XBOOLE_1: 7, A3;

          hence (s . [ 0 , A]) = 1 by A35, A34;

        end;

        then (s . [ 0 , kon(`1)]) = 1 by Th6;

        then (s . [ 0 , (P ^ )]) = 1 by A40, LTLAXIO1: 7;

        hence (P ^ ) is satisfiable;

      end;

    end

    ::$Notion-Name

    theorem :: LTLAXIO4:33

    F |= A implies F |- A

    proof

       A1:

      now

        let p;

        set PN = [( <*> l), <*p*>], tv = TVERUM ;

        assume ( {} l) |= p;

        then not (tv '&&' ( 'not' p)) is satisfiable by Th3, Th4;

        then not (PN ^ ) is satisfiable by Th7;

        then PN is Inconsistent;

        then ( {} l) |- ( 'not' (PN ^ ));

        then

         A2: ( {} l) |- ( 'not' (tv '&&' ( 'not' p))) by Th7;

        (( 'not' (tv '&&' ( 'not' p))) => p) is ctaut by LTLAXIO2: 38;

        then (( 'not' (tv '&&' ( 'not' p))) => p) in LTL_axioms by LTLAXIO1:def 17;

        then ( {} l) |- (( 'not' (tv '&&' ( 'not' p))) => p) by LTLAXIO1: 42;

        hence ( {} l) |- p by LTLAXIO1: 43, A2;

      end;

      assume

       A3: F |= A;

      now

        consider f be FinSequence such that

         A4: ( rng f) = F and f is one-to-one by FINSEQ_4: 58;

        reconsider f as FinSequence of l by A4, FINSEQ_1:def 4;

        assume

         A5: not F is empty;

        then

         A6: 1 <= ( len f) by RELAT_1: 38, A4, FINSEQ_1: 20;

        then 1 <= ( len ( impg (f,A))) by LTLAXIO2:def 3;

        then

         A7: (( impg (f,A)) /. 1) = (( impg (f,A)) . 1) by FINSEQ_4: 15;

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies ( rng (f /^ $1)) |= (( impg (f,A)) /. $1);

        

         a8: 1 in ( dom f) by A6, FINSEQ_3: 25;

        ( rng (f | 1)) = ( rng <*(f . 1)*>) by FINSEQ_5: 20, RELAT_1: 38, A4, A5

        .= ( rng <*(f /. 1)*>) by a8, PARTFUN1:def 6;

        

        then

         A8: (( rng (f /^ 1)) \/ {(f /. 1)}) = (( rng (f | 1)) \/ ( rng (f /^ 1))) by FINSEQ_1: 38

        .= ( rng ((f | 1) ^ (f /^ 1))) by FINSEQ_1: 31

        .= ( rng f) by RFINSEQ: 8;

        

         A9: ( len ( impg (f,A))) = ( len f) by A6, LTLAXIO2:def 3;

         A10:

        now

          let i;

          

           A11: i in NAT by ORDINAL1:def 12;

          assume

           A12: P[i];

          thus P[(i + 1)]

          proof

            assume that

             A13: 1 <= (i + 1) and

             A14: (i + 1) <= ( len f);

            per cases by NAT_1: 25;

              suppose

               A15: i = 0 ;

              (( 'G' (f /. 1)) => A) = (( impg (f,A)) . 1) by LTLAXIO2:def 3, A6

              .= (( impg (f,A)) /. 1) by FINSEQ_4: 15, A9, A6;

              hence ( rng (f /^ (i + 1))) |= (( impg (f,A)) /. (i + 1)) by A8, A4, A3, LTLAXIO1: 30, A15;

            end;

              suppose

               A16: 1 <= i;

              (i + 1) in ( dom f) by FINSEQ_3: 25, A13, A14;

              then ( rng ( <*(f /. (i + 1))*> ^ (f /^ (i + 1)))) |= (( impg (f,A)) /. i) by A12, A16, NAT_1: 13, A14, FINSEQ_5: 31;

              then (( rng <*(f /. (i + 1))*>) \/ ( rng (f /^ (i + 1)))) |= (( impg (f,A)) /. i) by FINSEQ_1: 31;

              then

               A17: (( rng (f /^ (i + 1))) \/ {(f /. (i + 1))}) |= (( impg (f,A)) /. i) by FINSEQ_1: 38;

              

               A18: i < ( len f) by NAT_1: 13, A14;

              (( impg (f,A)) /. (i + 1)) = (( impg (f,A)) . (i + 1)) by FINSEQ_4: 15, A13, A14, A9

              .= (( 'G' (f /. (i + 1))) => (( impg (f,A)) /. i)) by LTLAXIO2:def 3, A16, A18, A11;

              hence ( rng (f /^ (i + 1))) |= (( impg (f,A)) /. (i + 1)) by A17, LTLAXIO1: 30;

            end;

          end;

        end;

        

         A19: P[ 0 ];

        for i holds P[i] from NAT_1:sch 2( A19, A10);

        then ( rng (f /^ ( len f))) |= (( impg (f,A)) /. ( len f)) by A6;

        then ( {} l) |= (( impg (f,A)) /. ( len f)) by RFINSEQ: 27, RELAT_1: 38;

        then

         A20: ( {} l) |- (( impg (f,A)) /. ( len f)) by A1;

        defpred P[ Nat] means $1 < ( len f) implies ( rng (f /^ (( len f) -' $1))) |- (( impg (f,A)) /. (( len f) -' $1));

         A21:

        now

          let i;

          assume

           A22: P[i];

          thus P[(i + 1)]

          proof

            set j = (( len f) -' (i + 1));

            assume

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

            then

             A24: ((i + 1) + ( - (i + 1))) < (( len f) + ( - (i + 1))) by XREAL_1: 8;

            then

             A25: j = (( len f) - (i + 1)) by XREAL_0:def 2;

            then

             A26: 1 <= j by NAT_1: 25, A24;

            i < ( len f) by A23, NAT_1: 12;

            then (( len f) + ( - i)) > (i + ( - i)) by XREAL_1: 8;

            then

             A27: (( len f) - i) > 0 ;

            

             A28: (j + 1) = ((( len f) - (i + 1)) + 1) by XREAL_0:def 2, A24

            .= (( len f) -' i) by XREAL_0:def 2, A27;

            

             A29: (( len f) + ( - i)) <= ( len f) by XREAL_1: 32;

            then (j + 1) <= ( len f) by A25;

            then

             A30: j < ( len f) by NAT_1: 16, XXREAL_0: 2;

            (j + 1) <= ( len ( impg (f,A))) by A29, A25, LTLAXIO2:def 3;

            

            then (( impg (f,A)) /. (( len f) -' i)) = (( impg (f,A)) . (j + 1)) by A28, FINSEQ_4: 15, NAT_1: 11

            .= (( 'G' (f /. (j + 1))) => (( impg (f,A)) /. j)) by LTLAXIO2:def 3, A26, A30;

            then (( rng (f /^ (( len f) -' i))) \/ {(f /. (j + 1))}) |- (( impg (f,A)) /. j) by LTLAXIO1: 59, A22, NAT_1: 12, A23;

            then (( rng <*(f /. (j + 1))*>) \/ ( rng (f /^ (( len f) -' i)))) |- (( impg (f,A)) /. j) by FINSEQ_1: 38;

            then

             A31: ( rng ( <*(f /. (j + 1))*> ^ (f /^ (( len f) -' i)))) |- (( impg (f,A)) /. j) by FINSEQ_1: 31;

            (j + 1) in ( dom f) by FINSEQ_3: 25, NAT_1: 11, A29, A25;

            hence ( rng (f /^ j)) |- (( impg (f,A)) /. j) by A31, FINSEQ_5: 31, A28;

          end;

        end;

        (1 + ( - 1)) <= (( len f) + ( - 1)) by XREAL_1: 6, FINSEQ_1: 20, RELAT_1: 38, A4, A5;

        then (( len f) -' 1) = (( len f) - 1) by XREAL_0:def 2;

        then

        reconsider i = (( len f) - 1) as Element of NAT ;

        

         A32: (( len f) + ( - 1)) < ( len f) by XREAL_1: 37;

        (( len f) - 0 ) >= 1 by RELAT_1: 38, A4, A5, FINSEQ_1: 20;

        then (( len f) -' 0 ) = ( len f) by XREAL_0:def 2;

        then

         A33: P[ 0 ] by A20, RELAT_1: 38, RFINSEQ: 27;

        

         A34: for i holds P[i] from NAT_1:sch 2( A33, A21);

        (( len f) -' i) = (( len f) - i) by XREAL_0:def 2

        .= 1;

        then ( rng (f /^ 1)) |- (( impg (f,A)) /. 1) by A34, A32;

        then ( rng (f /^ 1)) |- (( 'G' (f /. 1)) => A) by LTLAXIO2:def 3, A7, A6;

        hence F |- A by A4, A8, LTLAXIO1: 59;

      end;

      hence F |- A by A1, A3;

    end;