ltlaxio5.miz



    begin

    theorem :: LTLAXIO5:1

    

     Lm1: for X be set, f be FinSequence of X, i be Nat st 1 <= i & i <= ( len f) holds (f . i) = (f /. i)

    proof

      let X be set, f be FinSequence of X, i be Nat;

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

      then i in ( dom f) by FINSEQ_3: 25;

      hence thesis by PARTFUN1:def 6;

    end;

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

F,G,X for Subset of LTLB_WFF ,

M for LTLModel,

i,j,n for Element of NAT ,

f,f1,f2,g for FinSequence of LTLB_WFF ;

    theorem :: LTLAXIO5:2

    

     mon2: F c= G & F |- A implies G |- A

    proof

      assume

       A0: F c= G & F |- A;

      then

      consider f such that

       A1: (f . ( len f)) = A & 1 <= ( len f) and

       A2: for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i);

      now

        let i be Nat;

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

        per cases by LTLAXIO1:def 29, A2;

          suppose (f . i) in F;

          hence prc (f,G,i) by A0;

        end;

          suppose (f . i) in LTL_axioms or (ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) IND_rule (f /. i))) or ex j be Nat st 1 <= j & j < i & (f /. j) NEX_rule (f /. i);

          hence prc (f,G,i);

        end;

      end;

      hence G |- A by A1;

    end;

    theorem :: LTLAXIO5:3

    

     th16: ((A => B) => ((B => C) => (A => C))) is LTL_TAUT_OF_PL

    proof

      let g be Function of LTLB_WFF , BOOLEAN ;

      set v = ( VAL g);

      

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

      

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

      

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

      

      thus (v . ((A => B) => ((B => C) => (A => C)))) = ((v . (A => B)) => (v . ((B => C) => (A => C)))) by LTLAXIO1:def 15

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

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

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

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

    end;

    theorem :: LTLAXIO5:4

    

     th17: ((A => (B => C)) => ((A => B) => (A => C))) is LTL_TAUT_OF_PL

    proof

      let g be Function of LTLB_WFF , BOOLEAN ;

      set v = ( VAL g);

      

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

      

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

      

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

      

      thus (v . ((A => (B => C)) => ((A => B) => (A => C)))) = ((v . (A => (B => C))) => (v . ((A => B) => (A => C)))) by LTLAXIO1:def 15

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

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

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

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

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

    end;

    theorem :: LTLAXIO5:5

    

     th18: F |- (( 'G' A) => A)

    proof

      

       A1: {A} c= (F \/ {A}) by XBOOLE_1: 7;

      A in {A} by TARSKI:def 1;

      then (F \/ {A}) |- A by A1, LTLAXIO1: 42;

      hence F |- (( 'G' A) => A) by LTLAXIO1: 57;

    end;

    theorem :: LTLAXIO5:6

    

     th19a: {A} |= ( 'G' ( 'X' A))

    proof

      assume not {A} |= ( 'G' ( 'X' A));

      then

      consider M such that

       A1: M |= {A} & not M |= ( 'G' ( 'X' A));

      consider i such that

       A2: not (( SAT M) . [i, ( 'G' ( 'X' A))]) = 1 by A1;

      consider j such that

       A3: not (( SAT M) . [(i + j), ( 'X' A)]) = 1 by A2, LTLAXIO1: 10;

      

       A4: not (( SAT M) . [((i + j) + 1), A]) = 1 by A3, LTLAXIO1: 9;

      A in {A} by TARSKI:def 1;

      then M |= A by A1;

      hence contradiction by A4;

    end;

    theorem :: LTLAXIO5:7

    

     th19: F |- (( 'G' A) => ( 'G' ( 'X' A)))

    proof

       {A} |- ( 'G' ( 'X' A)) by LTLAXIO4: 33, th19a;

      then (F \/ {A}) |- ( 'G' ( 'X' A)) by mon2, XBOOLE_1: 7;

      hence thesis by LTLAXIO1: 57;

    end;

    theorem :: LTLAXIO5:8

    

     th20: F |- (( 'G' (A => B)) => (( 'G' (A => ( 'X' A))) => ( 'G' (A => ( 'G' B)))))

    proof

      (A => B) in {(A => B)} by TARSKI:def 1;

      then (A => B) in (F \/ {(A => B)}) by XBOOLE_0:def 3;

      then (A => B) in ((F \/ {(A => B)}) \/ {(A => ( 'X' A))}) by XBOOLE_0:def 3;

      then

       A1: ((F \/ {(A => B)}) \/ {(A => ( 'X' A))}) |- (A => B) by LTLAXIO1: 42;

      (A => ( 'X' A)) in {(A => ( 'X' A))} by TARSKI:def 1;

      then (A => ( 'X' A)) in ((F \/ {(A => B)}) \/ {(A => ( 'X' A))}) by XBOOLE_0:def 3;

      then ((F \/ {(A => B)}) \/ {(A => ( 'X' A))}) |- (A => ( 'X' A)) by LTLAXIO1: 42;

      then ((F \/ {(A => B)}) \/ {(A => ( 'X' A))}) |- ( 'G' (A => ( 'G' B))) by LTLAXIO1: 45, LTLAXIO1: 54, A1;

      then (F \/ {(A => B)}) |- (( 'G' (A => ( 'X' A))) => ( 'G' (A => ( 'G' B)))) by LTLAXIO1: 57;

      hence thesis by LTLAXIO1: 57;

    end;

    begin

    definition

      let M, A;

      :: LTLAXIO5:def1

      pred M |=0 A means (( SAT M) . [ 0 , A]) = 1;

    end

    definition

      let M, F;

      :: LTLAXIO5:def2

      pred M |=0 F means for A st A in F holds M |=0 A;

    end

    definition

      let F, A;

      :: LTLAXIO5:def3

      pred F |=0 A means for M st M |=0 F holds M |=0 A;

    end

    begin

    theorem :: LTLAXIO5:9

    

     Th1: M |= F implies M |=0 F

    proof

      assume

       Z1: M |= F;

      let A;

      assume A in F;

      then M |= A by Z1;

      hence M |=0 A;

    end;

    theorem :: LTLAXIO5:10

    

     th261b: M |= A iff M |=0 ( 'G' A)

    proof

      hereby

        assume M |= A;

        then for i holds (( SAT M) . [( 0 + i), A]) = 1;

        hence M |=0 ( 'G' A) by LTLAXIO1: 10;

      end;

      assume

       Z2: M |=0 ( 'G' A);

      now

        let i;

        (( SAT M) . [( 0 + i), A]) = 1 by LTLAXIO1: 10, Z2;

        hence (( SAT M) . [i, A]) = 1;

      end;

      hence M |= A;

    end;

    theorem :: LTLAXIO5:11

    

     th262a: F |=0 A implies F |= A

    proof

      assume

       Z1: F |=0 A;

      let M;

      assume

       A1: M |= F;

      let i;

      (M ^\ i) |=0 F by A1, LTLAXIO1: 29, Th1;

      then (M ^\ i) |=0 A by Z1;

      then (( SAT M) . [(i + 0 ), A]) = 1 by LTLAXIO1: 28;

      hence (( SAT M) . [i, A]) = 1;

    end;

    definition

      let F;

      :: LTLAXIO5:def4

      func 'G' F -> Subset of LTLB_WFF equals { ( 'G' A) where A be Element of LTLB_WFF : A in F };

      correctness

      proof

        set s = { ( 'G' A) where A be Element of LTLB_WFF : A in F };

        s c= LTLB_WFF

        proof

          let x be object;

          assume x in s;

          then ex A st x = ( 'G' A) & A in F;

          hence x in LTLB_WFF ;

        end;

        hence thesis;

      end;

    end

    theorem :: LTLAXIO5:12

    

     th261bq: M |= F iff M |=0 ( 'G' F)

    proof

      hereby

        assume

         Z1: M |= F;

        thus M |=0 ( 'G' F)

        proof

          let A;

          assume A in ( 'G' F);

          then

          consider B such that

           A1: A = ( 'G' B) & B in F;

          thus M |=0 A by A1, th261b, Z1;

        end;

      end;

      assume

       Z1: M |=0 ( 'G' F);

      let A;

      assume A in F;

      then ( 'G' A) in ( 'G' F);

      hence M |= A by th261b, Z1;

    end;

    theorem :: LTLAXIO5:13

    

     th262b: F |= A iff ( 'G' F) |=0 A

    proof

      hereby

        assume

         Z1: F |= A;

        thus ( 'G' F) |=0 A

        proof

          let M;

          assume M |=0 ( 'G' F);

          then M |= A by Z1, th261bq;

          hence M |=0 A;

        end;

      end;

      assume

       Z2: ( 'G' F) |=0 A;

      thus F |= A

      proof

        let M;

        assume

         Z3: M |= F;

        let i;

        (M ^\ i) |= F by LTLAXIO1: 29, Z3;

        then (M ^\ i) |=0 A by Z2, th261bq;

        then (( SAT M) . [(i + 0 ), A]) = 1 by LTLAXIO1: 28;

        hence (( SAT M) . [i, A]) = 1;

      end;

    end;

    theorem :: LTLAXIO5:14

    

     th262ac1: {( prop n)} |= ( 'X' ( prop n)) & not {( prop n)} |=0 ( 'X' ( prop n))

    proof

      thus {( prop n)} |= ( 'X' ( prop n))

      proof

        let M;

        assume M |= {( prop n)};

        then

         A2: M |= ( prop n) by LTLAXIO1: 23;

        let i;

        (( SAT M) . [(i + 1), ( prop n)]) = 1 by A2;

        hence (( SAT M) . [i, ( 'X' ( prop n))]) = 1 by LTLAXIO1: 9;

      end;

      thus not {( prop n)} |=0 ( 'X' ( prop n))

      proof

        defpred P[ Element of NAT , Element of ( bool props )] means ($1 = 0 implies $2 = {( prop n)}) & ( not $1 = 0 implies $2 = ( {} LTLB_WFF ));

        

         A3: for x be Element of NAT holds ex y be Element of ( bool props ) st P[x, y]

        proof

          let x be Element of NAT ;

          per cases ;

            suppose

             S1: x = 0 ;

            ( prop n) in props by LTLAXIO1:def 10;

            then

            reconsider p0 = {( prop n)} as Element of ( bool props ) by ZFMISC_1: 31;

             P[x, p0] by S1;

            hence ex y be Element of ( bool props ) st P[x, y];

          end;

            suppose

             S2: not x = 0 ;

            reconsider e = ( {} LTLB_WFF ) as Element of ( bool props ) by XBOOLE_1: 2;

             P[x, e] by S2;

            hence ex y be Element of ( bool props ) st P[x, y];

          end;

        end;

        consider M be Function of NAT , ( bool props ) such that

         A4: for x be Element of NAT holds P[x, (M . x)] from FUNCT_2:sch 3( A3);

        reconsider M as LTLModel;

        

         A5: M |=0 {( prop n)}

        proof

          let A;

          assume A in {( prop n)};

          then

           A6: A = ( prop n) by TARSKI:def 1;

          (M . 0 ) = {( prop n)} by A4;

          then ( prop n) in (M . 0 ) by TARSKI:def 1;

          hence M |=0 A by LTLAXIO1:def 11, A6;

        end;

         not M |=0 ( 'X' ( prop n))

        proof

          assume M |=0 ( 'X' ( prop n));

          then (( SAT M) . [( 0 + 1), ( prop n)]) = 1 by LTLAXIO1: 9;

          then ( prop n) in (M . 1) by LTLAXIO1:def 11;

          hence contradiction by A4;

        end;

        hence thesis by A5;

      end;

    end;

    theorem :: LTLAXIO5:15

    ex F, A st F |= A & not F |=0 A

    proof

       {( prop 0 )} |= ( 'X' ( prop 0 )) & not {( prop 0 )} |=0 ( 'X' ( prop 0 )) by th262ac1;

      hence thesis;

    end;

    theorem :: LTLAXIO5:16

    

     th21: F |=0 ( 'G' A) implies F |= A

    proof

      assume

       Z1: F |=0 ( 'G' A);

      assume not F |= A;

      then

      consider M such that

       A1: M |= F & not M |= A;

      

       A3: M |=0 F

      proof

        let A;

        assume A in F;

        then M |= A by A1;

        hence M |=0 A;

      end;

      consider i such that

       A2: not (( SAT M) . [i, A]) = 1 by A1;

      M |=0 ( 'G' A) by A3, Z1;

      then (( SAT M) . [( 0 + i), A]) = 1 by LTLAXIO1: 10;

      hence contradiction by A2;

    end;

    theorem :: LTLAXIO5:17

    

     th21cp: {( prop i)} |= ( prop i) & not {( prop i)} |=0 ( 'G' ( prop i))

    proof

      thus {( prop i)} |= ( prop i)

      proof

        let M;

        

         A1: ( prop i) in {( prop i)} by TARSKI:def 1;

        assume M |= {( prop i)};

        hence thesis by A1;

      end;

       not {( prop i)} |=0 ( 'X' ( prop i)) by th262ac1;

      then

      consider M such that

       A2: M |=0 {( prop i)} & not M |=0 ( 'X' ( prop i));

       not (( SAT M) . [( 0 + 1), ( prop i)]) = 1 by LTLAXIO1: 9, A2;

      then not M |=0 ( 'G' ( prop i)) by LTLAXIO1: 10;

      hence not {( prop i)} |=0 ( 'G' ( prop i)) by A2;

    end;

    theorem :: LTLAXIO5:18

    ex F, A st (F |= A & not F |=0 ( 'G' A))

    proof

       {( prop 0 )} |= ( prop 0 ) & not {( prop 0 )} |=0 ( 'G' ( prop 0 )) by th21cp;

      hence thesis;

    end;

    theorem :: LTLAXIO5:19

    

     th263pa: M |=0 F & M |=0 G iff M |=0 (F \/ G)

    proof

      hereby

        assume

         A1: M |=0 F & M |=0 G;

        thus M |=0 (F \/ G)

        proof

          let A;

          assume A in (F \/ G);

          then A in F or A in G by XBOOLE_0:def 3;

          hence M |=0 A by A1;

        end;

      end;

      assume

       A2: M |=0 (F \/ G);

      thus M |=0 F

      proof

        let A;

        assume A in F;

        then A in (F \/ G) by XBOOLE_0:def 3;

        hence M |=0 A by A2;

      end;

      let A;

      assume A in G;

      then A in (F \/ G) by XBOOLE_0:def 3;

      hence M |=0 A by A2;

    end;

    theorem :: LTLAXIO5:20

    

     th263pb: M |=0 A iff M |=0 {A}

    proof

      thus M |=0 A implies M |=0 {A} by TARSKI:def 1;

      A in {A} by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: LTLAXIO5:21

    

     th263: (F \/ {A}) |=0 B iff F |=0 (A => B)

    proof

      hereby

        assume

         A3: (F \/ {A}) |=0 B;

        thus F |=0 (A => B)

        proof

          let M;

          assume

           A4: M |=0 F;

          

           A2: (( SAT M) . [ 0 , (A => B)]) = ((( SAT M) . [ 0 , A]) => (( SAT M) . [ 0 , B])) by LTLAXIO1:def 11;

          thus M |=0 (A => B)

          proof

            per cases by XBOOLEAN:def 3;

              suppose (( SAT M) . [ 0 , A]) = 0 ;

              hence (( SAT M) . [ 0 , (A => B)]) = 1 by A2;

            end;

              suppose (( SAT M) . [ 0 , A]) = 1;

              then M |=0 A;

              then M |=0 {A} by th263pb;

              then M |=0 B by A3, th263pa, A4;

              hence (( SAT M) . [ 0 , (A => B)]) = 1 by A2;

            end;

          end;

        end;

      end;

      assume

       A6: F |=0 (A => B);

      let M;

      assume M |=0 (F \/ {A});

      then

       A5: M |=0 F & M |=0 {A} by th263pa;

      then

       A7: M |=0 A by th263pb;

      M |=0 (A => B) by A5, A6;

      then ((( SAT M) . [ 0 , A]) => (( SAT M) . [ 0 , B])) = 1 by LTLAXIO1:def 11;

      hence M |=0 B by A7;

    end;

    theorem :: LTLAXIO5:22

    

     th264p: ( 'G' ( {} LTLB_WFF )) = ( {} LTLB_WFF )

    proof

      thus ( 'G' ( {} LTLB_WFF )) c= ( {} LTLB_WFF )

      proof

        let x be object;

        assume x in ( 'G' ( {} LTLB_WFF ));

        then

        consider A such that

         A1: x = ( 'G' A) & A in ( {} LTLB_WFF );

        thus x in ( {} LTLB_WFF ) by A1;

      end;

      thus ( {} LTLB_WFF ) c= ( 'G' ( {} LTLB_WFF ));

    end;

    theorem :: LTLAXIO5:23

    

     th218: F |= A & (for B st B in F holds ( {} LTLB_WFF ) |= B) implies ( {} LTLB_WFF ) |= A

    proof

      assume

       Z1: F |= A & (for B st B in F holds ( {} LTLB_WFF ) |= B);

      let M;

      assume

       Z2: M |= ( {} LTLB_WFF );

      now

        let B;

        assume B in F;

        then ( {} LTLB_WFF ) |= B by Z1;

        hence M |= B by Z2;

      end;

      then M |= F;

      hence M |= A by Z1;

    end;

    theorem :: LTLAXIO5:24

    

     th265: F |= A & (for B st B in F holds ( {} LTLB_WFF ) |=0 B) implies ( {} LTLB_WFF ) |=0 A

    proof

      assume

       Z1: F |= A & (for B st B in F holds ( {} LTLB_WFF ) |=0 B);

      then for B st B in F holds ( {} LTLB_WFF ) |= B by th262b, th264p;

      hence ( {} LTLB_WFF ) |=0 A by th262b, th264p, th218, Z1;

    end;

    theorem :: LTLAXIO5:25

    ( {} LTLB_WFF ) |=0 A implies ( {} LTLB_WFF ) |=0 ( 'X' A)

    proof

      assume

       Z1: ( {} LTLB_WFF ) |=0 A;

      

       A1: {A} |= A by LTLAXIO1: 23;

      B in {A} implies ( {} LTLB_WFF ) |=0 B by TARSKI:def 1, Z1;

      hence ( {} LTLB_WFF ) |=0 ( 'X' A) by th265, A1, LTLAXIO1: 25;

    end;

    begin

    definition

      :: LTLAXIO5:def5

      func LTL0_axioms -> Subset of LTLB_WFF equals ( 'G' LTL_axioms );

      correctness ;

    end

    definition

      let p, q;

      :: LTLAXIO5:def6

      pred p REFL0_rule q means p = ( 'G' q);

      :: LTLAXIO5:def7

      pred p NEX0_rule q means ex A st p = ( 'G' A) & q = ( 'G' ( 'X' A));

      let r;

      :: LTLAXIO5:def8

      pred p,q MP0_rule r means ex A, B st p = ( 'G' A) & q = ( 'G' (A => B)) & r = ( 'G' B);

      :: LTLAXIO5:def9

      pred p,q IND0_rule r means ex A, B st p = ( 'G' (A => B)) & q = ( 'G' (A => ( 'X' A))) & r = ( 'G' (A => ( 'G' B)));

    end

    definition

      let i be Nat, f, X;

      :: LTLAXIO5:def10

      pred prc0 f,X,i means

      : Def29: (f . i) in LTL0_axioms or (f . i) in X or (ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i))) or ex j be Nat st 1 <= j & j < i & ((f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i));

    end

    theorem :: LTLAXIO5:26

    

     Th38: for i,n be Nat st (n + ( len f)) <= ( len f2) & (for k be Nat st 1 <= k & k <= ( len f) holds (f . k) = (f2 . (k + n))) & 1 <= i & i <= ( len f) holds prc0 (f,X,i) implies prc0 (f2,X,(i + n))

    proof

      let i,n be Nat;

      assume that

       A1: (n + ( len f)) <= ( len f2) and

       A2: for k be Nat st 1 <= k & k <= ( len f) holds (f . k) = (f2 . (k + n)) and

       A3: 1 <= i and

       A4: i <= ( len f);

      (i + n) <= (( len f) + n) by A4, XREAL_1: 6;

      then

       A5: (i + n) <= ( len f2) by A1, XXREAL_0: 2;

      

       A6: (f /. i) = (f . i) by A3, A4, Lm1

      .= (f2 . (i + n)) by A2, A3, A4

      .= (f2 /. (i + n)) by A3, A5, Lm1, NAT_1: 12;

      assume

       A7: prc0 (f,X,i);

      per cases by A7;

        suppose (f . i) in LTL0_axioms ;

        hence prc0 (f2,X,(i + n)) by A2, A3, A4;

      end;

        suppose (f . i) in X;

        hence prc0 (f2,X,(i + n)) by A2, A3, A4;

      end;

        suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i));

        then

        consider j,k be Nat such that

         A8: 1 <= j and

         A9: j < i and

         A10: 1 <= k and

         A11: k < i and

         A12: ((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i);

        

         A13: 1 <= (j + n) & (j + n) < (i + n) by A8, A9, NAT_1: 12, XREAL_1: 8;

        

         A14: k <= ( len f) by A4, A11, XXREAL_0: 2;

        then (k + n) <= (( len f) + n) by XREAL_1: 6;

        then

         A15: (k + n) <= ( len f2) by A1, XXREAL_0: 2;

        

         A16: j <= ( len f) by A4, A9, XXREAL_0: 2;

        then (j + n) <= (( len f) + n) by XREAL_1: 6;

        then

         A17: (j + n) <= ( len f2) by A1, XXREAL_0: 2;

        

         A18: (f /. k) = (f . k) by A10, A14, Lm1

        .= (f2 . (k + n)) by A2, A10, A14

        .= (f2 /. (k + n)) by A10, A15, Lm1, NAT_1: 12;

        

         A19: 1 <= (k + n) & (k + n) < (i + n) by A10, A11, NAT_1: 12, XREAL_1: 8;

        (f /. j) = (f . j) by A8, A16, Lm1

        .= (f2 . (j + n)) by A2, A8, A16

        .= (f2 /. (j + n)) by A8, A17, Lm1, NAT_1: 12;

        hence prc0 (f2,X,(i + n)) by A6, A12, A13, A19, A18;

      end;

        suppose ex j be Nat st 1 <= j & j < i & ((f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i));

        then

        consider j be Nat such that

         A20: 1 <= j and

         A21: j < i and

         A22: (f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i);

        

         A23: 1 <= (j + n) & (j + n) < (i + n) by A20, A21, NAT_1: 12, XREAL_1: 8;

        

         A24: j <= ( len f) by A4, A21, XXREAL_0: 2;

        then (j + n) <= (( len f) + n) by XREAL_1: 6;

        then

         A25: (j + n) <= ( len f2) by A1, XXREAL_0: 2;

        (f /. j) = (f . j) by A20, A24, Lm1

        .= (f2 . (j + n)) by A2, A20, A24

        .= (f2 /. (j + n)) by A20, A25, Lm1, NAT_1: 12;

        hence prc0 (f2,X,(i + n)) by A6, A22, A23;

      end;

    end;

    theorem :: LTLAXIO5:27

    

     Th39: f2 = (f ^ f1) & 1 <= ( len f) & 1 <= ( len f1) & (for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,X,i)) & (for i be Nat st 1 <= i & i <= ( len f1) holds prc0 (f1,X,i)) implies for i be Nat st 1 <= i & i <= ( len f2) holds prc0 (f2,X,i)

    proof

      assume that

       A1: f2 = (f ^ f1) and 1 <= ( len f) and 1 <= ( len f1) and

       A2: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,X,i) and

       A3: for i be Nat st 1 <= i & i <= ( len f1) holds prc0 (f1,X,i);

      

       A4: ( len f2) = (( len f) + ( len f1)) by A1, FINSEQ_1: 22;

      

       A5: for k be Nat st 1 <= k & k <= ( len f1) holds (f1 . k) = (f2 . (k + ( len f))) by A1, FINSEQ_1: 65;

      let i be Nat;

      assume that

       A6: 1 <= i and

       A7: i <= ( len f2);

      per cases by NAT_1: 13;

        suppose

         A8: i <= ( len f);

        

        then

         A9: (f /. i) = (f . i) by A6, Lm1

        .= (f2 . i) by A1, A6, A8, FINSEQ_1: 64

        .= (f2 /. i) by A6, A7, Lm1;

        per cases by A2, A6, A8, Def29;

          suppose (f . i) in LTL0_axioms ;

          hence prc0 (f2,X,i) by A1, A6, A8, FINSEQ_1: 64;

        end;

          suppose (f . i) in X;

          hence prc0 (f2,X,i) by A1, A6, A8, FINSEQ_1: 64;

        end;

          suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i));

          then

          consider j,k be Nat such that

           A10: 1 <= j and

           A11: j < i and

           A12: 1 <= k and

           A13: k < i and

           A14: ((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i);

          

           A15: k <= ( len f) by A8, A13, XXREAL_0: 2;

          then

           A16: k <= ( len f2) by A4, NAT_1: 12;

          

           A17: (f /. k) = (f . k) by A12, A15, Lm1

          .= (f2 . k) by A1, A12, A15, FINSEQ_1: 64

          .= (f2 /. k) by A12, A16, Lm1;

          

           A18: j <= ( len f) by A8, A11, XXREAL_0: 2;

          then

           A19: j <= ( len f2) by A4, NAT_1: 12;

          (f /. j) = (f . j) by A10, A18, Lm1

          .= (f2 . j) by A1, A10, A18, FINSEQ_1: 64

          .= (f2 /. j) by A10, A19, Lm1;

          hence prc0 (f2,X,i) by A9, A10, A11, A12, A13, A14, A17;

        end;

          suppose ex j be Nat st 1 <= j & j < i & ((f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i));

          then

          consider j be Nat such that

           A20: 1 <= j and

           A21: j < i and

           A22: (f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i);

          

           A23: j <= ( len f) by A8, A21, XXREAL_0: 2;

          then

           A24: j <= ( len f2) by A4, NAT_1: 12;

          (f /. j) = (f . j) by A20, A23, Lm1

          .= (f2 . j) by A1, A20, A23, FINSEQ_1: 64

          .= (f2 /. j) by A20, A24, Lm1;

          hence prc0 (f2,X,i) by A9, A20, A21, A22;

        end;

      end;

        suppose

         A25: (( len f) + 1) <= i;

        set i1 = (i -' ( len f));

        i <= (( len f) + ( len f1)) by A1, A7, FINSEQ_1: 22;

        then (i -' ( len f)) <= ((( len f) + ( len f1)) -' ( len f)) by NAT_D: 42;

        then

         A26: i1 <= ( len f1) by NAT_D: 34;

        1 <= i1 by A25, NAT_D: 55;

        then prc0 (f2,X,(i1 + ( len f))) by A3, A4, A5, A26, Th38;

        hence prc0 (f2,X,i) by A25, NAT_D: 43, NAT_D: 55;

      end;

    end;

    definition

      let X, p;

      :: LTLAXIO5:def11

      pred X |-0 p means ex f st (f . ( len f)) = p & 1 <= ( len f) & for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,X,i);

    end

    theorem :: LTLAXIO5:28

    

     Th40: (f = (f1 ^ <*p*>) & 1 <= ( len f1) & for i be Nat st 1 <= i & i <= ( len f1) holds prc0 (f1,X,i)) & prc0 (f,X,( len f)) implies (for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,X,i)) & X |-0 p

    proof

      assume that

       A1: f = (f1 ^ <*p*>) and 1 <= ( len f1) and

       A2: for i be Nat st 1 <= i & i <= ( len f1) holds prc0 (f1,X,i);

      

       A3: ( len f) = (( len f1) + ( len <*p*>)) by A1, FINSEQ_1: 22

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

      assume

       A4: prc0 (f,X,( len f));

      

       A5: ( 0 + ( len f1)) <= ( len f) by A3, NAT_1: 12;

       A6:

      now

        let i be Nat;

        assume that

         A7: 1 <= i and

         A8: i <= ( len f);

        

         A9: i < (( len f1) + 1) or i = (( len f1) + 1) by A3, A8, XXREAL_0: 1;

        

         A10: for k be Nat st 1 <= k & k <= ( len f1) holds (f1 . k) = (f . (k + 0 )) by A1, FINSEQ_1: 64;

        per cases by A3, A9, NAT_1: 13;

          suppose i <= ( len f1);

          then prc0 (f,X,(i + 0 )) by A2, A5, A7, A10, Th38;

          hence prc0 (f,X,i);

        end;

          suppose i = ( len f);

          hence prc0 (f,X,i) by A4;

        end;

      end;

      hence for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,X,i);

      (f . ( len f)) = (f . (( len f1) + ( len <*p*>))) by A1, FINSEQ_1: 22

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

      .= p by A1, FINSEQ_1: 42;

      hence X |-0 p by A3, XREAL_1: 31, A6;

    end;

    begin

    theorem :: LTLAXIO5:29

    

     Th2: A in LTL0_axioms implies F |=0 A

    proof

      assume A in LTL0_axioms ;

      then

      consider B such that

       A8: A = ( 'G' B) & B in LTL_axioms ;

      ( {} LTLB_WFF ) |- B by LTLAXIO1: 42, A8;

      then ( {} LTLB_WFF ) |= ( 'G' B) by LTLAXIO1: 41, LTLAXIO1: 54;

      then

       B1: ( {} LTLB_WFF ) |=0 ( 'G' B) by th262b, th264p;

      let M;

      assume M |=0 F;

      M |=0 ( {} LTLB_WFF );

      hence M |=0 A by B1, A8;

    end;

    theorem :: LTLAXIO5:30

    

     Th3: F |=0 A & F |=0 (A => B) implies F |=0 B

    proof

      assume that

       A1: F |=0 A and

       A2: F |=0 (A => B);

      let M;

      assume

       B3: M |=0 F;

      then M |=0 (A => B) by A2;

      then

       B6: ((( SAT M) . [ 0 , A]) => (( SAT M) . [ 0 , B])) = 1 by LTLAXIO1:def 11;

      M |=0 A by A1, B3;

      hence M |=0 B by B6;

    end;

    theorem :: LTLAXIO5:31

    

     Th4: F |=0 ( 'G' A) & F |=0 ( 'G' (A => B)) implies F |=0 ( 'G' B)

    proof

      assume that

       A1: F |=0 ( 'G' A) and

       A2: F |=0 ( 'G' (A => B));

      let M;

      assume

       B10: M |=0 F;

      then

       B11: M |=0 ( 'G' A) by A1;

      

       B12: M |=0 ( 'G' (A => B)) by B10, A2;

      now

        let i;

        

         B13: (( SAT M) . [( 0 + i), A]) = 1 by B11, LTLAXIO1: 10;

        (( SAT M) . [( 0 + i), (A => B)]) = 1 by B12, LTLAXIO1: 10;

        then ((( SAT M) . [i, A]) => (( SAT M) . [i, B])) = 1 by LTLAXIO1:def 11;

        hence (( SAT M) . [( 0 + i), B]) = 1 by B13;

      end;

      hence M |=0 ( 'G' B) by LTLAXIO1: 10;

    end;

    theorem :: LTLAXIO5:32

    

     Th5: F |=0 ( 'G' A) implies F |=0 ( 'G' ( 'X' A))

    proof

      assume

       A1: F |=0 ( 'G' A);

      let M;

      assume M |=0 F;

      then

       A3: M |=0 ( 'G' A) by A1;

      now

        let i be Element of NAT ;

        (( SAT M) . [( 0 + (i + 1)), A]) = 1 by LTLAXIO1: 10, A3;

        hence (( SAT M) . [( 0 + i), ( 'X' A)]) = 1 by LTLAXIO1: 9;

      end;

      hence M |=0 ( 'G' ( 'X' A)) by LTLAXIO1: 10;

    end;

    theorem :: LTLAXIO5:33

    

     Th6: F |=0 ( 'G' A) implies F |=0 A

    proof

      assume

       Z1: F |=0 ( 'G' A);

      let M;

      assume M |=0 F;

      then M |=0 ( 'G' A) by Z1;

      then (( SAT M) . [( 0 + 0 ), A]) = 1 by LTLAXIO1: 10;

      hence (( SAT M) . [ 0 , A]) = 1;

    end;

    theorem :: LTLAXIO5:34

    

     Th7: F |=0 ( 'G' (A => B)) & F |=0 ( 'G' (A => ( 'X' A))) implies F |=0 ( 'G' (A => ( 'G' B)))

    proof

      assume that

       A1: F |=0 ( 'G' (A => B)) and

       A2: F |=0 ( 'G' (A => ( 'X' A)));

      let M;

      assume

       A3: M |=0 F;

      now

        let n be Element of NAT ;

        defpred P1[ Nat] means (( SAT M) . [(n + $1), A]) = 1;

        per cases by XBOOLEAN:def 3;

          suppose

           A4: (( SAT M) . [n, A]) = 1;

          

           A5: for k be Nat st P1[k] holds P1[(k + 1)]

          proof

            let k be Nat such that

             A6: P1[k];

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

            M |=0 ( 'G' (A => ( 'X' A))) by A2, A3;

            then (( SAT M) . [( 0 + (n + kk)), (A => ( 'X' A))]) = 1 by LTLAXIO1: 10;

            then ((( SAT M) . [(n + kk), A]) => (( SAT M) . [(n + kk), ( 'X' A)])) = 1 by LTLAXIO1:def 11;

            then (( SAT M) . [((n + kk) + 1), A]) = 1 by A6, LTLAXIO1: 9;

            hence P1[(k + 1)];

          end;

          

           A7: P1[ 0 ] by A4;

          

           A8: for i be Nat holds P1[i] from NAT_1:sch 2( A7, A5);

          now

            let i be Element of NAT ;

            M |=0 ( 'G' (A => B)) by A1, A3;

            then (( SAT M) . [( 0 + (n + i)), (A => B)]) = 1 by LTLAXIO1: 10;

            then

             A9: ((( SAT M) . [(n + i), A]) => (( SAT M) . [(n + i), B])) = 1 by LTLAXIO1:def 11;

            (( SAT M) . [(n + i), A]) = 1 by A8;

            hence (( SAT M) . [(n + i), B]) = 1 by A9;

          end;

          then (( SAT M) . [n, ( 'G' B)]) = 1 by LTLAXIO1: 10;

          then ((( SAT M) . [n, A]) => (( SAT M) . [n, ( 'G' B)])) = 1;

          hence (( SAT M) . [( 0 + n), (A => ( 'G' B))]) = 1 by LTLAXIO1:def 11;

        end;

          suppose (( SAT M) . [n, A]) = 0 ;

          then ((( SAT M) . [n, A]) => (( SAT M) . [n, ( 'G' B)])) = 1;

          hence (( SAT M) . [( 0 + n), (A => ( 'G' B))]) = 1 by LTLAXIO1:def 11;

        end;

      end;

      hence M |=0 ( 'G' (A => ( 'G' B))) by LTLAXIO1: 10;

    end;

    ::$Notion-Name

    theorem :: LTLAXIO5:35

    

     th266: F |-0 A implies F |=0 A

    proof

      assume F |-0 A;

      then

      consider f such that

       A1: (f . ( len f)) = A and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies F |=0 (f /. $1);

      

       A4: for i be Nat st for j be Nat st j < i holds P[j] holds P[i]

      proof

        let i be Nat;

        assume

         A5: for j be Nat st j < i holds P[j];

        per cases by NAT_1: 14;

          suppose i = 0 ;

          hence P[i];

        end;

          suppose not i < 1;

          assume that

           A6: 1 <= i and

           A7: i <= ( len f);

          per cases by A3, A6, A7, Def29;

            suppose (f . i) in LTL0_axioms ;

            then (f /. i) in LTL0_axioms by Lm1, A6, A7;

            hence F |=0 (f /. i) by Th2;

          end;

            suppose (f . i) in F;

            then

             A9: (f /. i) in F by A6, A7, Lm1;

            thus F |=0 (f /. i)

            proof

              let M;

              assume M |=0 F;

              hence M |=0 (f /. i) by A9;

            end;

          end;

            suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i));

            then

            consider j,k be Nat such that

             A10: 1 <= j and

             A11: j < i and

             A12: 1 <= k and

             A13: k < i and

             A14: ((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i);

            

             A15: k <= ( len f) by A7, A13, XXREAL_0: 2;

            then

             A15a: F |=0 (f /. k) by A5, A12, A13;

            

             A16: j <= ( len f) by A7, A11, XXREAL_0: 2;

            

             B5: F |=0 (f /. j) by A5, A10, A11, A16;

            per cases by A14;

              suppose ((f /. j),(f /. k)) MP_rule (f /. i);

              then F |=0 ((f /. j) => (f /. i)) by A15, A5, A12, A13;

              hence F |=0 (f /. i) by A5, A10, A11, A16, Th3;

            end;

              suppose ((f /. j),(f /. k)) MP0_rule (f /. i);

              then

              consider A, B such that

               B7: (f /. j) = ( 'G' A) and

               B8: (f /. k) = ( 'G' (A => B)) and

               B9: (f /. i) = ( 'G' B);

              thus F |=0 (f /. i) by Th4, B7, B8, B9, A15a, B5;

            end;

              suppose ((f /. j),(f /. k)) IND0_rule (f /. i);

              then

              consider A, B such that

               A17: (f /. j) = ( 'G' (A => B)) and

               A18: (f /. k) = ( 'G' (A => ( 'X' A))) & (f /. i) = ( 'G' (A => ( 'G' B)));

              F |=0 ( 'G' (A => B)) by A5, A10, A11, A16, A17;

              hence F |=0 (f /. i) by A15a, A18, Th7;

            end;

          end;

            suppose ex j be Nat st 1 <= j & j < i & ((f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i));

            then

            consider j be Nat such that

             A19: 1 <= j and

             A20: j < i and

             A21: (f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i);

            

             B11: j <= ( len f) by A7, A20, XXREAL_0: 2;

            per cases by A21;

              suppose (f /. j) NEX0_rule (f /. i);

              then

              consider A, B such that

               B7: (f /. j) = ( 'G' A) and

               B9: (f /. i) = ( 'G' ( 'X' A));

              thus F |=0 (f /. i) by Th5, B7, B9, B11, A5, A20, A19;

            end;

              suppose (f /. j) REFL0_rule (f /. i);

              hence F |=0 (f /. i) by Th6, B11, A5, A20, A19;

            end;

          end;

        end;

      end;

      

       A22: for i be Nat holds P[i] from NAT_1:sch 4( A4);

      (f /. ( len f)) = A by A1, A2, Lm1;

      hence F |=0 A by A2, A22;

    end;

    begin

    theorem :: LTLAXIO5:36

    

     th10: A in LTL0_axioms or A in F implies F |-0 A

    proof

      defpred P1[ set, set] means $2 = A;

      

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

      consider g such that

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

      

       A3: ( len g) = 1 by A2, FINSEQ_1:def 3;

      1 in ( Seg 1);

      then

       A4: (g . 1) = A by A2;

      assume

       A5: A in LTL0_axioms or A in F;

      for j be Nat st 1 <= j & j <= ( len g) holds prc0 (g,F,j)

      proof

        let j be Nat;

        assume

         A6: 1 <= j & j <= ( len g);

        per cases by A5;

          suppose A in LTL0_axioms ;

          hence thesis by A3, A4, A6, XXREAL_0: 1;

        end;

          suppose A in F;

          hence thesis by A3, A4, A6, XXREAL_0: 1;

        end;

      end;

      hence F |-0 A by A3, A4;

    end;

    theorem :: LTLAXIO5:37

    

     th9: F |-0 ( 'G' A) implies F |-0 A

    proof

      assume F |-0 ( 'G' A);

      then

      consider f such that

       A1: (f . ( len f)) = ( 'G' A) and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i);

      set g = (f ^ <*A*>);

      

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

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

      then

       A5: ( len f) < ( len g) by NAT_1: 16;

      

      then

       A6: (g /. ( len f)) = (g . ( len f)) by A2, Lm1

      .= ( 'G' A) by A1, A2, FINSEQ_1: 64;

      1 <= ( len g) by A2, A4, NAT_1: 16;

      

      then (g /. ( len g)) = (g . ( len g)) by Lm1

      .= A by A4, FINSEQ_1: 42;

      then (g /. ( len f)) REFL0_rule (g /. ( len g)) by A6;

      then prc0 (g,F,( len g)) by A2, A5;

      hence F |-0 A by A2, A3, Th40;

    end;

    theorem :: LTLAXIO5:38

    

     th12: F |-0 ( 'G' A) implies F |-0 ( 'G' ( 'X' A))

    proof

      assume F |-0 ( 'G' A);

      then

      consider f such that

       A1: (f . ( len f)) = ( 'G' A) and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i);

      set g = (f ^ <*( 'G' ( 'X' A))*>);

      

       A4: ( len g) = (( len f) + ( len <*( 'G' ( 'X' A))*>)) by FINSEQ_1: 22

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

      then

       A5: ( len f) < ( len g) by NAT_1: 16;

      

      then

       A6: (g /. ( len f)) = (g . ( len f)) by A2, Lm1

      .= ( 'G' A) by A1, A2, FINSEQ_1: 64;

      1 <= ( len g) by A2, A4, NAT_1: 16;

      

      then (g /. ( len g)) = (g . ( len g)) by Lm1

      .= ( 'G' ( 'X' A)) by A4, FINSEQ_1: 42;

      then (g /. ( len f)) NEX0_rule (g /. ( len g)) by A6;

      then prc0 (g,F,( len g)) by A2, A5;

      hence F |-0 ( 'G' ( 'X' A)) by A2, A3, Th40;

    end;

    theorem :: LTLAXIO5:39

    

     th11a: F |-0 A & F |-0 (A => B) implies F |-0 B

    proof

      assume that

       A1: F |-0 A and

       A2: F |-0 (A => B);

      consider f such that

       A3: (f . ( len f)) = A and

       A4: 1 <= ( len f) and

       A5: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i) by A1;

      consider g such that

       A6: (g . ( len g)) = (A => B) and

       A7: 1 <= ( len g) and

       A8: for i be Nat st 1 <= i & i <= ( len g) holds prc0 (g,F,i) by A2;

      

       A9: for i be Nat st 1 <= i & i <= ( len (f ^ g)) holds prc0 ((f ^ g),F,i) by A4, A5, A7, A8, Th39;

      set h = ((f ^ g) ^ <*B*>);

      

       A10: h = (f ^ (g ^ <*B*>)) by FINSEQ_1: 32;

      

       A11: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      then

       A12: 1 <= ( len (f ^ g)) by A4, NAT_1: 12;

      

       A13: ( len h) = (( len (f ^ g)) + ( len <*B*>)) by FINSEQ_1: 22

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

      then 1 <= ( len h) by A4, A11, NAT_1: 16;

      

      then

       A14: (h /. ( len h)) = (h . ( len h)) by Lm1

      .= B by A13, FINSEQ_1: 42;

      ( len h) = (( len f) + (( len g) + 1)) by A11, A13;

      then

       A15: ( len f) < ( len h) by NAT_1: 16;

      

      then

       A16: (h /. ( len f)) = (h . ( len f)) by A4, Lm1

      .= A by A3, A4, A10, FINSEQ_1: 64;

      

       A17: ( len (f ^ g)) < ( len h) by A13, NAT_1: 16;

      

      then (h /. ( len (f ^ g))) = (h . ( len (f ^ g))) by A12, Lm1

      .= ((f ^ g) . ( len (f ^ g))) by A12, FINSEQ_1: 64

      .= ((f ^ g) . (( len f) + ( len g))) by FINSEQ_1: 22

      .= (A => B) by A6, A7, FINSEQ_1: 65;

      then ((h /. ( len f)),(h /. ( len (f ^ g)))) MP_rule (h /. ( len h)) by A16, A14;

      then prc0 (h,F,( len h)) by A4, A12, A15, A17;

      hence F |-0 B by A12, A9, Th40;

    end;

    theorem :: LTLAXIO5:40

    

     th11: F |-0 ( 'G' A) & F |-0 ( 'G' (A => B)) implies F |-0 ( 'G' B)

    proof

      assume that

       A1: F |-0 ( 'G' A) and

       A2: F |-0 ( 'G' (A => B));

      consider f such that

       A3: (f . ( len f)) = ( 'G' A) and

       A4: 1 <= ( len f) and

       A5: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i) by A1;

      consider g such that

       A6: (g . ( len g)) = ( 'G' (A => B)) and

       A7: 1 <= ( len g) and

       A8: for i be Nat st 1 <= i & i <= ( len g) holds prc0 (g,F,i) by A2;

      

       A9: for i be Nat st 1 <= i & i <= ( len (f ^ g)) holds prc0 ((f ^ g),F,i) by A4, A5, A7, A8, Th39;

      set h = ((f ^ g) ^ <*( 'G' B)*>);

      

       A10: h = (f ^ (g ^ <*( 'G' B)*>)) by FINSEQ_1: 32;

      

       A11: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      then

       A12: 1 <= ( len (f ^ g)) by A4, NAT_1: 12;

      

       A13: ( len h) = (( len (f ^ g)) + ( len <*( 'G' B)*>)) by FINSEQ_1: 22

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

      then 1 <= ( len h) by A4, A11, NAT_1: 16;

      

      then

       A14: (h /. ( len h)) = (h . ( len h)) by Lm1

      .= ( 'G' B) by A13, FINSEQ_1: 42;

      ( len h) = (( len f) + (( len g) + 1)) by A11, A13;

      then

       A15: ( len f) < ( len h) by NAT_1: 16;

      

      then

       A16: (h /. ( len f)) = (h . ( len f)) by A4, Lm1

      .= ( 'G' A) by A3, A4, A10, FINSEQ_1: 64;

      

       A17: ( len (f ^ g)) < ( len h) by A13, NAT_1: 16;

      

      then (h /. ( len (f ^ g))) = (h . ( len (f ^ g))) by A12, Lm1

      .= ((f ^ g) . ( len (f ^ g))) by A12, FINSEQ_1: 64

      .= ((f ^ g) . (( len f) + ( len g))) by FINSEQ_1: 22

      .= ( 'G' (A => B)) by A6, A7, FINSEQ_1: 65;

      then ((h /. ( len f)),(h /. ( len (f ^ g)))) MP0_rule (h /. ( len h)) by A16, A14;

      then prc0 (h,F,( len h)) by A4, A12, A15, A17;

      hence F |-0 ( 'G' B) by A12, A9, Th40;

    end;

    theorem :: LTLAXIO5:41

    

     th13: F |-0 ( 'G' (A => B)) & F |-0 ( 'G' (A => ( 'X' A))) implies F |-0 ( 'G' (A => ( 'G' B)))

    proof

      assume that

       A1: F |-0 ( 'G' (A => B)) and

       A2: F |-0 ( 'G' (A => ( 'X' A)));

      consider f such that

       A3: (f . ( len f)) = ( 'G' (A => B)) and

       A4: 1 <= ( len f) and

       A5: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i) by A1;

      consider g such that

       A6: (g . ( len g)) = ( 'G' (A => ( 'X' A))) and

       A7: 1 <= ( len g) and

       A8: for i be Nat st 1 <= i & i <= ( len g) holds prc0 (g,F,i) by A2;

      

       A9: for i be Nat st 1 <= i & i <= ( len (f ^ g)) holds prc0 ((f ^ g),F,i) by A4, A5, A7, A8, Th39;

      set h = ((f ^ g) ^ <*( 'G' (A => ( 'G' B)))*>);

      

       A10: h = (f ^ (g ^ <*( 'G' (A => ( 'G' B)))*>)) by FINSEQ_1: 32;

      

       A11: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      then

       A12: 1 <= ( len (f ^ g)) by A4, NAT_1: 12;

      

       A13: ( len h) = (( len (f ^ g)) + ( len <*( 'G' (A => ( 'G' B)))*>)) by FINSEQ_1: 22

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

      then 1 <= ( len h) by A4, A11, NAT_1: 16;

      

      then

       A14: (h /. ( len h)) = (h . ( len h)) by Lm1

      .= ( 'G' (A => ( 'G' B))) by A13, FINSEQ_1: 42;

      ( len h) = (( len f) + (( len g) + 1)) by A11, A13;

      then

       A15: ( len f) < ( len h) by NAT_1: 16;

      

      then

       A16: (h /. ( len f)) = (h . ( len f)) by A4, Lm1

      .= ( 'G' (A => B)) by A3, A4, A10, FINSEQ_1: 64;

      

       A17: ( len (f ^ g)) < ( len h) by A13, NAT_1: 16;

      

      then (h /. ( len (f ^ g))) = (h . ( len (f ^ g))) by A12, Lm1

      .= ((f ^ g) . ( len (f ^ g))) by A12, FINSEQ_1: 64

      .= ((f ^ g) . (( len f) + ( len g))) by FINSEQ_1: 22

      .= ( 'G' (A => ( 'X' A))) by A6, A7, FINSEQ_1: 65;

      then ((h /. ( len f)),(h /. ( len (f ^ g)))) IND0_rule (h /. ( len h)) by A16, A14;

      then prc0 (h,F,( len h)) by A4, A12, A15, A17;

      hence F |-0 ( 'G' (A => ( 'G' B))) by A12, A9, Th40;

    end;

    theorem :: LTLAXIO5:42

    

     th15: A in LTL_axioms implies F |-0 A

    proof

      assume A in LTL_axioms ;

      then ( 'G' A) in LTL0_axioms ;

      then F |-0 ( 'G' A) by th10;

      hence F |-0 A by th9;

    end;

    theorem :: LTLAXIO5:43

    A in LTL0_axioms implies F |- A

    proof

      assume A in LTL0_axioms ;

      then

      consider B such that

       A1: A = ( 'G' B) & B in LTL_axioms ;

      F |- B by A1, LTLAXIO1: 42;

      hence F |- A by A1, LTLAXIO1: 54;

    end;

    theorem :: LTLAXIO5:44

    

     th267: ( {} LTLB_WFF ) |- A implies ( {} LTLB_WFF ) |-0 A

    proof

      assume ( {} LTLB_WFF ) |- A;

      then

      consider f such that

       A1: (f . ( len f)) = A and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc (f,( {} LTLB_WFF ),i);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies ( {} LTLB_WFF ) |-0 ( 'G' (f /. $1));

      

       A4: for i be Nat st for j be Nat st j < i holds P[j] holds P[i]

      proof

        let i be Nat;

        assume

         A5: for j be Nat st j < i holds P[j];

        per cases by NAT_1: 14;

          suppose i = 0 ;

          hence P[i];

        end;

          suppose not i < 1;

          assume that

           A6: 1 <= i and

           A7: i <= ( len f);

          per cases by A3, A6, A7, LTLAXIO1:def 29;

            suppose (f . i) in LTL_axioms ;

            then (f /. i) in LTL_axioms by Lm1, A6, A7;

            then ( 'G' (f /. i)) in LTL0_axioms ;

            hence thesis by th10;

          end;

            suppose (f . i) in ( {} LTLB_WFF );

            hence thesis;

          end;

            suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) IND_rule (f /. i));

            then

            consider j,k be Nat such that

             A15: 1 <= j and

             A16: j < i and

             A17: 1 <= k and

             A18: k < i and

             A19: ((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) IND_rule (f /. i);

            j <= ( len f) by A7, A16, XXREAL_0: 2;

            then

             A20: ( {} LTLB_WFF ) |-0 ( 'G' (f /. j)) by A5, A15, A16;

            k <= ( len f) by A7, A18, XXREAL_0: 2;

            then

             A21: ( {} LTLB_WFF ) |-0 ( 'G' (f /. k)) by A5, A17, A18;

            per cases by A19;

              suppose ((f /. j),(f /. k)) MP_rule (f /. i);

              hence thesis by A20, A21, th11;

            end;

              suppose ((f /. j),(f /. k)) IND_rule (f /. i);

              then

              consider B, C such that

               A24: (f /. j) = (B => C) and

               A25: (f /. k) = (B => ( 'X' B)) and

               A26: (f /. i) = (B => ( 'G' C));

              thus thesis by A24, A25, A26, th13, A20, A21;

            end;

          end;

            suppose ex j be Nat st 1 <= j & j < i & (f /. j) NEX_rule (f /. i);

            then

            consider j be Nat such that

             A15: 1 <= j and

             A16: j < i and

             A19: (f /. j) NEX_rule (f /. i);

            j <= ( len f) by A7, A16, XXREAL_0: 2;

            then ( {} LTLB_WFF ) |-0 ( 'G' (f /. j)) by A5, A15, A16;

            hence thesis by A19, th12;

          end;

        end;

      end;

      

       A37: for i be Nat holds P[i] from NAT_1:sch 4( A4);

      A = (f /. ( len f)) by A1, A2, Lm1;

      then ( {} LTLB_WFF ) |-0 ( 'G' A) by A37, A2;

      hence ( {} LTLB_WFF ) |-0 A by th9;

    end;

    theorem :: LTLAXIO5:45

    

     th14: {( prop i)} |- ( 'X' ( prop i)) & not {( prop i)} |-0 ( 'X' ( prop i))

    proof

      ( prop i) in {( prop i)} by TARSKI:def 1;

      then {( prop i)} |- ( prop i) by LTLAXIO1: 42;

      hence {( prop i)} |- ( 'X' ( prop i)) by LTLAXIO1: 44;

      thus not {( prop i)} |-0 ( 'X' ( prop i)) by th266, th262ac1;

    end;

    theorem :: LTLAXIO5:46

    

     mon: F c= G & F |-0 A implies G |-0 A

    proof

      assume

       A0: F c= G & F |-0 A;

      then

      consider f such that

       A1: (f . ( len f)) = A & 1 <= ( len f) and

       A2: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,F,i);

      now

        let i be Nat;

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

        per cases by Def29, A2;

          suppose (f . i) in F;

          hence prc0 (f,G,i) by A0;

        end;

          suppose (f . i) in LTL0_axioms or (ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i))) or ex j be Nat st 1 <= j & j < i & ((f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i));

          hence prc0 (f,G,i);

        end;

      end;

      hence G |-0 A by A1;

    end;

    definition

      let f, A;

      :: LTLAXIO5:def12

      func implications (f,A) -> FinSequence of LTLB_WFF means

      : imps: ( len it ) = ( len f) & (it . 1) = ((f /. 1) => A) & for i st 1 <= i & i < ( len f) holds (it . (i + 1)) = ((f /. (i + 1)) => (it /. i)) if ( len f) > 0

      otherwise it = ( <*> LTLB_WFF );

      existence

      proof

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

         A1:

        now

          let n be Nat;

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

          let x be Element of LTLB_WFF ;

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

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

        end;

        consider p be FinSequence of LTLB_WFF such that

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

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

        proof

          assume

           A3: ( len f) > 0 ;

          take p;

          now

            let i;

            assume

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

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

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

          end;

          hence thesis by A2, A3;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of LTLB_WFF ;

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

        proof

          assume that

           A5: ( len f) > 0 and

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

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

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

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

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

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

          

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

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

          

          then

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

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

           A14:

          now

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

            let n;

            set m = (n -' 1);

            assume n in ( dom f1);

            then

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

            then 1 <= n by FINSEQ_1: 1;

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

            then

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

            then

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

            

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

            proof

              let i be Nat;

              assume

               A19: P[i];

              assume

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

              

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

              per cases by NAT_1: 25;

                suppose i = 0 ;

                

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

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

              end;

                suppose i >= 1;

                

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

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

                

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

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

              end;

            end;

            

             A23: P[ 0 ] by A7, A10;

            

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

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

          end;

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

          hence thesis by A14, PARTFUN1: 5;

        end;

        thus thesis;

      end;

      consistency ;

    end

    ::$Notion-Name

    theorem :: LTLAXIO5:47

    

     th268: for F be finite Subset of LTLB_WFF holds F |=0 A implies F |-0 A

    proof

      let F be finite Subset of LTLB_WFF ;

      assume

       Z1: F |=0 A;

      per cases ;

        suppose

         S1: F is empty;

        then F |= A by th262b, th264p, Z1;

        hence F |-0 A by th267, S1, LTLAXIO4: 33;

      end;

        suppose

         S2: not F is empty;

        consider f be FinSequence such that

         A4: ( rng f) = F & f is one-to-one by FINSEQ_4: 58;

        reconsider f as FinSequence of LTLB_WFF by A4, FINSEQ_1:def 4;

        

         A6: 1 <= ( len f) by RELAT_1: 38, A4, FINSEQ_1: 20, S2;

        then 1 <= ( len ( implications (f,A))) by imps;

        then

         A7: (( implications (f,A)) /. 1) = (( implications (f,A)) . 1) by FINSEQ_4: 15;

        

         AA: 1 in ( dom f) by A6, FINSEQ_3: 25;

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies ( rng (f /^ $1)) |=0 (( implications (f,A)) /. $1);

        ( rng (f | 1)) = ( rng <*(f . 1)*>) by FINSEQ_5: 20, RELAT_1: 38, A4, S2

        .= ( rng <*(f /. 1)*>) by PARTFUN1:def 6, AA;

        

        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 ( implications (f,A))) = ( len f) by A6, imps;

         A10:

        now

          let i be Nat;

          

           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 ;

              ((f /. 1) => A) = (( implications (f,A)) . 1) by imps, A6

              .= (( implications (f,A)) /. 1) by FINSEQ_4: 15, A9, A6;

              hence ( rng (f /^ (i + 1))) |=0 (( implications (f,A)) /. (i + 1)) by A8, A4, Z1, th263, 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)))) |=0 (( implications (f,A)) /. i) by A12, A16, NAT_1: 13, A14, FINSEQ_5: 31;

              then (( rng <*(f /. (i + 1))*>) \/ ( rng (f /^ (i + 1)))) |=0 (( implications (f,A)) /. i) by FINSEQ_1: 31;

              then

               A17: (( rng (f /^ (i + 1))) \/ {(f /. (i + 1))}) |=0 (( implications (f,A)) /. i) by FINSEQ_1: 38;

              

               A18: i < ( len f) by NAT_1: 13, A14;

              (( implications (f,A)) /. (i + 1)) = (( implications (f,A)) . (i + 1)) by FINSEQ_4: 15, A13, A14, A9

              .= ((f /. (i + 1)) => (( implications (f,A)) /. i)) by imps, A16, A18, A11;

              hence ( rng (f /^ (i + 1))) |=0 (( implications (f,A)) /. (i + 1)) by A17, th263;

            end;

          end;

        end;

        

         A19: P[ 0 ];

        for i be Nat holds P[i] from NAT_1:sch 2( A19, A10);

        then ( rng (f /^ ( len f))) |=0 (( implications (f,A)) /. ( len f)) by A6;

        then ( {} LTLB_WFF ) |=0 (( implications (f,A)) /. ( len f)) by RFINSEQ: 27, RELAT_1: 38;

        then

         D2: ( {} LTLB_WFF ) |- (( implications (f,A)) /. ( len f)) by LTLAXIO4: 33, th262b, th264p;

        defpred P[ Nat] means $1 < ( len f) implies ( rng f) |-0 (( implications (f,A)) /. (( len f) -' $1));

         A21:

        now

          let i be Nat;

          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 ( implications (f,A))) by A29, A25, imps;

            

            then

             E5: (( implications (f,A)) /. (( len f) -' i)) = (( implications (f,A)) . (j + 1)) by A28, FINSEQ_4: 15, NAT_1: 11

            .= ((f /. (j + 1)) => (( implications (f,A)) /. j)) by imps, A26, A30;

            

             E9: (j + 1) in ( dom f) by FINSEQ_3: 25, NAT_1: 11, A29, A25;

            then (f . (j + 1)) in ( rng f) by FUNCT_1: 3;

            then (f /. (j + 1)) in ( rng f) by PARTFUN1:def 6, E9;

            then ( rng f) |-0 (f /. (j + 1)) by th10;

            hence ( rng f) |-0 (( implications (f,A)) /. j) by th11a, E5, A22, A23, NAT_1: 12;

          end;

        end;

        ( {} LTLB_WFF ) c= ( rng f);

        then

         D3: ( rng f) |-0 (( implications (f,A)) /. ( len f)) by mon, D2, th267;

        (( len f) - 0 ) >= 1 by RELAT_1: 38, A4, S2, FINSEQ_1: 20;

        then

         A33: P[ 0 ] by D3, XREAL_0:def 2;

        

         A34: for i be Nat holds P[i] from NAT_1:sch 2( A33, A21);

        (1 + ( - 1)) <= (( len f) + ( - 1)) by XREAL_1: 6, FINSEQ_1: 20, RELAT_1: 38, A4, S2;

        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) -' i) = (( len f) - i) by XREAL_0:def 2

        .= 1;

        then ( rng f) |-0 (( implications (f,A)) /. 1) by A34, A32;

        then

         C2: F |-0 ((f /. 1) => A) by A4, imps, A7, A6;

        

         C3: 1 in ( dom f) by A6, FINSEQ_3: 25;

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

        then (f /. 1) in ( rng f) by PARTFUN1:def 6, C3;

        then F |-0 (f /. 1) by A4, th10;

        hence F |-0 A by C2, th11a;

      end;

    end;

    begin

    theorem :: LTLAXIO5:48

    (F \/ {A}) |-0 B implies F |-0 (A => B)

    proof

      assume (F \/ {A}) |-0 B;

      then

      consider f such that

       A1: (f . ( len f)) = B and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc0 (f,(F \/ {A}),i);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies F |-0 (A => (f /. $1));

      

       A4: for i be Nat st for j be Nat st j < i holds P[j] holds P[i]

      proof

        let i be Nat;

        assume

         A5: for j be Nat st j < i holds P[j];

        per cases by NAT_1: 14;

          suppose i = 0 ;

          hence P[i];

        end;

          suppose not i < 1;

          assume that

           A6: 1 <= i and

           A7: i <= ( len f);

          per cases by A3, A6, A7, Def29;

            suppose

             A8: (f . i) in LTL0_axioms ;

            

             A9: F |-0 ((f /. i) => (A => (f /. i))) by th15, LTLAXIO1: 34;

            (f /. i) in LTL0_axioms by A6, A7, A8, Lm1;

            then F |-0 (f /. i) by th10;

            hence thesis by A9, th11a;

          end;

            suppose

             A10: (f . i) in (F \/ {A});

            per cases by A10, XBOOLE_0:def 3;

              suppose

               A11: (f . i) in F;

              

               A12: F |-0 ((f /. i) => (A => (f /. i))) by th15, LTLAXIO1: 34;

              (f /. i) in F by A6, A7, A11, Lm1;

              then F |-0 (f /. i) by th10;

              hence thesis by A12, th11a;

            end;

              suppose (f . i) in {A};

              then (f . i) = A by TARSKI:def 1;

              then

               B1: (f /. i) = A by A6, A7, Lm1;

              (A => A) is LTL_TAUT_OF_PL by LTLAXIO2: 24;

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

              hence thesis by B1, th15;

            end;

          end;

            suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i));

            then

            consider j,k be Nat such that

             A15: 1 <= j and

             A16: j < i and

             A17: 1 <= k and

             A18: k < i and

             A19: ((f /. j),(f /. k)) MP_rule (f /. i) or ((f /. j),(f /. k)) MP0_rule (f /. i) or ((f /. j),(f /. k)) IND0_rule (f /. i);

            j <= ( len f) by A7, A16, XXREAL_0: 2;

            then

             A20: F |-0 (A => (f /. j)) by A5, A15, A16;

            k <= ( len f) by A7, A18, XXREAL_0: 2;

            then

             A21: F |-0 (A => (f /. k)) by A5, A17, A18;

            per cases by A19;

              suppose

               A22: ((f /. j),(f /. k)) MP_rule (f /. i);

              

               A23: F |-0 ((A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))) by th15, LTLAXIO1: 35;

              F |-0 ((A => (f /. j)) => (A => (f /. i))) by A23, th11a, A21, A22;

              hence F |-0 (A => (f /. i)) by A20, th11a;

            end;

              suppose ((f /. j),(f /. k)) MP0_rule (f /. i);

              then

              consider C, D such that

               A24: (f /. j) = ( 'G' C) and

               A25: (f /. k) = ( 'G' (C => D)) and

               A26: (f /. i) = ( 'G' D);

              

               B1: ( {} LTLB_WFF ) c= F;

              ( {} LTLB_WFF ) |-0 ((f /. k) => ((f /. j) => (f /. i))) by th267, LTLAXIO1: 60, A24, A25, A26;

              then

               B2: F |-0 ((f /. k) => ((f /. j) => (f /. i))) by mon, B1;

              ((A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i))))) is LTL_TAUT_OF_PL by th16;

              then ((A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i))))) in LTL_axioms by LTLAXIO1:def 17;

              then F |-0 ((A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i))))) by th15;

              then F |-0 (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) by th11a, A21;

              then

               B3: F |-0 (A => ((f /. j) => (f /. i))) by B2, th11a;

              ((A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))) is LTL_TAUT_OF_PL by th17;

              then ((A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))) in LTL_axioms by LTLAXIO1:def 17;

              then F |-0 ((A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))) by th15;

              then F |-0 ((A => (f /. j)) => (A => (f /. i))) by th11a, B3;

              hence F |-0 (A => (f /. i)) by th11a, A20;

            end;

              suppose ((f /. j),(f /. k)) IND0_rule (f /. i);

              then

              consider C, D such that

               A24: (f /. j) = ( 'G' (C => D)) and

               A25: (f /. k) = ( 'G' (C => ( 'X' C))) and

               A26: (f /. i) = ( 'G' (C => ( 'G' D)));

              ((A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k))))) is LTL_TAUT_OF_PL by LTLAXIO2: 40;

              then ((A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k))))) in LTL_axioms by LTLAXIO1:def 17;

              then F |-0 ((A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k))))) by th15;

              then F |-0 ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) by th11a, A20;

              then

               B10: F |-0 (A => ((f /. j) '&&' (f /. k))) by th11a, A21;

              

               B12: ( {} LTLB_WFF ) c= F;

              ( {} LTLB_WFF ) |- ((f /. j) => ((f /. k) => (f /. i))) by th20, A24, A25, A26;

              then ( {} LTLB_WFF ) |- (((f /. j) '&&' (f /. k)) => (f /. i)) by LTLAXIO1: 48;

              then

               B11: F |-0 (((f /. j) '&&' (f /. k)) => (f /. i)) by mon, B12, th267;

              ((A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i)))) is LTL_TAUT_OF_PL by th16;

              then ((A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i)))) in LTL_axioms by LTLAXIO1:def 17;

              then F |-0 ((A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i)))) by th15;

              then F |-0 ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) by th11a, B10;

              hence thesis by th11a, B11;

            end;

          end;

            suppose ex j be Nat st 1 <= j & j < i & ((f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i));

            then

            consider j be Nat, q, r such that

             A32: 1 <= j and

             A33: j < i and

             A34: (f /. j) NEX0_rule (f /. i) or (f /. j) REFL0_rule (f /. i);

            

             B4: j <= ( len f) by A7, A33, XXREAL_0: 2;

            then

             B4a: F |-0 (A => (f /. j)) by A5, A32, A33;

            per cases by A34;

              suppose (f /. j) NEX0_rule (f /. i);

              then

              consider C such that

               A24: (f /. j) = ( 'G' C) and

               A26: (f /. i) = ( 'G' ( 'X' C));

              

               B8: ( {} LTLB_WFF ) c= F;

              ( {} LTLB_WFF ) |-0 ((f /. j) => (f /. i)) by th19, th267, A24, A26;

              then

               B9: F |-0 ((f /. j) => (f /. i)) by mon, B8;

              ((A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i)))) is LTL_TAUT_OF_PL by th16;

              then ((A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i)))) in LTL_axioms by LTLAXIO1:def 17;

              then F |-0 ((A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i)))) by th15;

              then F |-0 (((f /. j) => (f /. i)) => (A => (f /. i))) by th11a, B4a;

              hence thesis by B9, th11a;

            end;

              suppose (f /. j) REFL0_rule (f /. i);

              then

               B6: F |-0 (A => ( 'G' (f /. i))) by B4, A5, A32, A33;

              

               B5: ( {} LTLB_WFF ) c= F;

              ( {} LTLB_WFF ) |-0 (( 'G' (f /. i)) => (f /. i)) by th267, th18;

              then

               B7: F |-0 (( 'G' (f /. i)) => (f /. i)) by mon, B5;

              ((A => ( 'G' (f /. i))) => ((( 'G' (f /. i)) => (f /. i)) => (A => (f /. i)))) is LTL_TAUT_OF_PL by th16;

              then ((A => ( 'G' (f /. i))) => ((( 'G' (f /. i)) => (f /. i)) => (A => (f /. i)))) in LTL_axioms by LTLAXIO1:def 17;

              then F |-0 ((A => ( 'G' (f /. i))) => ((( 'G' (f /. i)) => (f /. i)) => (A => (f /. i)))) by th15;

              then F |-0 ((( 'G' (f /. i)) => (f /. i)) => (A => (f /. i))) by B6, th11a;

              hence thesis by th11a, B7;

            end;

          end;

        end;

      end;

      

       A37: for i be Nat holds P[i] from NAT_1:sch 4( A4);

      B = (f /. ( len f)) by A1, A2, Lm1;

      hence F |-0 (A => B) by A2, A37;

    end;

    theorem :: LTLAXIO5:49

    F |-0 (A => B) implies (F \/ {A}) |-0 B

    proof

      A in {A} by TARSKI:def 1;

      then A in (F \/ {A}) by XBOOLE_0:def 3;

      then

       A1: (F \/ {A}) |-0 A by th10;

      assume F |-0 (A => B);

      then (F \/ {A}) |-0 (A => B) by mon, XBOOLE_1: 7;

      hence (F \/ {A}) |-0 B by A1, th11a;

    end;

    begin

    registration

      let F be finite Subset of LTLB_WFF ;

      cluster ( 'G' F) -> finite;

      coherence

      proof

        deffunc H( Element of LTLB_WFF ) = ( 'G' $1);

        

         A1: F is finite;

        { H(w) where w be Element of LTLB_WFF : w in F } is finite from FRAENKEL:sch 21( A1);

        hence ( 'G' F) is finite;

      end;

    end

    theorem :: LTLAXIO5:50

    for F be finite Subset of LTLB_WFF holds (F |- A iff ( 'G' F) |-0 A)

    proof

      let F be finite Subset of LTLB_WFF ;

      hereby

        assume F |- A;

        then F |= A by LTLAXIO1: 41;

        hence ( 'G' F) qua finite Subset of LTLB_WFF |-0 A by th268, th262b;

      end;

      assume ( 'G' F) |-0 A;

      then ( 'G' F) |=0 A by th266;

      hence F |- A by LTLAXIO4: 33, th262b;

    end;

    theorem :: LTLAXIO5:51

    for F be finite Subset of LTLB_WFF holds (F |-0 A implies F |- A)

    proof

      let F be finite Subset of LTLB_WFF ;

      assume F |-0 A;

      then F |=0 A by th266;

      hence F |- A by LTLAXIO4: 33, th262a;

    end;

    theorem :: LTLAXIO5:52

     {( prop i)} |- ( 'G' ( prop i)) & not {( prop i)} |-0 ( 'G' ( prop i))

    proof

      thus {( prop i)} |- ( 'G' ( prop i))

      proof

        ( prop i) in {( prop i)} by TARSKI:def 1;

        then {( prop i)} |- ( prop i) by LTLAXIO1: 42;

        hence thesis by LTLAXIO1: 54;

      end;

      thus not {( prop i)} |-0 ( 'G' ( prop i))

      proof

        assume {( prop i)} |-0 ( 'G' ( prop i));

        then

         A2: {( prop i)} |=0 ( 'G' ( prop i)) by th266;

         not {( prop i)} |=0 ( 'X' ( prop i)) by th268, th14;

        then

        consider M such that

         A1: M |=0 {( prop i)} & not M |=0 ( 'X' ( prop i));

        M |=0 ( 'G' ( prop i)) by A2, A1;

        then (( SAT M) . [( 0 + 1), ( prop i)]) = 1 by LTLAXIO1: 10;

        hence contradiction by LTLAXIO1: 9, A1;

      end;

    end;

    theorem :: LTLAXIO5:53

    for F be finite Subset of LTLB_WFF holds (F |-0 ( 'G' A) implies F |- A)

    proof

      let F be finite Subset of LTLB_WFF ;

      assume F |-0 ( 'G' A);

      then F |=0 ( 'G' A) by th266;

      hence F |- A by LTLAXIO4: 33, th21;

    end;

    theorem :: LTLAXIO5:54

     {( prop i)} |- ( prop i) & not {( prop i)} |-0 ( 'G' ( prop i))

    proof

      ( prop i) in {( prop i)} by TARSKI:def 1;

      hence {( prop i)} |- ( prop i) by LTLAXIO1: 42;

      thus not {( prop i)} |-0 ( 'G' ( prop i)) by th266, th21cp;

    end;