ltlaxio3.miz



    begin

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

n for Element of NAT ,

X for Subset of LTLB_WFF ,

g for Function of LTLB_WFF , BOOLEAN ,

x,y for set;

    set l = LTLB_WFF ;

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

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

    theorem :: LTLAXIO3:1

    

     Th1: for X be non empty set, t be FinSequence of X, k be Nat st (k + 1) <= ( len t) holds (t /^ k) = ( <*(t . (k + 1))*> ^ (t /^ (k + 1)))

    proof

      let X be non empty set, t be FinSequence of X, k be Nat;

      

       A1: ((k + 1) -' 1) = ((k + 1) - 1) by XREAL_0:def 2

      .= k;

      assume (k + 1) <= ( len t);

      

      then t = (((t | ((k + 1) -' 1)) ^ <*(t . (k + 1))*>) ^ (t /^ (k + 1))) by NAT_1: 11, FINSEQ_5: 84

      .= ((t | k) ^ ( <*(t . (k + 1))*> ^ (t /^ (k + 1)))) by A1, FINSEQ_1: 32;

      then ((t | k) ^ (t /^ k)) = ((t | k) ^ ( <*(t . (k + 1))*> ^ (t /^ (k + 1)))) by RFINSEQ: 8;

      hence (t /^ k) = ( <*(t . (k + 1))*> ^ (t /^ (k + 1))) by FINSEQ_1: 33;

    end;

    theorem :: LTLAXIO3:2

    

     Th2: ( NAT --> {} ) is LTLModel

    proof

      set M = ( NAT --> {} );

       A1:

      now

        let x be object;

        assume x in NAT ;

        then

         A2: (M . x) = {} by FUNCOP_1: 7;

         {} c= props ;

        hence (M . x) in ( bool props ) by A2;

      end;

      ( dom M) = NAT by FUNCOP_1: 13;

      hence thesis by A1, FUNCT_2: 3;

    end;

    definition

      let X;

      :: LTLAXIO3:def1

      attr X is without_implication means for p st p in X holds not p is conditional;

    end

    definition

      let D be set;

      :: LTLAXIO3:def2

      func D ** -> set means

      : Def2: for x holds (x in it iff x is one-to-one FinSequence of D);

      existence

      proof

        defpred S2[ object] means $1 is one-to-one FinSequence of D;

        consider X be set such that

         A1: for x be object holds (x in X iff x in ( bool [: NAT , D:]) & S2[x]) from XBOOLE_0:sch 1;

        take X;

        let x be set;

        thus x in X implies x is one-to-one FinSequence of D by A1;

        assume x is one-to-one FinSequence of D;

        then

        reconsider p = x as one-to-one FinSequence of D;

        p c= [: NAT , D:];

        hence x in X by A1;

      end;

      uniqueness

      proof

        let D1,D2 be set;

        assume that

         A2: for x be set holds (x in D1 iff x is one-to-one FinSequence of D) and

         A3: for x be set holds (x in D2 iff x is one-to-one FinSequence of D);

        now

          let x be object;

          thus x in D1 implies x in D2

          proof

            assume x in D1;

            then x is one-to-one FinSequence of D by A2;

            hence x in D2 by A3;

          end;

          assume x in D2;

          then x is one-to-one FinSequence of D by A3;

          hence x in D1 by A2;

        end;

        hence D1 = D2 by TARSKI: 2;

      end;

    end

    registration

      let D be set;

      cluster (D ** ) -> non empty;

      coherence

      proof

         the one-to-one FinSequence of D in (D ** ) by Def2;

        hence thesis;

      end;

    end

    registration

      let D be finite set;

      cluster (D ** ) -> finite;

      coherence

      proof

        set seg = ( Seg ( card D));

        

         A1: (D ** ) c= ( PFuncs (seg,D))

        proof

          let x be object;

          assume x in (D ** );

          then

          reconsider f = x as one-to-one FinSequence of D by Def2;

          

           A2: ( dom f) c= seg

          proof

            let x be object;

            assume

             A3: x in ( dom f);

            then

            reconsider x1 = x as Nat;

            

             A4: x in ( Seg ( len f)) by A3, FINSEQ_1:def 3;

            then

             A5: 1 <= x1 by FINSEQ_1: 1;

            x1 <= ( len f) by A4, FINSEQ_1: 1;

            then

             A6: x1 <= ( card ( rng f)) by FINSEQ_4: 62;

            ( Segm ( card ( rng f))) c= ( Segm ( card D)) by CARD_1: 11;

            then ( card ( rng f)) <= ( card D) by NAT_1: 39;

            then x1 <= ( card D) by XXREAL_0: 2, A6;

            hence thesis by A5;

          end;

          ( rng f) c= D;

          hence thesis by A2, PARTFUN1:def 3;

        end;

        ( PFuncs (seg,D)) is finite by PRE_POLY: 17;

        hence thesis by A1;

      end;

    end

    theorem :: LTLAXIO3:3

    

     Th3: for D1,D2 be set st D1 c= D2 holds (D1 ** ) c= (D2 ** )

    proof

      let D1,D2 be set;

      assume

       A1: D1 c= D2;

      let x be object;

      assume x in (D1 ** );

      then

      reconsider p = x as one-to-one FinSequence of D1 by Def2;

      ( rng p) c= D2 by A1;

      then x is one-to-one FinSequence of D2 by FINSEQ_1:def 4;

      hence x in (D2 ** ) by Def2;

    end;

    definition

      let a1 be set;

      let a2 be Subset of a1;

      :: original: **

      redefine

      func a2 ** -> non empty Subset of (a1 ** ) ;

      coherence by Th3;

    end

    theorem :: LTLAXIO3:4

    

     Th4: for F,G be one-to-one FinSequence st ( rng F) misses ( rng G) holds (F ^ G) is one-to-one

    proof

      let F,G be one-to-one FinSequence;

      assume

       A1: ( rng F) misses ( rng G);

      reconsider FG = (F ^ G) as Function of ( dom (F ^ G)), ( rng (F ^ G)) by FUNCT_2: 1;

      

       A2: FG is onto by FUNCT_2:def 3;

      ( card ( dom (F ^ G))) = ( card ( Seg (( len F) + ( len G)))) by FINSEQ_1:def 7

      .= (( len F) + ( len G)) by FINSEQ_1: 57

      .= (( card ( rng F)) + ( len G)) by FINSEQ_4: 62

      .= (( card ( rng F)) + ( card ( rng G))) by FINSEQ_4: 62

      .= ( card (( rng F) \/ ( rng G))) by A1, CARD_2: 40

      .= ( card ( rng (F ^ G))) by FINSEQ_1: 31;

      hence (F ^ G) is one-to-one by A2, FINSEQ_4: 63;

    end;

    definition

      let X be set;

      let f,g be one-to-one FinSequence of X;

      assume

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

      :: LTLAXIO3:def3

      func f ^^ g -> one-to-one FinSequence of X equals

      : Def3: (f ^ g);

      coherence by Th4, A1;

    end

    begin

    definition

      :: LTLAXIO3:def4

      func tau1 -> Function of LTLB_WFF , ( bool LTLB_WFF ) means

      : Def4: (it . TFALSUM ) = { TFALSUM } & (it . ( prop n)) = {( prop n)} & (it . (A => B)) = (( {(A => B)} \/ (it . A)) \/ (it . B)) & (it . (A 'U' B)) = {(A 'U' B)};

      existence

      proof

        set bltl = ( bool l);

        defpred P1[ Element of l, Element of l, set, set, set] means $5 = {($1 'U' $2)};

        deffunc F2( Element of NAT ) = {( prop $1)};

        defpred P3[ Element of l, Element of l, set, set, set] means ($3 is Element of bltl & $4 is Element of bltl implies ex a,b,c be Element of bltl st a = $3 & b = $4 & c = $5 & c = (( {($1 => $2)} \/ $3) \/ $4)) & ( not $3 is Element of bltl or not $4 is Element of bltl implies $5 = ( {} l));

        

         A1: for A, B holds for x,y be set holds ex z be set st P3[A, B, x, y, z]

        proof

          let A, B, x, y;

          per cases ;

            suppose that

             A2: x is Element of bltl and

             A3: y is Element of bltl;

            reconsider b = y as Element of bltl by A3;

            reconsider a = x as Element of bltl by A2;

            consider z be set such that

             A4: z = (( {(A => B)} \/ a) \/ b);

            take z;

            thus thesis by A4;

          end;

            suppose not x is Element of bltl or not y is Element of bltl;

            hence thesis;

          end;

        end;

        

         A5: for A, B holds for x,y be set holds ex z be set st P1[A, B, x, y, z];

        

         A6: for p, q holds for a,b,c,d be set st P1[p, q, a, b, c] & P1[p, q, a, b, d] holds c = d;

        

         A7: for p, q holds for a,b,c,d be set st P3[p, q, a, b, c] & P3[p, q, a, b, d] holds c = d;

        consider val be ManySortedSet of l such that

         A8: (val . TFALSUM ) = { TFALSUM } & (for n holds (val . ( prop n)) = F2(n)) & for p, q holds P1[p, q, (val . p), (val . q), (val . (p 'U' q))] & P3[p, q, (val . p), (val . q), (val . (p => q))] from HILBERT2:sch 3( A5, A1, A6, A7);

         A9:

        now

           A10:

          now

            let A, B;

            

             A11: P3[A, B, (val . A), (val . B), (val . (A => B))] by A8;

            per cases ;

              suppose (val . A) is Element of bltl & (val . B) is Element of bltl;

              thus (val . (A => B)) in bltl by A11;

            end;

              suppose not ((val . A) is Element of bltl & (val . B) is Element of bltl);

              then (val . (A => B)) = ( {} l) by A8;

              hence (val . (A => B)) in bltl;

            end;

          end;

          let x be object;

          assume x in l;

          then

          reconsider x1 = x as Element of l;

           A12:

          now

            let n;

            (val . ( prop n)) = {( prop n)} by A8;

            hence (val . ( prop n)) in bltl;

          end;

           A13:

          now

            let A, B;

            (val . (A 'U' B)) = {(A 'U' B)} by A8;

            hence (val . (A 'U' B)) in bltl;

          end;

          per cases by LTLAXIO1: 4;

            suppose x1 = TFALSUM ;

            hence (val . x) in bltl by A8;

          end;

            suppose ex n be Element of NAT st x1 = ( prop n);

            hence (val . x) in bltl by A12;

          end;

            suppose ex p, q st x1 = (p 'U' q);

            hence (val . x) in bltl by A13;

          end;

            suppose ex p, q st x1 = (p => q);

            hence (val . x) in bltl by A10;

          end;

        end;

        ( dom val) = l by PARTFUN1:def 2;

        then

        reconsider val as Function of l, bltl by A9, FUNCT_2: 3;

        take val;

        now

          let A, B;

           P3[A, B, (val . A), (val . B), (val . (A => B))] by A8;

          hence (val . (A => B)) = (( {(A => B)} \/ (val . A)) \/ (val . B));

        end;

        hence thesis by A8;

      end;

      uniqueness

      proof

        set bltl = ( bool l);

        let v1,v2 be Function of l, bltl;

        assume

         A14: (v1 . TFALSUM ) = { TFALSUM } & (v1 . ( prop n)) = {( prop n)} & (v1 . (A => B)) = (( {(A => B)} \/ (v1 . A)) \/ (v1 . B)) & (v1 . (A 'U' B)) = {(A 'U' B)};

        assume

         A15: (v2 . TFALSUM ) = { TFALSUM } & (v2 . ( prop n)) = {( prop n)} & (v2 . (A => B)) = (( {(A => B)} \/ (v2 . A)) \/ (v2 . B)) & (v2 . (A 'U' B)) = {(A 'U' B)};

        thus v1 = v2

        proof

          defpred P1[ Element of l] means (v1 . $1) = (v2 . $1);

          

           A16: for n holds P1[( prop n)]

          proof

            let n;

            (v1 . ( prop n)) = {( prop n)} by A14

            .= (v2 . ( prop n)) by A15;

            hence P1[( prop n)];

          end;

          

           A17: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

          proof

            let r, s;

            assume

             A18: P1[r] & P1[s];

            

             A19: (v1 . (r 'U' s)) = {(r 'U' s)} by A14

            .= (v2 . (r 'U' s)) by A15;

            (v1 . (r => s)) = (( {(r => s)} \/ (v1 . r)) \/ (v1 . s)) by A14

            .= (v2 . (r => s)) by A15, A18;

            hence thesis by A19;

          end;

          

           A20: P1[ TFALSUM ] by A14, A15;

          for x be Element of l holds P1[x] from HILBERT2:sch 2( A20, A16, A17);

          then

           A21: for x be Element of l st x in ( dom v1) holds P1[x];

          ( dom v1) = l by FUNCT_2:def 1

          .= ( dom v2) by FUNCT_2:def 1;

          hence thesis by A21, PARTFUN1: 5;

        end;

      end;

    end

    theorem :: LTLAXIO3:5

    

     Th5: not A is conditional implies ( tau1 . A) = {A}

    proof

      assume not A is conditional;

      then A is conjunctive or A is simple or A = TFALSUM by HILBERT2: 9;

      then ex r, s st A = (r 'U' s) or ex n st A = ( prop n) or A = TFALSUM by HILBERT2:def 8, HILBERT2:def 6;

      hence thesis by Def4;

    end;

    theorem :: LTLAXIO3:6

    

     Th6: p in ( tau1 . p)

    proof

      defpred P1[ Element of l] means $1 in ( tau1 . $1);

      

       A1: for n holds P1[( prop n)]

      proof

        let n;

        ( tau1 . ( prop n)) = {( prop n)} by Def4;

        hence thesis by TARSKI:def 1;

      end;

      

       A2: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that P1[r] and P1[s];

        ( tau1 . (r 'U' s)) = {(r 'U' s)} by Def4;

        hence P1[(r 'U' s)] by TARSKI:def 1;

        ( tau1 . (r => s)) = (( {(r => s)} \/ ( tau1 . r)) \/ ( tau1 . s)) by Def4;

        then {(r => s)} c= ( {(r => s)} \/ ( tau1 . r)) & ( {(r => s)} \/ ( tau1 . r)) c= ( tau1 . (r => s)) by XBOOLE_1: 7;

        hence P1[(r => s)] by ZFMISC_1: 31;

      end;

      ( tau1 . TFALSUM ) = { TFALSUM } by Def4;

      then

       A3: P1[ TFALSUM ] by TARSKI:def 1;

      for p holds P1[p] from HILBERT2:sch 2( A3, A1, A2);

      hence thesis;

    end;

    registration

      let p;

      cluster ( tau1 . p) -> non empty finite;

      coherence

      proof

        thus ( tau1 . p) is non empty by Th6;

        defpred P1[ Element of l] means ( tau1 . $1) is finite;

        

         A1: for n holds P1[( prop n)]

        proof

          let n;

          ( tau1 . ( prop n)) = {( prop n)} by Def4;

          hence thesis;

        end;

        

         A2: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

        proof

          let r, s;

          assume

           A3: P1[r] & P1[s];

          ( tau1 . (r 'U' s)) = {(r 'U' s)} by Def4;

          hence P1[(r 'U' s)];

          ( tau1 . (r => s)) = (( {(r => s)} \/ ( tau1 . r)) \/ ( tau1 . s)) by Def4;

          hence P1[(r => s)] by A3;

        end;

        

         A4: P1[ TFALSUM ] by Def4;

        for p holds P1[p] from HILBERT2:sch 2( A4, A1, A2);

        hence ( tau1 . p) is finite;

      end;

    end

    theorem :: LTLAXIO3:7

    

     Th7: (p => q) in ( tau1 . r) implies p in ( tau1 . r) & q in ( tau1 . r)

    proof

      defpred P1[ Element of l] means (p => q) in ( tau1 . $1) implies p in ( tau1 . $1) & q in ( tau1 . $1);

      

       A1: for n holds P1[( prop n)]

      proof

        let n;

        set pr = ( prop n);

        assume (p => q) in ( tau1 . pr);

        then (p => q) in {pr} by Def4;

        then (p => q) = pr by TARSKI:def 1;

        hence p in ( tau1 . pr) & q in ( tau1 . pr) by HILBERT2: 26;

      end;

      

       A2: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that

         A3: P1[r] and

         A4: P1[s];

        thus P1[(r 'U' s)]

        proof

          set f = (r 'U' s);

          assume (p => q) in ( tau1 . f);

          then (p => q) in {f} by Def4;

          then (p => q) = f by TARSKI:def 1;

          hence p in ( tau1 . f) & q in ( tau1 . f) by HILBERT2: 22;

        end;

        thus P1[(r => s)]

        proof

          set f = (r => s);

          

           A5: ( tau1 . f) = (( {f} \/ ( tau1 . r)) \/ ( tau1 . s)) by Def4;

          then

           A6: ( tau1 . s) c= ( tau1 . f) by XBOOLE_1: 7;

          ( tau1 . r) c= ( {f} \/ ( tau1 . r)) & ( {f} \/ ( tau1 . r)) c= ( tau1 . f) by XBOOLE_1: 7, A5;

          then

           A7: ( tau1 . r) c= ( tau1 . f);

          assume

           A8: (p => q) in ( tau1 . f);

          per cases by A8, A5, XBOOLE_0:def 3;

            suppose

             A9: (p => q) in ( {f} \/ ( tau1 . r));

            per cases by A9, XBOOLE_0:def 3;

              suppose (p => q) in {f};

              then

               A10: (p => q) = f by TARSKI:def 1;

              then

               A11: p = r by HILBERT2: 20;

              r in ( tau1 . r) by Th6;

              hence p in ( tau1 . f) by A11, A7;

              

               A12: q = s by A10, HILBERT2: 20;

              s in ( tau1 . s) by Th6;

              hence q in ( tau1 . f) by A12, A6;

            end;

              suppose (p => q) in ( tau1 . r);

              hence p in ( tau1 . f) & q in ( tau1 . f) by A3, A7;

            end;

          end;

            suppose (p => q) in ( tau1 . s);

            hence p in ( tau1 . f) & q in ( tau1 . f) by A4, A6;

          end;

        end;

      end;

      

       A13: P1[ TFALSUM ]

      proof

        set f = TFALSUM ;

        assume (p => q) in ( tau1 . f);

        then (p => q) in {f} by Def4;

        then (p => q) = f by TARSKI:def 1;

        hence p in ( tau1 . f) & q in ( tau1 . f) by HILBERT2: 25;

      end;

      for p holds P1[p] from HILBERT2:sch 2( A13, A1, A2);

      hence thesis;

    end;

    theorem :: LTLAXIO3:8

    

     Th8: p in ( tau1 . q) implies ( tau1 . p) c= ( tau1 . q)

    proof

      defpred P1[ Element of l] means $1 in ( tau1 . q) implies ( tau1 . $1) c= ( tau1 . q);

      

       A1: for n holds P1[( prop n)]

      proof

        let n;

        set pr = ( prop n);

        assume

         A2: pr in ( tau1 . q);

        let x be object;

        assume x in ( tau1 . pr);

        then x in {pr} by Def4;

        hence x in ( tau1 . q) by TARSKI:def 1, A2;

      end;

      

       A3: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that

         A4: P1[r] and

         A5: P1[s];

        thus P1[(r 'U' s)]

        proof

          set f = (r 'U' s);

          assume

           A6: f in ( tau1 . q);

          let x be object;

          assume x in ( tau1 . f);

          then x in {f} by Def4;

          hence x in ( tau1 . q) by TARSKI:def 1, A6;

        end;

        thus P1[(r => s)]

        proof

          set f = (r => s);

          assume

           A7: f in ( tau1 . q);

          then {f} c= ( tau1 . q) by ZFMISC_1: 31;

          then ( {f} \/ ( tau1 . r)) c= ( tau1 . q) by XBOOLE_1: 8, A7, Th7, A4;

          then

           A8: (( {f} \/ ( tau1 . r)) \/ ( tau1 . s)) c= ( tau1 . q) by XBOOLE_1: 8, A7, Th7, A5;

          let x be object;

          assume x in ( tau1 . f);

          then x in (( {f} \/ ( tau1 . r)) \/ ( tau1 . s)) by Def4;

          hence x in ( tau1 . q) by A8;

        end;

      end;

      

       A9: P1[ TFALSUM ]

      proof

        set f = TFALSUM ;

        assume

         A10: f in ( tau1 . q);

        let x be object;

        assume x in ( tau1 . f);

        then x in {f} by Def4;

        hence x in ( tau1 . q) by TARSKI:def 1, A10;

      end;

      for p holds P1[p] from HILBERT2:sch 2( A9, A1, A3);

      hence thesis;

    end;

    theorem :: LTLAXIO3:9

    

     Th9: (p 'U' q) in ( tau1 . ( 'not' A)) implies (p 'U' q) in ( tau1 . A)

    proof

      set a = (p 'U' q), na = ( 'not' A), f = TFALSUM ;

      

       A1: a <> (A => f) by HILBERT2: 22;

      assume a in ( tau1 . na);

      then a in (( {(A => f)} \/ ( tau1 . A)) \/ ( tau1 . f)) by Def4;

      then

       A2: a in ( {(A => f)} \/ ( tau1 . A)) or a in ( tau1 . f) by XBOOLE_0:def 3;

      a <> f by HILBERT2: 23;

      then not a in {f} by TARSKI:def 1;

      then a in {(A => f)} or a in ( tau1 . A) by A2, Def4, XBOOLE_0:def 3;

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: LTLAXIO3:10

    

     Th10: (p 'U' q) in ( tau1 . (A '&&' B)) implies ((p 'U' q) in ( tau1 . A) or (p 'U' q) in ( tau1 . B))

    proof

      set a = (p 'U' q), nb = ( 'not' B);

      assume a in ( tau1 . (A '&&' B));

      then a in ( tau1 . (A => nb)) by Th9;

      then a in (( {(A => nb)} \/ ( tau1 . A)) \/ ( tau1 . nb)) by Def4;

      then

       A1: a in ( {(A => nb)} \/ (( tau1 . A) \/ ( tau1 . nb))) by XBOOLE_1: 4;

      a <> (A => nb) by HILBERT2: 22;

      then not a in {(A => nb)} by TARSKI:def 1;

      then a in (( tau1 . A) \/ ( tau1 . nb)) by A1, XBOOLE_0:def 3;

      then a in ( tau1 . A) or a in ( tau1 . nb) by XBOOLE_0:def 3;

      hence thesis by Th9;

    end;

    theorem :: LTLAXIO3:11

    p in ( tau1 . q) & p <> q implies ( len p) < ( len q)

    proof

      defpred P1[ Element of l] means p in ( tau1 . $1) & p <> $1 implies ( len p) < ( len $1);

      

       A1: for n holds P1[( prop n)]

      proof

        let n;

        ( tau1 . ( prop n)) = {( prop n)} by Def4;

        hence thesis by TARSKI:def 1;

      end;

      

       A2: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that

         A3: P1[r] and

         A4: P1[s];

        set u = (r => s);

        ( tau1 . (r 'U' s)) = {(r 'U' s)} by Def4;

        hence P1[(r 'U' s)] by TARSKI:def 1;

        thus P1[u]

        proof

          assume that

           A5: p in ( tau1 . u) and

           A6: p <> u;

          ( tau1 . u) = (( {u} \/ ( tau1 . r)) \/ ( tau1 . s)) by Def4;

          then p in ( {u} \/ (( tau1 . r) \/ ( tau1 . s))) by XBOOLE_1: 4, A5;

          then

           A7: p in {u} or p in (( tau1 . r) \/ ( tau1 . s)) by XBOOLE_0:def 3;

          per cases by A7, TARSKI:def 1, A6, XBOOLE_0:def 3;

            suppose p in ( tau1 . r);

            hence thesis by HILBERT2: 16, XXREAL_0: 2, A3;

          end;

            suppose p in ( tau1 . s);

            hence thesis by HILBERT2: 16, XXREAL_0: 2, A4;

          end;

        end;

      end;

      ( tau1 . TFALSUM ) = { TFALSUM } by Def4;

      then

       A8: P1[ TFALSUM ] by TARSKI:def 1;

      for p holds P1[p] from HILBERT2:sch 2( A8, A1, A2);

      hence thesis;

    end;

    theorem :: LTLAXIO3:12

    

     Th12: ( tau1 . p) c= ( tau1 . ( 'not' p))

    proof

      set np = ( 'not' p), f = TFALSUM ;

      

       A1: ( tau1 . p) c= ( {np} \/ ( tau1 . p)) by XBOOLE_1: 7;

      ( {np} \/ ( tau1 . p)) c= (( {np} \/ ( tau1 . p)) \/ ( tau1 . f)) & ( tau1 . np) = (( {np} \/ ( tau1 . p)) \/ ( tau1 . f)) by XBOOLE_1: 7, Def4;

      hence thesis by A1;

    end;

    theorem :: LTLAXIO3:13

    

     Th13: ( tau1 . q) c= ( tau1 . (p '&&' q))

    proof

      set pq = (p '&&' q), np = ( 'not' p), nq = ( 'not' q);

      

       A1: ( tau1 . (p => nq)) c= ( tau1 . ( 'not' (p => nq))) by Th12;

      ( tau1 . (p => nq)) = (( {(p => nq)} \/ ( tau1 . p)) \/ ( tau1 . nq)) by Def4;

      then

       A2: ( tau1 . nq) c= ( tau1 . (p => nq)) by XBOOLE_1: 7;

      ( tau1 . q) c= ( tau1 . nq) by Th12;

      then ( tau1 . q) c= ( tau1 . (p => nq)) by A2;

      hence thesis by A1;

    end;

    theorem :: LTLAXIO3:14

    

     Th14: ( tau1 . q) c= ( tau1 . (p 'or' q))

    proof

      set pq = (p 'or' q), np = ( 'not' p), nq = ( 'not' q), npq = (np '&&' nq);

      ( tau1 . nq) c= ( tau1 . npq) & ( tau1 . q) c= ( tau1 . nq) by Th13, Th12;

      then

       A1: ( tau1 . q) c= ( tau1 . npq);

      ( tau1 . npq) c= ( tau1 . pq) by Th12;

      hence thesis by A1;

    end;

    definition

      let X;

      :: LTLAXIO3:def5

      func tau X -> Subset of LTLB_WFF means

      : Def5: x in it iff ex A st A in X & x in ( tau1 . A);

      existence

      proof

        set t = { ( tau1 . p) where p be Element of l : p in X };

        ( union t) c= l

        proof

          let x be object;

          assume x in ( union t);

          then

          consider y such that

           A1: x in y and

           A2: y in t by TARSKI:def 4;

          ex p be Element of l st y = ( tau1 . p) & p in X by A2;

          hence x in l by A1;

        end;

        then

        reconsider ut = ( union t) as Subset of l;

        x in ut iff ex A st A in X & x in ( tau1 . A)

        proof

          hereby

            assume x in ut;

            then

            consider y such that

             A3: x in y and

             A4: y in t by TARSKI:def 4;

            ex p st y = ( tau1 . p) & p in X by A4;

            hence ex A st A in X & x in ( tau1 . A) by A3;

          end;

          given A such that

           A5: A in X and

           A6: x in ( tau1 . A);

          ( tau1 . A) in t by A5;

          hence x in ut by TARSKI:def 4, A6;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let Y,Z be Subset of l such that

         A7: x in Y iff ex A st A in X & x in ( tau1 . A) and

         A8: x in Z iff ex A st A in X & x in ( tau1 . A);

        thus Y c= Z

        proof

          let x be object;

          assume x in Y;

          then ex A st A in X & x in ( tau1 . A) by A7;

          hence thesis by A8;

        end;

        thus Z c= Y

        proof

          let x be object;

          assume x in Z;

          then ex A st A in X & x in ( tau1 . A) by A8;

          hence thesis by A7;

        end;

      end;

    end

    theorem :: LTLAXIO3:15

    

     Th15: ( tau X) = ( union { ( tau1 . p) where p be Element of LTLB_WFF : p in X })

    proof

      set A = { ( tau1 . p) where p be Element of l : p in X };

      hereby

        let x be object;

        assume x in ( tau X);

        then

        consider p such that

         A1: p in X and

         A2: x in ( tau1 . p) by Def5;

        ( tau1 . p) in A by A1;

        hence x in ( union A) by TARSKI:def 4, A2;

      end;

      let x be object;

      assume x in ( union A);

      then

      consider y such that

       A3: x in y and

       A4: y in A by TARSKI:def 4;

      

       A5: ex p st y = ( tau1 . p) & p in X by A4;

      then

      reconsider x1 = x as Element of l by A3;

      thus x in ( tau X) by A5, A3, Def5;

    end;

    theorem :: LTLAXIO3:16

    

     Th16: X c= ( tau X)

    proof

      let x be object;

      defpred P1[ Element of l] means $1 in X implies $1 in ( tau X);

      assume

       A1: x in X;

      then

      reconsider x1 = x as Element of l;

      

       A2: for n holds P1[( prop n)]

      proof

        let n;

        set pr = ( prop n);

        pr in {pr} by TARSKI:def 1;

        then

         A3: pr in ( tau1 . pr) by Def4;

        assume pr in X;

        hence thesis by A3, Def5;

      end;

      

       A4: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that P1[r] and P1[s];

        thus P1[(r 'U' s)]

        proof

          set f = (r 'U' s);

          f in {f} by TARSKI:def 1;

          then

           A5: f in ( tau1 . f) by Def4;

          assume f in X;

          hence thesis by A5, Def5;

        end;

        thus P1[(r => s)]

        proof

          set f = (r => s);

          ( tau1 . f) = (( {f} \/ ( tau1 . r)) \/ ( tau1 . s)) by Def4

          .= ( {f} \/ (( tau1 . r) \/ ( tau1 . s))) by XBOOLE_1: 4;

          then

           A6: f in {f} & {f} c= ( tau1 . f) by TARSKI:def 1, XBOOLE_1: 7;

          assume f in X;

          hence thesis by A6, Def5;

        end;

      end;

      

       A7: P1[ TFALSUM ]

      proof

        set f = TFALSUM ;

        f in {f} by TARSKI:def 1;

        then

         A8: f in ( tau1 . f) by Def4;

        assume f in X;

        hence thesis by A8, Def5;

      end;

      for p holds P1[p] from HILBERT2:sch 2( A7, A2, A4);

      hence x in ( tau X) by A1;

    end;

    registration

      let X be empty Subset of LTLB_WFF ;

      cluster ( tau X) -> empty;

      coherence

      proof

        assume ( tau X) is non empty;

        then

        consider x be object such that

         A1: x in ( tau X);

        ex p st p in X & x in ( tau1 . p) by A1, Def5;

        hence contradiction;

      end;

    end

    registration

      let X be finite Subset of LTLB_WFF ;

      cluster ( tau X) -> finite;

      coherence

      proof

        set A = { ( tau1 . p) where p be Element of l : p in X };

        deffunc F( Element of l) = ( tau1 . $1);

        

         A1: for x st x in A holds x is finite

        proof

          let x;

          assume x in A;

          then ex p st x = ( tau1 . p) & p in X;

          hence thesis;

        end;

        set B = { F(p) where p be Element of l : p in X };

        

         A2: X is finite;

        

         A3: B is finite from FRAENKEL:sch 21( A2);

        ( tau X) = ( union A) by Th15;

        hence ( tau X) is finite by A3, FINSET_1: 7, A1;

      end;

    end

    registration

      let X be non empty Subset of LTLB_WFF ;

      cluster ( tau X) -> non empty;

      coherence

      proof

        X c= ( tau X) by Th16;

        hence thesis;

      end;

    end

    theorem :: LTLAXIO3:17

    ( tau ( tau X)) = ( tau X)

    proof

      thus ( tau ( tau X)) c= ( tau X)

      proof

        let x be object;

        assume x in ( tau ( tau X));

        then

        consider p such that

         A1: p in ( tau X) and

         A2: x in ( tau1 . p) by Def5;

        consider q such that

         A3: q in X and

         A4: p in ( tau1 . q) by A1, Def5;

        ( tau1 . p) c= ( tau1 . q) by A4, Th8;

        hence x in ( tau X) by A2, A3, Def5;

      end;

      thus ( tau X) c= ( tau ( tau X)) by Th16;

    end;

    theorem :: LTLAXIO3:18

    X is without_implication implies ( tau X) = X

    proof

      assume

       A1: X is without_implication;

      

       A2: ( tau X) c= X

      proof

        let x be object;

        assume x in ( tau X);

        then

        consider p such that

         A3: p in X and

         A4: x in ( tau1 . p) by Def5;

        x in {p} by A3, A1, Th5, A4;

        hence thesis by A3, TARSKI:def 1;

      end;

      X c= ( tau X) by Th16;

      hence thesis by A2;

    end;

    theorem :: LTLAXIO3:19

    

     Th19: (p => q) in ( tau X) implies p in ( tau X) & q in ( tau X)

    proof

      set t = { ( tau1 . r) where r be Element of l : r in X };

      assume (p => q) in ( tau X);

      then

      consider B such that

       A1: B in X and

       A2: (p => q) in ( tau1 . B) by Def5;

      

       A3: ( tau1 . B) in t by A1;

      p in ( tau1 . B) by Th7, A2;

      then

       A4: p in ( union t) by A3, TARSKI:def 4;

      q in ( tau1 . B) by Th7, A2;

      then q in ( union t) by TARSKI:def 4, A3;

      hence thesis by A4, Th15;

    end;

    theorem :: LTLAXIO3:20

    

     Th20: (p '&&' q) in ( tau X) implies p in ( tau X) & q in ( tau X)

    proof

      assume (p '&&' q) in ( tau X);

      then

       A1: (p => (q => TFALSUM )) in ( tau X) by Th19;

      then ( 'not' q) in ( tau X) by Th19;

      hence thesis by A1, Th19;

    end;

    theorem :: LTLAXIO3:21

    

     Th21: (p 'or' q) in ( tau X) implies p in ( tau X) & q in ( tau X)

    proof

      assume (p 'or' q) in ( tau X);

      then (( 'not' p) '&&' ( 'not' q)) in ( tau X) by Th19;

      then ( 'not' p) in ( tau X) & ( 'not' q) in ( tau X) by Th20;

      hence thesis by Th19;

    end;

    theorem :: LTLAXIO3:22

    ( untn (p,q)) in ( tau X) implies p in ( tau X) & q in ( tau X) & (p 'U' q) in ( tau X)

    proof

      assume

       A1: ( untn (p,q)) in ( tau X);

      then (p '&&' (p 'U' q)) in ( tau X) by Th21;

      hence thesis by A1, Th21, Th20;

    end;

    theorem :: LTLAXIO3:23

    p in ( tau X) implies ( tau1 . p) c= ( tau X)

    proof

      assume p in ( tau X);

      then

      consider B such that

       A1: B in X and

       A2: p in ( tau1 . B) by Def5;

      

       A3: ( tau1 . B) c= ( tau X) by Def5, A1;

      ( tau1 . p) c= ( tau1 . B) by A2, Th8;

      hence thesis by A3;

    end;

    begin

    definition

      :: LTLAXIO3:def6

      func Sub -> Function of LTLB_WFF , ( bool LTLB_WFF ) means

      : Def6: (it . TFALSUM ) = { TFALSUM } & (it . ( prop n)) = {( prop n)} & (it . (A => B)) = (( {(A => B)} \/ (it . A)) \/ (it . B)) & (it . (A 'U' B)) = ((( tau1 . ( untn (A,B))) \/ (it . A)) \/ (it . B));

      existence

      proof

        set bltl = ( bool l);

        deffunc F2( Element of NAT ) = {( prop $1)};

        defpred P3[ Element of l, Element of l, set, set, set] means ($3 is Element of bltl & $4 is Element of bltl implies ex a,b,c be Element of bltl st a = $3 & b = $4 & c = $5 & c = (( {($1 => $2)} \/ $3) \/ $4)) & ( not $3 is Element of bltl or not $4 is Element of bltl implies $5 = ( {} l));

        defpred P1[ Element of l, Element of l, set, set, set] means ($3 is Element of bltl & $4 is Element of bltl implies ex a,b,c be Element of bltl st a = $3 & b = $4 & c = $5 & c = ((( tau1 . ( untn ($1,$2))) \/ $3) \/ $4)) & ( not $3 is Element of bltl or not $4 is Element of bltl implies $5 = ( {} l));

        

         A1: for A, B holds for x,y be set holds ex z be set st P3[A, B, x, y, z]

        proof

          let A, B, x, y;

          per cases ;

            suppose that

             A2: x is Element of bltl and

             A3: y is Element of bltl;

            reconsider b = y as Element of bltl by A3;

            reconsider a = x as Element of bltl by A2;

            consider z be set such that

             A4: z = (( {(A => B)} \/ a) \/ b);

            take z;

            thus thesis by A4;

          end;

            suppose not x is Element of bltl or not y is Element of bltl;

            hence thesis;

          end;

        end;

        

         A5: for A, B holds for x,y be set holds ex z be set st P1[A, B, x, y, z]

        proof

          let A, B, x, y;

          per cases ;

            suppose that

             A6: x is Element of bltl and

             A7: y is Element of bltl;

            reconsider b = y as Element of bltl by A7;

            reconsider a = x as Element of bltl by A6;

            consider z be set such that

             A8: z = ((( tau1 . ( untn (A,B))) \/ a) \/ b);

            take z;

            thus thesis by A8;

          end;

            suppose not x is Element of bltl or not y is Element of bltl;

            hence thesis;

          end;

        end;

        

         A9: for p, q holds for a,b,c,d be set st P1[p, q, a, b, c] & P1[p, q, a, b, d] holds c = d;

        

         A10: for p, q holds for a,b,c,d be set st P3[p, q, a, b, c] & P3[p, q, a, b, d] holds c = d;

        consider val be ManySortedSet of l such that

         A11: (val . TFALSUM ) = { TFALSUM } & (for n holds (val . ( prop n)) = F2(n)) & for p, q holds P1[p, q, (val . p), (val . q), (val . (p 'U' q))] & P3[p, q, (val . p), (val . q), (val . (p => q))] from HILBERT2:sch 3( A5, A1, A9, A10);

         A12:

        now

           A13:

          now

            let A, B;

             P3[A, B, (val . A), (val . B), (val . (A => B))] by A11;

            hence (val . (A => B)) in bltl;

          end;

           A14:

          now

            let A, B;

             P1[A, B, (val . A), (val . B), (val . (A 'U' B))] by A11;

            hence (val . (A 'U' B)) in bltl;

          end;

          let x be object;

          assume x in l;

          then

          reconsider x1 = x as Element of l;

           A15:

          now

            let n;

            (val . ( prop n)) = {( prop n)} by A11;

            hence (val . ( prop n)) in bltl;

          end;

          per cases by LTLAXIO1: 4;

            suppose x1 = TFALSUM ;

            hence (val . x) in bltl by A11;

          end;

            suppose ex n be Element of NAT st x1 = ( prop n);

            hence (val . x) in bltl by A15;

          end;

            suppose ex p, q st x1 = (p 'U' q);

            hence (val . x) in bltl by A14;

          end;

            suppose ex p, q st x1 = (p => q);

            hence (val . x) in bltl by A13;

          end;

        end;

        ( dom val) = l by PARTFUN1:def 2;

        then

        reconsider val as Function of l, bltl by A12, FUNCT_2: 3;

         A16:

        now

          let A, B;

           P3[A, B, (val . A), (val . B), (val . (A => B))] by A11;

          hence (val . (A => B)) = (( {(A => B)} \/ (val . A)) \/ (val . B));

        end;

        take val;

        now

          let A, B;

           P1[A, B, (val . A), (val . B), (val . (A 'U' B))] by A11;

          hence (val . (A 'U' B)) = ((( tau1 . ( untn (A,B))) \/ (val . A)) \/ (val . B));

        end;

        hence thesis by A16, A11;

      end;

      uniqueness

      proof

        set bltl = ( bool LTLB_WFF );

        let v1,v2 be Function of l, bltl;

        assume

         A17: (v1 . TFALSUM ) = { TFALSUM } & (v1 . ( prop n)) = {( prop n)} & (v1 . (A => B)) = (( {(A => B)} \/ (v1 . A)) \/ (v1 . B)) & (v1 . (A 'U' B)) = ((( tau1 . ( untn (A,B))) \/ (v1 . A)) \/ (v1 . B));

        assume

         A18: (v2 . TFALSUM ) = { TFALSUM } & (v2 . ( prop n)) = {( prop n)} & (v2 . (A => B)) = (( {(A => B)} \/ (v2 . A)) \/ (v2 . B)) & (v2 . (A 'U' B)) = ((( tau1 . ( untn (A,B))) \/ (v2 . A)) \/ (v2 . B));

        thus v1 = v2

        proof

          defpred P1[ Element of l] means (v1 . $1) = (v2 . $1);

          

           A19: for n holds P1[( prop n)]

          proof

            let n;

            (v1 . ( prop n)) = {( prop n)} by A17

            .= (v2 . ( prop n)) by A18;

            hence P1[( prop n)];

          end;

          

           A20: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

          proof

            let r, s;

            assume

             A21: P1[r] & P1[s];

            

             A22: (v1 . (r 'U' s)) = ((( tau1 . ( untn (r,s))) \/ (v1 . r)) \/ (v1 . s)) by A17

            .= (v2 . (r 'U' s)) by A18, A21;

            (v1 . (r => s)) = (( {(r => s)} \/ (v1 . r)) \/ (v1 . s)) by A17

            .= (v2 . (r => s)) by A18, A21;

            hence thesis by A22;

          end;

          

           A23: P1[ TFALSUM ] by A17, A18;

          for x be Element of l holds P1[x] from HILBERT2:sch 2( A23, A19, A20);

          then

           A24: for x be Element of l st x in ( dom v1) holds P1[x];

          ( dom v1) = l by FUNCT_2:def 1

          .= ( dom v2) by FUNCT_2:def 1;

          hence thesis by A24, PARTFUN1: 5;

        end;

      end;

    end

    theorem :: LTLAXIO3:24

    

     Th24: (p 'U' q) in ( Sub . (p 'U' q))

    proof

      set puq = (p 'U' q);

      

       A1: ( tau1 . puq) c= ( tau1 . (p '&&' puq)) by Th13;

      puq in {puq} by TARSKI:def 1;

      then

       A2: puq in ( tau1 . puq) by Def4;

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

      then ( tau1 . ( untn (p,q))) c= (( tau1 . ( untn (p,q))) \/ ( Sub . p)) & (( tau1 . ( untn (p,q))) \/ ( Sub . p)) c= ( Sub . puq) by XBOOLE_1: 7, Def6;

      then

       A3: ( tau1 . ( untn (p,q))) c= ( Sub . puq);

      ( tau1 . (p '&&' puq)) c= ( tau1 . ( untn (p,q))) by Th14;

      then ( tau1 . (p '&&' puq)) c= ( Sub . puq) by A3;

      then ( tau1 . puq) c= ( Sub . puq) by A1;

      hence thesis by A2;

    end;

    theorem :: LTLAXIO3:25

    

     Th25: ( tau1 . p) c= ( Sub . p)

    proof

      defpred P1[ Element of l] means ( tau1 . $1) c= ( Sub . $1);

      set f = TFALSUM ;

      

       A1: for n holds P1[( prop n)]

      proof

        let n;

        set pr = ( prop n);

        ( tau1 . pr) = {pr} by Def4

        .= ( Sub . pr) by Def6;

        hence thesis;

      end;

      

       A2: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that

         A3: P1[r] and

         A4: P1[s];

        thus P1[(r 'U' s)]

        proof

          set f = (r 'U' s);

           {f} c= ( Sub . f) by Th24, ZFMISC_1: 31;

          hence thesis by Def4;

        end;

        thus P1[(r => s)]

        proof

          set f = (r => s);

          

           A5: ( Sub . f) = (( {f} \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          ( {f} \/ ( tau1 . r)) c= ( {f} \/ ( Sub . r)) & ( tau1 . f) = (( {f} \/ ( tau1 . r)) \/ ( tau1 . s)) by XBOOLE_1: 13, A3, Def4;

          hence thesis by A5, A4, XBOOLE_1: 13;

        end;

      end;

      ( tau1 . f) = {f} by Def4

      .= ( Sub . f) by Def6;

      then

       A6: P1[f];

      for p holds P1[p] from HILBERT2:sch 2( A6, A1, A2);

      hence thesis;

    end;

    registration

      let p;

      cluster ( Sub . p) -> non empty finite;

      coherence

      proof

        ( tau1 . p) c= ( Sub . p) by Th25;

        hence ( Sub . p) is non empty;

        defpred P1[ Element of l] means ( Sub . $1) is finite;

        

         A1: for n holds P1[( prop n)]

        proof

          let n;

          ( Sub . ( prop n)) = {( prop n)} by Def6;

          hence thesis;

        end;

        

         A2: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

        proof

          let r, s;

          assume

           A3: P1[r] & P1[s];

          ( Sub . (r 'U' s)) = ((( tau1 . ( untn (r,s))) \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          hence P1[(r 'U' s)] by A3;

          ( Sub . (r => s)) = (( {(r => s)} \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          hence P1[(r => s)] by A3;

        end;

        

         A4: P1[ TFALSUM ] by Def6;

        for p holds P1[p] from HILBERT2:sch 2( A4, A1, A2);

        hence ( Sub . p) is finite;

      end;

    end

    theorem :: LTLAXIO3:26

    p in ( Sub . (A 'U' B)) implies ((A 'U' B) in ( Sub . q) implies p in ( Sub . q))

    proof

      set aub = (A 'U' B), f = TFALSUM ;

      defpred P1[ Element of l] means aub in ( Sub . $1) implies p in ( Sub . $1);

      

       A1: for n holds P1[( prop n)]

      proof

        let n;

        set pr = ( prop n);

        assume aub in ( Sub . pr);

        then aub in {pr} by Def6;

        then aub = pr by TARSKI:def 1;

        hence thesis by HILBERT2: 24;

      end;

      assume

       A2: p in ( Sub . aub);

      

       A3: for r, s st P1[r] & P1[s] holds P1[(r 'U' s)] & P1[(r => s)]

      proof

        let r, s;

        assume that

         A4: P1[r] and

         A5: P1[s];

        thus P1[(r 'U' s)]

        proof

          set f = (r 'U' s);

          

           A6: ( tau1 . r) c= ( Sub . r) by Th25;

          

           A7: ( Sub . f) = ((( tau1 . ( untn (r,s))) \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          then

           A8: ( Sub . s) c= ( Sub . f) by XBOOLE_1: 7;

          ( Sub . r) c= (( tau1 . ( untn (r,s))) \/ ( Sub . r)) & (( tau1 . ( untn (r,s))) \/ ( Sub . r)) c= ( Sub . f) by XBOOLE_1: 7, A7;

          then

           A9: ( Sub . r) c= ( Sub . f);

          assume aub in ( Sub . f);

          then

           A10: aub in ((( tau1 . ( untn (r,s))) \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          

           A11: ( tau1 . s) c= ( Sub . s) by Th25;

          per cases by A10, XBOOLE_0:def 3;

            suppose

             A12: aub in (( tau1 . ( untn (r,s))) \/ ( Sub . r));

            per cases by A12, XBOOLE_0:def 3;

              suppose aub in ( tau1 . ( untn (r,s)));

              then aub in ( tau1 . (( 'not' s) '&&' ( 'not' (r '&&' f)))) by Th9;

              then aub in ( tau1 . ( 'not' s)) or aub in ( tau1 . ( 'not' (r '&&' f))) by Th10;

              then

               A13: aub in ( tau1 . s) or aub in ( tau1 . (r '&&' f)) by Th9;

              per cases by A13, Th10;

                suppose

                 A14: aub in ( tau1 . r) or aub in ( tau1 . s);

                per cases by A14;

                  suppose aub in ( tau1 . r);

                  hence p in ( Sub . f) by A6, A4, A9;

                end;

                  suppose aub in ( tau1 . s);

                  hence p in ( Sub . f) by A11, A5, A8;

                end;

              end;

                suppose aub in ( tau1 . f);

                then aub in {f} by Def4;

                hence p in ( Sub . f) by TARSKI:def 1, A2;

              end;

            end;

              suppose aub in ( Sub . r);

              hence p in ( Sub . f) by A4, A9;

            end;

          end;

            suppose aub in ( Sub . s);

            hence p in ( Sub . f) by A5, A8;

          end;

        end;

        thus P1[(r => s)]

        proof

          set f = (r => s);

          

           A15: ( Sub . f) = (( {f} \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          then

           A16: ( Sub . s) c= ( Sub . f) by XBOOLE_1: 7;

          ( Sub . r) c= ( {f} \/ ( Sub . r)) & ( {f} \/ ( Sub . r)) c= ( Sub . f) by XBOOLE_1: 7, A15;

          then

           A17: ( Sub . r) c= ( Sub . f);

          assume aub in ( Sub . f);

          then

           A18: aub in (( {f} \/ ( Sub . r)) \/ ( Sub . s)) by Def6;

          per cases by A18, XBOOLE_0:def 3;

            suppose

             A19: aub in ( {f} \/ ( Sub . r));

            per cases by A19, XBOOLE_0:def 3;

              suppose aub in {f};

              then aub = f by TARSKI:def 1;

              hence p in ( Sub . f) by HILBERT2: 22;

            end;

              suppose aub in ( Sub . r);

              hence p in ( Sub . f) by A4, A17;

            end;

          end;

            suppose aub in ( Sub . s);

            hence p in ( Sub . f) by A5, A16;

          end;

        end;

      end;

      

       A20: P1[f]

      proof

        assume aub in ( Sub . f);

        then aub in {f} by Def6;

        then aub = f by TARSKI:def 1;

        hence thesis by HILBERT2: 23;

      end;

      for p holds P1[p] from HILBERT2:sch 2( A20, A1, A3);

      hence thesis;

    end;

    definition

      let X;

      :: LTLAXIO3:def7

      func Subt X -> Subset of ( bool LTLB_WFF ) equals { ( Sub . A) where A be Element of LTLB_WFF : A in X };

      correctness

      proof

        set s = { ( Sub . A) where A be Element of l : A in X };

        s c= ( bool l)

        proof

          let x be object;

          assume x in s;

          then ex A st x = ( Sub . A) & A in X;

          hence x in ( bool l);

        end;

        hence thesis;

      end;

    end

    registration

      let X be finite Subset of LTLB_WFF ;

      cluster ( Subt X) -> finite finite-membered;

      coherence

      proof

        deffunc F( Element of l) = ( Sub . $1);

        

         A1: X is finite;

        { F(A) where A be Element of l : A in X } is finite from FRAENKEL:sch 21( A1);

        hence ( Subt X) is finite;

        let x;

        assume x in ( Subt X);

        then ex A st x = ( Sub . A) & A in X;

        hence x is finite;

      end;

    end

    begin

    definition

      mode PNPair is Element of [:( LTLB_WFF ** ), ( LTLB_WFF ** ):];

    end

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

    reserve P,Q,P1,R for PNPair;

    definition

      let P;

      :: original: `1

      redefine

      func P `1 -> one-to-one FinSequence of LTLB_WFF ;

      coherence

      proof

        consider x,y be object such that x in (l ** ) and y in (l ** ) and

         A1: P = [x, y] by ZFMISC_1:def 2;

        (P `1 ) = ( [x, y] `1 ) by A1

        .= x;

        hence thesis by Def2;

      end;

      :: original: `2

      redefine

      func P `2 -> one-to-one FinSequence of LTLB_WFF ;

      coherence

      proof

        consider x,y be object such that x in (l ** ) and y in (l ** ) and

         A2: P = [x, y] by ZFMISC_1:def 2;

        (P `2 ) = ( [x, y] `2 ) by A2

        .= y;

        hence thesis by Def2;

      end;

    end

    definition

      let P;

      :: LTLAXIO3:def8

      func rng P -> finite Subset of LTLB_WFF equals (( rng (P `1 )) \/ ( rng (P `2 )));

      correctness ;

    end

    definition

      let fp,fm be one-to-one FinSequence of LTLB_WFF ;

      :: original: [

      redefine

      func [fp,fm] -> PNPair ;

      coherence

      proof

        fp in (l ** ) & fm in (l ** ) by Def2;

        hence [fp, fm] is PNPair by ZFMISC_1:def 2;

      end;

    end

    definition

      let P;

      :: LTLAXIO3:def9

      func P ^ -> Element of LTLB_WFF equals ((( con (P `1 )) /. ( len ( con (P `1 )))) '&&' (( con ( nega (P `2 ))) /. ( len ( con ( nega (P `2 ))))));

      correctness ;

    end

    theorem :: LTLAXIO3:27

    

     Th27: ( [( <*> LTLB_WFF ), ( <*> LTLB_WFF )] ^ ) = ( TVERUM '&&' TVERUM )

    proof

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

      then ( len ( nega ( <*> l))) = 0 by LTLAXIO2:def 4;

      then ( nega ( <*> l)) = 0 ;

      hence ( [( <*> l), ( <*> l)] ^ ) = ( TVERUM '&&' TVERUM ) by LTLAXIO2: 10;

    end;

    theorem :: LTLAXIO3:28

    

     Th28: A in ( rng (P `1 )) implies ( {} LTLB_WFF ) |- ((P ^ ) => A)

    proof

      set fp = (P `1 ), fm = (P `2 ), nfm = ( nega fm);

      assume A in ( rng fp);

      then

      consider i be Nat such that

       A1: i in ( dom fp) and

       A2: (fp . i) = A by FINSEQ_2: 10;

      ((P ^ ) => A) is ctaut

      proof

        let g;

        set v = ( VAL g), r = (v . kon(|)), s = (v . kon(/^));

        

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

        

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

        .= (((v . kon(fp)) '&' (v . kon(nfm))) => (v . A)) by LTLAXIO1: 31

        .= ((((r '&' (v . (fp /. i))) '&' s) '&' (v . kon(nfm))) => (v . A)) by LTLAXIO2: 18, A1

        .= ((((r '&' (v . A)) '&' s) '&' (v . kon(nfm))) => (v . A)) by PARTFUN1:def 6, A1, A2

        .= 1 by A3;

      end;

      then ((P ^ ) => A) in LTL_axioms by LTLAXIO1:def 17;

      hence ( {} l) |- ((P ^ ) => A) by LTLAXIO1: 42;

    end;

    theorem :: LTLAXIO3:29

    

     Th29: A in ( rng (P `2 )) implies ( {} LTLB_WFF ) |- ((P ^ ) => ( 'not' A))

    proof

      set fp = (P `1 ), fm = (P `2 ), nfm = ( nega fm);

      assume A in ( rng fm);

      then

      consider i be Nat such that

       A1: i in ( dom fm) and

       A2: (fm . i) = A by FINSEQ_2: 10;

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

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

      then

       A3: i <= ( len nfm) by LTLAXIO2:def 4;

      1 <= i by A1, FINSEQ_3: 25;

      then

       A4: i in ( dom nfm) by A3, FINSEQ_3: 25;

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

      proof

        let g;

        set v = ( VAL g), p = (v . kon(fp)), q = (v . kon(nfm)), r = (v . kon(|)), s = (v . kon(/^));

        

         A5: (v . ( 'not' A)) = 1 or (v . ( 'not' A)) = 0 by XBOOLEAN:def 3;

        

         A6: q = ((r '&' (v . (nfm /. i))) '&' s) by LTLAXIO2: 18, A4

        .= ((r '&' (v . ( 'not' (fm /. i)))) '&' s) by LTLAXIO2: 8, A1

        .= ((r '&' (v . ( 'not' A))) '&' s) by PARTFUN1:def 6, A1, A2;

        

        thus (v . ((P ^ ) => ( 'not' A))) = ((v . (P ^ )) => (v . ( 'not' A))) by LTLAXIO1:def 15

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

        .= 1 by A5, A6;

      end;

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

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

    end;

    definition

      let P;

      :: LTLAXIO3:def10

      attr P is Inconsistent means

      : Def10: ( {} LTLB_WFF ) |- ( 'not' (P ^ ));

    end

    notation

      let P;

      antonym P is consistent for P is Inconsistent;

    end

    definition

      let P;

      :: LTLAXIO3:def11

      attr P is complete means ( tau ( rng P)) = ( rng P);

    end

    registration

      cluster [( <*> LTLB_WFF ), ( <*> LTLB_WFF )] -> consistent;

      coherence

      proof

        let P;

        assume

         A1: P = [( <*> l), ( <*> l)];

         not ( {} l) |= ( 'not' (P ^ ))

        proof

          reconsider M = ( NAT --> {} ) as LTLModel by Th2;

          set s = ( SAT M);

          take M;

          thus M |= ( {} l);

          (s . [ 0 , ( 'not' (P ^ ))]) <> 1

          proof

            assume (s . [ 0 , ( 'not' (P ^ ))]) = 1;

            then (s . [ 0 , (P ^ )]) = 0 by LTLAXIO1: 5;

            then (s . [ 0 , TVERUM ]) <> 1 by LTLAXIO1: 7, A1, Th27;

            hence contradiction by LTLAXIO1: 6;

          end;

          hence not M |= ( 'not' (P ^ ));

        end;

        hence P is consistent by LTLAXIO1: 41;

      end;

    end

    registration

      cluster [( <*> LTLB_WFF ), ( <*> LTLB_WFF )] -> complete;

      coherence

      proof

        let P;

        assume

         A1: P = [( <*> l), ( <*> l)];

        then

         A2: ( rng (P `1 )) = {} ;

        ( rng (P `2 )) = {} by A1;

        then ( tau ( rng P)) = ( rng P) by A2;

        hence P is complete;

      end;

    end

    registration

      cluster consistent complete for PNPair;

      existence

      proof

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

        take p;

        thus thesis;

      end;

    end

    registration

      let P be consistent PNPair;

      cluster [(P `1 ), (P `2 )] -> consistent;

      coherence

      proof

        let a be PNPair;

        assume a = [(P `1 ), (P `2 )];

        then

         A1: (a `1 ) = (P `1 ) & (a `2 ) = (P `2 );

         not ( {} l) |- ( 'not' (P ^ )) by Def10;

        then not ( {} l) |- ( 'not' (a ^ )) by A1;

        hence a is consistent;

      end;

    end

    begin

    theorem :: LTLAXIO3:30

    for P be consistent PNPair holds ( rng (P `1 )) misses ( rng (P `2 ))

    proof

      let P be consistent PNPair;

      assume not ( rng (P `1 )) misses ( rng (P `2 ));

      then not (( rng (P `1 )) /\ ( rng (P `2 ))) = {} ;

      then

      consider x be object such that

       A1: x in (( rng (P `1 )) /\ ( rng (P `2 ))) by XBOOLE_0:def 1;

      x in ( rng (P `1 )) by XBOOLE_0:def 4, A1;

      then

      consider n1 be object such that

       A2: n1 in ( dom (P `1 )) and

       A3: ((P `1 ) . n1) = x by FUNCT_1:def 3;

      x in ( rng (P `2 )) by XBOOLE_0:def 4, A1;

      then

      consider n2 be object such that

       A4: n2 in ( dom (P `2 )) and

       A5: ((P `2 ) . n2) = x by FUNCT_1:def 3;

      reconsider n1, n2 as Element of NAT by A2, A4;

      x = ((P `2 ) /. n2) by PARTFUN1:def 6, A4, A5;

      then

      reconsider x as Element of l;

      

       A6: 1 <= n2 by FINSEQ_3: 25, A4;

      

       A7: n2 <= ( len (P `2 )) by FINSEQ_3: 25, A4;

      ( 'not' (P ^ )) is ctaut

      proof

        let g;

        set nP2 = ( nega (P `2 )), v = ( VAL g);

        

         A8: (v . x) = TRUE or (v . x) = FALSE by XBOOLEAN:def 3;

        

         A9: (v . ((P `1 ) /. n1)) = (v . x) by PARTFUN1:def 6, A2, A3;

        n2 <= ( len nP2) by A7, LTLAXIO2:def 4;

        then

         A10: n2 in ( dom nP2) by FINSEQ_3: 25, A6;

        

         A11: (v . (nP2 /. n2)) = (v . ( 'not' ((P `2 ) /. n2))) by LTLAXIO2: 8, A4

        .= (v . ( 'not' x)) by A4, A5, PARTFUN1:def 6

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

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

        

         A12: (v . (P ^ )) = ((v . kon(`1)) '&' (v . kon(nega))) by LTLAXIO1: 31

        .= ((((v . kon(|)) '&' (v . ((P `1 ) /. n1))) '&' (v . kon(/^))) '&' (v . kon(nP2))) by LTLAXIO2: 18, A2

        .= ((((v . kon(|)) '&' (v . ((P `1 ) /. n1))) '&' (v . kon(/^))) '&' (((v . kon(|)) '&' (v . (nP2 /. n2))) '&' (v . kon(/^)))) by LTLAXIO2: 18, A10

        .= 0 by A8, A11, A9;

        

        thus (v . ( 'not' (P ^ ))) = ((v . (P ^ )) => (v . TFALSUM )) by LTLAXIO1:def 15

        .= 1 by A12;

      end;

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

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

      hence contradiction by Def10;

    end;

    theorem :: LTLAXIO3:31

    

     Th31: for P be consistent PNPair st not A in ( rng P) holds ( [((P `1 ) ^^ <*A*>), (P `2 )] is consistent or [(P `1 ), ((P `2 ) ^^ <*A*>)] is consistent)

    proof

      let P be consistent PNPair;

      set fpa = ((P `1 ) ^^ <*A*>), fma = ((P `2 ) ^^ <*A*>), Pl = [fpa, (P `2 )], Pr = [(P `1 ), fma], np = ( 'not' (P ^ )), npl = ( 'not' (Pl ^ )), npr = ( 'not' (Pr ^ )), na = <*( 'not' A)*>;

      assume

       A1: not A in ( rng P);

      then not A in ( rng (P `1 )) by XBOOLE_0:def 3;

      then ( rng (P `1 )) misses {A} by ZFMISC_1: 50;

      then ( rng (P `1 )) misses ( rng <*A*>) by FINSEQ_1: 39;

      then

       A2: fpa = ((P `1 ) ^ <*A*>) by Def3;

       not A in ( rng (P `2 )) by A1, XBOOLE_0:def 3;

      then ( rng (P `2 )) misses {A} by ZFMISC_1: 50;

      then ( rng (P `2 )) misses ( rng <*A*>) by FINSEQ_1: 39;

      then fma = ((P `2 ) ^ <*A*>) by Def3;

      then

       A3: ( nega fma) = (( nega (P `2 )) ^ <*( 'not' A)*>) by LTLAXIO2: 15;

      (npl => (npr => np)) is ctaut

      proof

        let g;

        set v = ( VAL g), vf = (v . TFALSUM );

        

         A4: vf = 0 by LTLAXIO1:def 15;

        set p = (((v . (P ^ )) '&' (v . A)) => vf), q = (((v . (P ^ )) '&' ((v . A) => vf)) => vf);

        

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

        

         A6: (v . (Pr ^ )) = ((v . kon(`1)) '&' (v . kon(nega))) by LTLAXIO1: 31

        .= ((v . kon(`1)) '&' ((v . kon(nega)) '&' (v . kon(na)))) by LTLAXIO2: 17, A3

        .= (((v . kon(`1)) '&' (v . kon(nega))) '&' (v . kon(na)))

        .= ((v . (P ^ )) '&' (v . kon(na))) by LTLAXIO1: 31

        .= ((v . (P ^ )) '&' (v . ( 'not' A))) by LTLAXIO2: 11

        .= ((v . (P ^ )) '&' ((v . A) => vf)) by LTLAXIO1:def 15;

        

         A7: (v . (Pl ^ )) = ((v . kon(fpa)) '&' (v . kon(nega))) by LTLAXIO1: 31

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

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

        .= (((v . kon(`1)) '&' (v . kon(nega))) '&' (v . A))

        .= ((v . (P ^ )) '&' (v . A)) by LTLAXIO1: 31;

        

         A8: (v . (P ^ )) = 1 or (v . (P ^ )) = 0 by XBOOLEAN:def 3;

        

        thus (v . (npl => (npr => np))) = ((v . npl) => (v . (npr => np))) by LTLAXIO1:def 15

        .= ((v . npl) => ((v . npr) => (v . np))) by LTLAXIO1:def 15

        .= (p => ((v . npr) => (v . np))) by A7, LTLAXIO1:def 15

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

        .= 1 by A8, A5, A4, LTLAXIO1:def 15;

      end;

      then (npl => (npr => np)) in LTL_axioms by LTLAXIO1:def 17;

      then

       A9: ( {} l) |- (npl => (npr => np)) by LTLAXIO1: 42;

      assume that

       A10: Pl is Inconsistent and

       A11: Pr is Inconsistent;

      ( {} l) |- npl by A10;

      then

       A12: ( {} l) |- (npr => np) by A9, LTLAXIO1: 43;

      ( {} l) |- npr by A11;

      hence contradiction by A12, Def10, LTLAXIO1: 43;

    end;

    theorem :: LTLAXIO3:32

    for P be consistent PNPair holds not TFALSUM in ( rng (P `1 ))

    proof

      let P be consistent PNPair;

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

      then ( {} l) |- ( 'not' (P ^ )) by Th28;

      hence contradiction by Def10;

    end;

    theorem :: LTLAXIO3:33

    for P be consistent PNPair st A in ( rng P) & B in ( rng P) & (A => B) in ( rng P) holds ((A => B) in ( rng (P `1 )) iff (A in ( rng (P `2 )) or B in ( rng (P `1 ))))

    proof

      let P be consistent PNPair;

      assume that

       A1: A in ( rng P) and

       A2: B in ( rng P) and

       A3: (A => B) in ( rng P);

      set p = (P ^ ), pa = (p => A), pna = (p => ( 'not' A)), pb = (p => B), pnb = (p => ( 'not' B)), pab = (p => (A => B)), pnab = (p => ( 'not' (A => B))), np = ( 'not' p);

      hereby

        (pa => (pnb => (pab => np))) is ctaut

        proof

          let g;

          set v = ( VAL g), vf = (v . TFALSUM );

          

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

          

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

          

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

          

           A7: vf = 0 & (v . pa) = ((v . p) => (v . A)) by LTLAXIO1:def 15;

          

           A8: (v . pab) = ((v . p) => (v . (A => B))) by LTLAXIO1:def 15

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

          

           A9: (v . pnb) = ((v . p) => (v . ( 'not' B))) by LTLAXIO1:def 15

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

          

          thus (v . (pa => (pnb => (pab => np)))) = ((v . pa) => (v . (pnb => (pab => np)))) by LTLAXIO1:def 15

          .= ((v . pa) => ((v . pnb) => (v . (pab => np)))) by LTLAXIO1:def 15

          .= ((v . pa) => ((v . pnb) => ((v . pab) => (v . np)))) by LTLAXIO1:def 15

          .= 1 by A4, A5, A6, A7, A8, LTLAXIO1:def 15, A9;

        end;

        then (pa => (pnb => (pab => np))) in LTL_axioms by LTLAXIO1:def 17;

        then

         A10: ( {} l) |- (pa => (pnb => (pab => np))) by LTLAXIO1: 42;

        assume (A => B) in ( rng (P `1 ));

        then

         A11: ( {} l) |- pab by Th28;

        assume that

         A12: not A in ( rng (P `2 )) and

         A13: not B in ( rng (P `1 ));

        B in ( rng (P `2 )) by A13, A2, XBOOLE_0:def 3;

        then

         A14: ( {} l) |- pnb by Th29;

        A in ( rng (P `1 )) by A12, A1, XBOOLE_0:def 3;

        then ( {} l) |- pa by Th28;

        then ( {} l) |- (pnb => (pab => np)) by A10, LTLAXIO1: 43;

        then ( {} l) |- (pab => np) by LTLAXIO1: 43, A14;

        hence contradiction by LTLAXIO1: 43, A11, Def10;

      end;

      assume

       A15: A in ( rng (P `2 )) or B in ( rng (P `1 ));

      assume not (A => B) in ( rng (P `1 ));

      then (A => B) in ( rng (P `2 )) by XBOOLE_0:def 3, A3;

      then

       A16: ( {} l) |- pnab by Th29;

      per cases by A15;

        suppose

         A17: A in ( rng (P `2 ));

        (pna => (pnab => np)) is ctaut

        proof

          let g;

          set v = ( VAL g), vf = (v . TFALSUM );

          

           A18: vf = 0 by LTLAXIO1:def 15;

          

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

          

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

          

           A21: (v . pna) = ((v . p) => (v . ( 'not' A))) by LTLAXIO1:def 15

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

          

           A22: (v . pnab) = ((v . p) => (v . ( 'not' (A => B)))) by LTLAXIO1:def 15

          .= ((v . p) => ((v . (A => B)) => vf)) by LTLAXIO1:def 15

          .= ((v . p) => (((v . A) => (v . B)) => vf)) by LTLAXIO1:def 15;

          

          thus (v . (pna => (pnab => np))) = ((v . pna) => (v . (pnab => np))) by LTLAXIO1:def 15

          .= ((v . pna) => ((v . pnab) => (v . np))) by LTLAXIO1:def 15

          .= 1 by A19, A20, A18, LTLAXIO1:def 15, A21, A22;

        end;

        then (pna => (pnab => np)) in LTL_axioms by LTLAXIO1:def 17;

        then

         A23: ( {} l) |- (pna => (pnab => np)) by LTLAXIO1: 42;

        ( {} l) |- pna by A17, Th29;

        then ( {} l) |- (pnab => np) by A23, LTLAXIO1: 43;

        hence contradiction by LTLAXIO1: 43, A16, Def10;

      end;

        suppose

         A24: B in ( rng (P `1 ));

        (pb => (pnab => np)) is ctaut

        proof

          let g;

          set v = ( VAL g), vf = (v . TFALSUM );

          

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

          

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

          

           A27: vf = 0 & (v . pb) = ((v . p) => (v . B)) by LTLAXIO1:def 15;

          

           A28: (v . pnab) = ((v . p) => (v . ( 'not' (A => B)))) by LTLAXIO1:def 15

          .= ((v . p) => ((v . (A => B)) => vf)) by LTLAXIO1:def 15

          .= ((v . p) => (((v . A) => (v . B)) => vf)) by LTLAXIO1:def 15;

          

          thus (v . (pb => (pnab => np))) = ((v . pb) => (v . (pnab => np))) by LTLAXIO1:def 15

          .= ((v . pb) => ((v . pnab) => (v . np))) by LTLAXIO1:def 15

          .= 1 by A25, A26, A27, LTLAXIO1:def 15, A28;

        end;

        then (pb => (pnab => np)) in LTL_axioms by LTLAXIO1:def 17;

        then

         A29: ( {} l) |- (pb => (pnab => np)) by LTLAXIO1: 42;

        ( {} l) |- pb by A24, Th28;

        then ( {} l) |- (pnab => np) by A29, LTLAXIO1: 43;

        hence contradiction by LTLAXIO1: 43, A16, Def10;

      end;

    end;

    theorem :: LTLAXIO3:34

    for P be consistent PNPair holds ex P1 be consistent PNPair st ( rng (P `1 )) c= ( rng (P1 `1 )) & ( rng (P `2 )) c= ( rng (P1 `2 )) & ( tau ( rng P)) = ( rng P1)

    proof

      let P be consistent PNPair;

      set tfp = (( tau ( rng P)) \ ( rng P));

      consider t be FinSequence such that

       A1: ( rng t) = tfp and

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

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

      defpred Pr[ Nat, Element of [:(l ** ), (l ** ):], Element of [:(l ** ), (l ** ):]] means $2 is consistent implies (( [(($2 `1 ) ^^ <*(t /. $1)*>), ($2 `2 )] is consistent implies $3 = [(($2 `1 ) ^^ <*(t /. $1)*>), ($2 `2 )]) & ( not [(($2 `1 ) ^^ <*(t /. $1)*>), ($2 `2 )] is consistent implies $3 = [($2 `1 ), (($2 `2 ) ^^ <*(t /. $1)*>)]));

       A3:

      now

        let n be Nat;

        assume that 1 <= n and n <= ((( len t) + 1) - 1);

        let x be Element of [:(l ** ), (l ** ):];

         [((x `1 ) ^^ <*(t /. n)*>), (x `2 )] is consistent or not [((x `1 ) ^^ <*(t /. n)*>), (x `2 )] is consistent;

        hence ex y be Element of [:(l ** ), (l ** ):] st Pr[n, x, y];

      end;

      consider pn be FinSequence of [:(l ** ), (l ** ):] such that

       A4: ( len pn) = (( len t) + 1) & ((pn /. 1) = P or (( len t) + 1) = 0 ) & for n be Nat st 1 <= n & n <= ((( len t) + 1) - 1) holds Pr[n, (pn /. n), (pn /. (n + 1))] from RECDEF_1:sch 18( A3);

      defpred Pr1[ Nat] means $1 <= ( len pn) implies ($1 <= ( len t) implies ( rng (pn /. $1)) misses (( rng <*(t /. $1)*>) \/ ( rng (t /^ $1)))) & (pn /. $1) is consistent & ( rng P) c= ( rng (pn /. $1));

      

       A5: for k be non zero Nat st Pr1[k] holds Pr1[(k + 1)]

      proof

        let k be non zero Nat;

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

        

         A6: 1 <= k by NAT_1: 25;

        

         A7: (k + 1) > k by NAT_1: 13;

        assume

         A8: Pr1[k];

        

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

        thus Pr1[(k + 1)]

        proof

          (t /. k1) in {(t /. k1)} by TARSKI:def 1;

          then

           A10: (t /. k1) in ( rng <*(t /. k1)*>) by FINSEQ_1: 39;

          assume

           A11: (k + 1) <= ( len pn);

          then

          reconsider P1 = (pn /. k1) as consistent PNPair by NAT_1: 13, A8;

          set pp = [((P1 `1 ) ^^ <*(t /. k1)*>), (P1 `2 )], pp2 = [(P1 `1 ), ((P1 `2 ) ^^ <*(t /. k1)*>)];

          

           A12: ( rng P1) misses ( rng (t /^ k1)) by XBOOLE_1: 7, XBOOLE_1: 63, A8, A4, A11, XREAL_1: 6, NAT_1: 13;

          ( rng P1) misses ( rng <*(t /. k1)*>) by XBOOLE_1: 63, XBOOLE_1: 7, A8, A4, A11, XREAL_1: 6, NAT_1: 13;

          then

           A13: ( rng (P1 `2 )) misses ( rng <*(t /. k1)*>) by XBOOLE_1: 7, XBOOLE_1: 63;

          

           A14: ( rng P1) misses ( rng <*(t /. k1)*>) by XBOOLE_1: 7, XBOOLE_1: 63, A8, A4, A11, XREAL_1: 6, NAT_1: 13;

          then

           A15: ( rng (P1 `1 )) misses ( rng <*(t /. k1)*>) by XBOOLE_1: 7, XBOOLE_1: 63;

          (( rng P1) /\ ( rng <*(t /. k1)*>)) = {} by A14;

          then

           A16: not (t /. k1) in ( rng P1) by A10, XBOOLE_0:def 4;

          

           A17: ((k + 1) + ( - 1)) <= ((( len t) + 1) + ( - 1)) by A4, A11, XREAL_1: 6;

          then

           A18: k in ( dom t) by FINSEQ_3: 25, A6;

          

           A19: Pr[k1, P1, (pn /. (k1 + 1))] by A4, A6, A17;

          set r1 = [((P1 `1 ) ^^ <*(t /. k1)*>), (pp `2 )], r2 = [(pp2 `1 ), ((P1 `2 ) ^^ <*(t /. k1)*>)];

          per cases ;

            suppose

             A20: pp is consistent;

            

            then

             A21: ( rng (pn /. (k + 1))) = (( rng (r1 `1 )) \/ ( rng (r1 `2 ))) by A19

            .= (( rng ((P1 `1 ) ^ <*(t /. k1)*>)) \/ ( rng (P1 `2 ))) by Def3, A15

            .= ((( rng (P1 `1 )) \/ ( rng <*(t /. k1)*>)) \/ ( rng (P1 `2 ))) by FINSEQ_1: 31

            .= (( rng P1) \/ ( rng <*(t /. k1)*>)) by XBOOLE_1: 4;

            thus (k + 1) <= ( len t) implies ( rng (pn /. (k + 1))) misses (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))))

            proof

              assume

               A22: (k + 1) <= ( len t);

              then ( <*(t . (k + 1))*> ^ (t /^ (k + 1))) = (t /^ k) by Th1;

              then (( rng <*(t . (k + 1))*>) \/ ( rng (t /^ (k + 1)))) = ( rng (t /^ k)) by FINSEQ_1: 31;

              then

               A23: ( rng (t /^ (k + 1))) c= ( rng (t /^ k)) by XBOOLE_1: 7;

              (k + 1) in ( dom t) by FINSEQ_3: 25, A22, A9;

              then {(t /. (k + 1))} c= ( rng (t /^ k)) by FINSEQ_6: 58, A7, ZFMISC_1: 31;

              then ( rng <*(t /. (k + 1))*>) c= ( rng (t /^ k)) by FINSEQ_1: 39;

              then

               A24: (( rng (t /^ (k + 1))) \/ ( rng <*(t /. (k + 1))*>)) c= (( rng (t /^ k)) \/ ( rng (t /^ k))) by XBOOLE_1: 13, A23;

              k1 in ( Seg k1) by A6;

              then (t . k1) in ( rng (t | ( Seg k))) by FUNCT_1: 50, A18;

              then (t /. k1) in ( rng (t | k)) by PARTFUN1:def 6, A18;

              then {(t /. k1)} c= ( rng (t | k)) by ZFMISC_1: 31;

              then ( rng <*(t /. k1)*>) c= ( rng (t | k)) by FINSEQ_1: 39;

              then

               A25: ( rng <*(t /. k1)*>) misses (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1)))) by FINSEQ_5: 34, XBOOLE_1: 64, A24;

              (( rng (pn /. (k + 1))) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))))) = ((( rng P1) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))))) \/ (( rng <*(t /. k1)*>) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1)))))) by XBOOLE_1: 23, A21

              .= ( {} \/ (( rng <*(t /. k1)*>) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1)))))) by A24, XBOOLE_1: 63, A12, XBOOLE_0:def 7

              .= {} by A25;

              hence ( rng (pn /. (k + 1))) misses (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))));

            end;

            thus (pn /. (k + 1)) is consistent by A4, A6, A17, A20;

            ( rng (pn /. k)) c= ( rng (pn /. (k + 1))) by XBOOLE_1: 7, A21;

            hence ( rng P) c= ( rng (pn /. (k + 1))) by A8, A11, NAT_1: 13;

          end;

            suppose not pp is consistent;

            

            then

             A26: ( rng (pn /. (k + 1))) = (( rng (r2 `1 )) \/ ( rng (r2 `2 ))) by A19

            .= (( rng (P1 `1 )) \/ ( rng ((P1 `2 ) ^ <*(t /. k1)*>))) by Def3, A13

            .= (( rng (P1 `1 )) \/ (( rng (P1 `2 )) \/ ( rng <*(t /. k1)*>))) by FINSEQ_1: 31

            .= (( rng P1) \/ ( rng <*(t /. k1)*>)) by XBOOLE_1: 4;

            thus (k + 1) <= ( len t) implies ( rng (pn /. (k + 1))) misses (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))))

            proof

              assume

               A27: (k + 1) <= ( len t);

              then ( <*(t . (k + 1))*> ^ (t /^ (k + 1))) = (t /^ k) by Th1;

              then (( rng <*(t . (k + 1))*>) \/ ( rng (t /^ (k + 1)))) = ( rng (t /^ k)) by FINSEQ_1: 31;

              then

               A28: ( rng (t /^ (k + 1))) c= ( rng (t /^ k)) by XBOOLE_1: 7;

              (k + 1) in ( dom t) by FINSEQ_3: 25, A27, A9;

              then {(t /. (k + 1))} c= ( rng (t /^ k)) by FINSEQ_6: 58, A7, ZFMISC_1: 31;

              then ( rng <*(t /. (k + 1))*>) c= ( rng (t /^ k)) by FINSEQ_1: 39;

              then

               A29: (( rng (t /^ (k + 1))) \/ ( rng <*(t /. (k + 1))*>)) c= (( rng (t /^ k)) \/ ( rng (t /^ k))) by XBOOLE_1: 13, A28;

              k1 in ( Seg k1) by A6;

              then (t . k1) in ( rng (t | ( Seg k))) by FUNCT_1: 50, A18;

              then (t /. k1) in ( rng (t | k)) by PARTFUN1:def 6, A18;

              then {(t /. k1)} c= ( rng (t | k)) by ZFMISC_1: 31;

              then ( rng <*(t /. k1)*>) c= ( rng (t | k)) by FINSEQ_1: 39;

              then

               A30: ( rng <*(t /. k1)*>) misses (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1)))) by FINSEQ_5: 34, XBOOLE_1: 64, A29;

              (( rng (pn /. (k + 1))) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))))) = ((( rng P1) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))))) \/ (( rng <*(t /. k1)*>) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1)))))) by XBOOLE_1: 23, A26

              .= ( {} \/ (( rng <*(t /. k1)*>) /\ (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1)))))) by A29, XBOOLE_1: 63, A12, XBOOLE_0:def 7

              .= {} by A30;

              hence ( rng (pn /. (k + 1))) misses (( rng <*(t /. (k + 1))*>) \/ ( rng (t /^ (k + 1))));

            end;

            thus (pn /. (k + 1)) is consistent by A19, Th31, A16;

            ( rng (pn /. k)) c= ( rng (pn /. (k + 1))) by XBOOLE_1: 7, A26;

            hence ( rng P) c= ( rng (pn /. (k + 1))) by A8, A11, NAT_1: 13;

          end;

        end;

      end;

      reconsider lpn = ( len pn) as non zero Nat by A4;

      

       A31: Pr1[1]

      proof

        assume 1 <= ( len pn);

        thus 1 <= ( len t) implies ( rng (pn /. 1)) misses (( rng <*(t /. 1)*>) \/ ( rng (t /^ 1)))

        proof

          assume 1 <= ( len t);

          then

           A32: t <> {} ;

          (( rng <*(t /. 1)*>) \/ ( rng (t /^ 1))) = ( rng ( <*(t /. 1)*> ^ (t /^ 1))) by FINSEQ_1: 31

          .= ( rng (t :- (t /. 1))) by FINSEQ_6: 43, A32

          .= ( rng t) by FINSEQ_6: 44, A32;

          hence thesis by A4, XBOOLE_1: 79, A1;

        end;

        thus (pn /. 1) is consistent by A4;

        thus ( rng P) c= ( rng (pn /. 1)) by A4;

      end;

      

       A33: for k be non zero Nat holds Pr1[k] from NAT_1:sch 10( A31, A5);

      then (pn /. lpn) is consistent;

      then

      reconsider P2 = (pn /. ( len pn)) as consistent PNPair;

      set i2 = (( len pn) -' 1), P3 = (pn /. lpn);

      

       A34: (( len pn) -' i2) = (( len pn) -' (( len pn) - 1)) by A4, XREAL_0:def 2

      .= (( len pn) - (( len pn) - 1)) by XREAL_0:def 2

      .= 1;

      defpred Pr6[ Nat] means $1 < ( len pn) implies ( rng ((pn /. (( len pn) -' $1)) `1 )) c= ( rng (P2 `1 )) & ( rng ((pn /. (( len pn) -' $1)) `2 )) c= ( rng (P2 `2 ));

       A35:

      now

        let n;

        assume that

         A36: 1 <= n and

         A37: n <= ( len t);

        n <= ( len pn) by A37, NAT_1: 13, A4;

        then ( rng (pn /. n)) misses (( rng <*(t /. n)*>) \/ ( rng (t /^ n))) by A33, A36, A37;

        then

         A38: ( rng (pn /. n)) misses ( rng <*(t /. n)*>) by XBOOLE_1: 7, XBOOLE_1: 63;

        hence ( rng ((pn /. n) `1 )) misses ( rng <*(t /. n)*>) by XBOOLE_1: 7, XBOOLE_1: 63;

        thus ( rng ((pn /. n) `2 )) misses ( rng <*(t /. n)*>) by XBOOLE_1: 7, XBOOLE_1: 63, A38;

      end;

       A39:

      now

        let n be Nat;

        set k = (( len pn) -' (n + 1));

        assume

         A40: Pr6[n];

        thus Pr6[(n + 1)]

        proof

          assume

           A41: (n + 1) < ( len pn);

          then

           A42: ((n + 1) + ( - 1)) < ( len pn) by XREAL_1: 36;

          then

           A43: (n + ( - n)) < (( len pn) + ( - n)) by XREAL_1: 8;

          

           A44: ((n + 1) + ( - (n + 1))) < (( len pn) + ( - (n + 1))) by A41, XREAL_1: 8;

          

          then

           A45: k = (( len pn) - (n + 1)) by XREAL_0:def 2

          .= (( len t) - n) by A4;

          

           A46: (( len pn) - (n + 1)) > 0 by A44;

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

          then

           A47: 1 <= k by NAT_1: 25;

          reconsider k as non zero Element of NAT by XREAL_0:def 2, A46;

          set P1 = (pn /. k);

          

           A48: ( len t) >= (( len t) + ( - n)) by XREAL_1: 32;

          then

           A49: ( rng (P1 `2 )) misses ( rng <*(t /. k)*>) by A35, A47, A45;

          

           A50: ( rng (P1 `1 )) misses ( rng <*(t /. k)*>) by A35, A47, A48, A45;

          

           A51: (k + 1) = ((( len pn) - (n + 1)) + 1) by XREAL_0:def 2

          .= (( len pn) - n)

          .= (( len pn) -' n) by XREAL_0:def 2, A43;

          k < ( len pn) by A4, NAT_1: 13, A48, A45;

          then

           A52: (pn /. k) is consistent PNPair by A33;

          per cases ;

            suppose [((P1 `1 ) ^^ <*(t /. k)*>), (P1 `2 )] is consistent;

            then

             A53: (pn /. (k + 1)) = [((P1 `1 ) ^^ <*(t /. k)*>), (P1 `2 )] by A47, A48, A45, A4, A52;

            then ( rng ((P1 `1 ) ^^ <*(t /. k)*>)) c= ( rng (P2 `1 )) by A40, A42, A51;

            then ( rng ((P1 `1 ) ^ <*(t /. k)*>)) c= ( rng (P2 `1 )) by A50, Def3;

            then

             A54: (( rng (P1 `1 )) \/ ( rng <*(t /. k)*>)) c= ( rng (P2 `1 )) by FINSEQ_1: 31;

            ( rng (P1 `1 )) c= (( rng (P1 `1 )) \/ ( rng <*(t /. k)*>)) by XBOOLE_1: 7;

            hence thesis by A40, A42, A51, A53, A54;

          end;

            suppose not [((P1 `1 ) ^^ <*(t /. k)*>), (P1 `2 )] is consistent;

            then

             A55: (pn /. (k + 1)) = [(P1 `1 ), ((P1 `2 ) ^^ <*(t /. k)*>)] by A47, A48, A45, A4, A52;

            then ( rng ((P1 `2 ) ^^ <*(t /. k)*>)) c= ( rng (P2 `2 )) by A40, A42, A51;

            then ( rng ((P1 `2 ) ^ <*(t /. k)*>)) c= ( rng (P2 `2 )) by A49, Def3;

            then

             A56: (( rng (P1 `2 )) \/ ( rng <*(t /. k)*>)) c= ( rng (P2 `2 )) by FINSEQ_1: 31;

            ( rng (P1 `2 )) c= (( rng (P1 `2 )) \/ ( rng <*(t /. k)*>)) by XBOOLE_1: 7;

            hence thesis by A56, A55, A40, A42, A51;

          end;

        end;

      end;

      

       A57: Pr6[ 0 ]

      proof

        assume 0 < ( len pn);

        then (( len pn) - 0 ) > 0 ;

        hence thesis by XREAL_0:def 2;

      end;

      

       A58: for n be Nat holds Pr6[n] from NAT_1:sch 2( A57, A39);

      then

       A59: (( len pn) + ( - 1)) < ( len pn) & Pr6[i2] by XREAL_1: 30;

      

       A60: ( tau ( rng P)) c= ( rng P2)

      proof

        let x be object;

        assume x in ( tau ( rng P));

        then

         A61: x in (tfp \/ ( rng P)) by XBOOLE_1: 45, Th16;

        per cases by A61, XBOOLE_0:def 3;

          suppose x in tfp;

          then

          consider i be Nat such that

           A62: i in ( dom t) and

           A63: (t . i) = x by A1, FINSEQ_2: 10;

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

          set P5 = (pn /. i1);

          

           A64: i <= ((( len t) + 1) - 1) by FINSEQ_3: 25, A62;

          then

           A65: i < ( len pn) by A4, NAT_1: 13;

          reconsider ii = (( len pn) -' (i + 1)) as Element of NAT ;

          set P3 = (pn /. (( len pn) -' ii));

          (( - 1) * (i + 1)) < (( - 1) * 0 ) by XREAL_1: 69;

          then

           A66: (( len pn) + ( - (i + 1))) < ( len pn) by XREAL_1: 30;

          

           A67: 1 <= i by FINSEQ_3: 25, A62;

          then

           A68: Pr[i1, (pn /. i1), (pn /. (i1 + 1))] by A64, A4;

          

           A69: i <= ( len t) by FINSEQ_3: 25, A62;

          then

           A70: ( rng (P5 `1 )) misses ( rng <*(t /. i)*>) by A35, A67;

          

           A71: ( rng (P5 `2 )) misses ( rng <*(t /. i)*>) by A35, A67, A69;

          (i + 1) <= ( len pn) by XREAL_1: 6, A69, A4;

          then ((i + 1) + ( - (i + 1))) <= (( len pn) + ( - (i + 1))) by XREAL_1: 6;

          then

           A72: ii = (( len pn) - (i + 1)) by XREAL_0:def 2;

          

          then

           A73: (( len pn) -' ii) = (( len pn) - (( len pn) - (i + 1))) by XREAL_0:def 2

          .= (i + 1);

           Pr6[(( len pn) -' (i + 1))] by A58;

          then

           A74: ( rng P3) c= ( rng P2) by A66, A72, XBOOLE_1: 13;

          per cases ;

            suppose

             A75: [((P5 `1 ) ^^ <*(t /. i)*>), (P5 `2 )] is consistent;

            ( rng <*(t /. i)*>) c= (( rng (P5 `1 )) \/ ( rng <*(t /. i)*>)) by XBOOLE_1: 7;

            then ( rng <*(t /. i)*>) c= ( rng ((P5 `1 ) ^ <*(t /. i)*>)) by FINSEQ_1: 31;

            then ( rng <*(t /. i)*>) c= (( rng ((P5 `1 ) ^ <*(t /. i)*>)) \/ ( rng (P5 `2 ))) by XBOOLE_1: 10;

            then ( rng <*(t /. i)*>) c= (( rng ((P5 `1 ) ^^ <*(t /. i)*>)) \/ ( rng (P5 `2 ))) by A70, Def3;

            then ( rng <*(t /. i)*>) c= (( rng (P3 `1 )) \/ ( rng (P5 `2 ))) by A73, A75, A33, A65, A67, A68;

            then ( rng <*(t /. i)*>) c= ( rng P3) by A75, A33, A65, A67, A68, A73;

            then

             A76: ( rng <*(t /. i)*>) c= ( rng P2) by A74;

            (t /. i) in {(t /. i)} by TARSKI:def 1;

            then (t /. i) in ( rng <*(t /. i)*>) by FINSEQ_1: 38;

            then (t /. i) in ( rng P2) by A76;

            hence x in ( rng P2) by A62, A63, PARTFUN1:def 6;

          end;

            suppose

             A77: not [((P5 `1 ) ^^ <*(t /. i)*>), (P5 `2 )] is consistent;

            

             mg: P3 = [(P5 `1 ), ((P5 `2 ) ^^ <*(t /. i)*>)] by A77, A33, A65, A67, A68, A73;

            ( rng <*(t /. i)*>) c= (( rng (P5 `2 )) \/ ( rng <*(t /. i)*>)) by XBOOLE_1: 7;

            then ( rng <*(t /. i)*>) c= ( rng ((P5 `2 ) ^ <*(t /. i)*>)) by FINSEQ_1: 31;

            then ( rng <*(t /. i)*>) c= (( rng (P5 `1 )) \/ ( rng ((P5 `2 ) ^ <*(t /. i)*>))) by XBOOLE_1: 10;

            then ( rng <*(t /. i)*>) c= (( rng (P5 `1 )) \/ ( rng ((P5 `2 ) ^^ <*(t /. i)*>))) by A71, Def3;

            then ( rng <*(t /. i)*>) c= (( rng (P5 `1 )) \/ ( rng (P3 `2 ))) by mg;

            then ( rng <*(t /. i)*>) c= ( rng P3) by mg;

            then

             A78: ( rng <*(t /. i)*>) c= ( rng P2) by A74;

            (t /. i) in {(t /. i)} by TARSKI:def 1;

            then (t /. i) in ( rng <*(t /. i)*>) by FINSEQ_1: 38;

            then (t /. i) in ( rng P2) by A78;

            hence x in ( rng P2) by A62, A63, PARTFUN1:def 6;

          end;

        end;

          suppose

           A79: x in ( rng P);

          ( rng P) c= ( rng (pn /. ( len pn))) by A33, A4;

          hence x in ( rng P2) by A79;

        end;

      end;

      defpred Pr4[ Nat] means $1 <= ( len pn) implies (( rng ((pn /. $1) `1 )) \/ ( rng ((pn /. $1) `2 ))) c= ( tau ( rng P));

      

       A80: tfp c= ( tau ( rng P)) by XBOOLE_1: 36;

      

       A81: for k be non zero Nat st Pr4[k] holds Pr4[(k + 1)]

      proof

        let k be non zero Nat;

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

        

         A82: 1 <= k by NAT_1: 25;

        assume

         A83: Pr4[k];

        thus Pr4[(k + 1)]

        proof

          set P1 = (pn /. k1);

          set P4 = (pn /. k);

          assume

           A84: (k + 1) <= ( len pn);

          then

           A85: ((k + 1) + ( - 1)) <= ((( len t) + 1) + ( - 1)) by A4, XREAL_1: 6;

          then

           A86: ( rng (P1 `2 )) misses ( rng <*(t /. k)*>) by A35, A82;

          

           A87: ( rng (P1 `1 )) misses ( rng <*(t /. k)*>) by A35, A82, A85;

          k < ( len pn) by A84, NAT_1: 13;

          then

           A88: (pn /. k1) is consistent by A33;

          

           A89: {(t /. k1)} c= ( tau ( rng P))

          proof

            let x be object;

            

             A90: k1 in ( dom t) by FINSEQ_3: 25, A82, A85;

            then (t . k1) in ( rng t) by FUNCT_1: 3;

            then

             A91: (t /. k1) in ( rng t) by PARTFUN1:def 6, A90;

            assume x in {(t /. k1)};

            then x in ( rng t) by A91, TARSKI:def 1;

            hence thesis by A1, A80;

          end;

          per cases ;

            suppose

             A92: [((P1 `1 ) ^^ <*(t /. k1)*>), (P1 `2 )] is consistent;

            set P3 = (pn /. (k1 + 1));

            

             A93: (pn /. (k1 + 1)) = [((P1 `1 ) ^^ <*(t /. k1)*>), (P1 `2 )] by A92, A85, A4, A82, A88;

            then

             A94: ( rng (P3 `2 )) = ( rng (P4 `2 ));

            ( rng (P3 `1 )) = ( rng ((P1 `1 ) ^^ <*(t /. k1)*>)) by A93

            .= ( rng ((P1 `1 ) ^ <*(t /. k1)*>)) by A87, Def3

            .= (( rng (P1 `1 )) \/ ( rng <*(t /. k1)*>)) by FINSEQ_1: 31

            .= (( rng (P4 `1 )) \/ {(t /. k1)}) by FINSEQ_1: 38;

            then ( rng P3) = (( rng P4) \/ {(t /. k1)}) by XBOOLE_1: 4, A94;

            hence thesis by XBOOLE_1: 8, A89, A83, A84, NAT_1: 13;

          end;

            suppose

             A95: not [((P1 `1 ) ^^ <*(t /. k1)*>), (P1 `2 )] is consistent;

            set P3 = (pn /. (k1 + 1));

            

             A96: (pn /. (k1 + 1)) = [(P1 `1 ), ((P1 `2 ) ^^ <*(t /. k1)*>)] by A95, A85, A4, A82, A88;

            then

             A97: ( rng (P3 `1 )) = ( rng (P4 `1 ));

            ( rng (P3 `2 )) = ( rng ((P1 `2 ) ^^ <*(t /. k1)*>)) by A96

            .= ( rng ((P1 `2 ) ^ <*(t /. k1)*>)) by Def3, A86

            .= (( rng (P1 `2 )) \/ ( rng <*(t /. k1)*>)) by FINSEQ_1: 31

            .= (( rng (P4 `2 )) \/ {(t /. k1)}) by FINSEQ_1: 38;

            then ( rng P3) = (( rng P4) \/ {(t /. k1)}) by A97, XBOOLE_1: 4;

            hence thesis by XBOOLE_1: 8, A89, A83, A84, NAT_1: 13;

          end;

        end;

      end;

      

       A98: Pr4[1] by Th16, A4;

      for k be non zero Nat holds Pr4[k] from NAT_1:sch 10( A98, A81);

      then ( rng P3) c= ( tau ( rng P));

      hence thesis by A34, A4, A59, XREAL_0:def 2, A60, XBOOLE_0:def 10;

    end;