ltlaxio1.miz

begin



 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 ( Seg ( len f)) by FINSEQ_1: 1;

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

 hence thesis by PARTFUN1:def 6;

 end;

 reserve a,b,c for boolean object;

 theorem :: LTLAXIO1:1



 Th1: ((a => (b '&' c)) => (a => b)) = 1

 proof



 A1: b = 0 or b = 1 by XBOOLEAN:def 3;

 a = 0 or a = 1 by XBOOLEAN:def 3;

 hence ((a => (b '&' c)) => (a => b)) = 1 by A1;

 end;

 theorem :: LTLAXIO1:2



 Th2: ((a => (b => c)) => ((a '&' b) => c)) = 1

 proof



 A1: a = 0 or a = 1 by XBOOLEAN:def 3;



 A2: b = 0 or b = 1 by XBOOLEAN:def 3;

 c = 0 or c = 1 by XBOOLEAN:def 3;

 hence thesis by A1, A2;

 end;

 theorem :: LTLAXIO1:3



 Th3: (((a '&' b) => c) => (a => (b => c))) = 1

 proof



 A1: a = 0 or a = 1 by XBOOLEAN:def 3;



 A2: b = 0 or b = 1 by XBOOLEAN:def 3;

 c = 0 or c = 1 by XBOOLEAN:def 3;

 hence thesis by A1, A2;

 end;

 begin

 notation

 synonym LTLB_WFF for HP-WFF ;

 end

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

F,G,X,Y for Subset of LTLB_WFF ,

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

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

 notation

 synonym TFALSUM for VERUM ;

 end

 notation

 let p, q;

 synonym p 'U' q for p '&' q;

 end

 theorem :: LTLAXIO1:4



 Th4: for A holds A = TFALSUM or ex n st A = ( prop n) or ex p, q st A = (p => q) or ex p, q st A = (p 'U' q)

 proof

 let A;

 A = VERUM or A is simple or A is conjunctive or A is conditional by HILBERT2: 9;

 hence thesis by HILBERT2:def 6, HILBERT2:def 7, HILBERT2:def 8;

 end;

 definition

 let p;

 :: LTLAXIO1:def1

 func 'not' p -> Element of LTLB_WFF equals (p => TFALSUM );

 correctness ;

 :: LTLAXIO1:def2

 func 'X' p -> Element of LTLB_WFF equals ( TFALSUM 'U' p);

 correctness ;

 end

 definition

 :: LTLAXIO1:def3

 func TVERUM -> Element of LTLB_WFF equals ( 'not' TFALSUM );

 correctness ;

 end

 definition

 let p, q;

 :: LTLAXIO1:def4

 func p '&&' q -> Element of LTLB_WFF equals ( 'not' (p => ( 'not' q)));

 correctness ;

 end

 definition

 let p, q;

 :: LTLAXIO1:def5

 func p 'or' q -> Element of LTLB_WFF equals ( 'not' (( 'not' p) '&&' ( 'not' q)));

 correctness ;

 end

 definition

 let p;

 :: LTLAXIO1:def6

 func 'G' p -> Element of LTLB_WFF equals ( 'not' (( 'not' p) 'or' ( TVERUM 'U' ( 'not' p))));

 correctness ;

 end

 definition

 let p;

 :: LTLAXIO1:def7

 func 'F' p -> Element of LTLB_WFF equals ( 'not' ( 'G' ( 'not' p)));

 correctness ;

 end

 definition

 let p, q;

 :: LTLAXIO1:def8

 func p 'Uw' q -> Element of LTLB_WFF equals (q 'or' (p '&&' (p 'U' q)));

 correctness ;

 end

 definition

 let p, q;

 :: LTLAXIO1:def9

 func p 'R' q -> Element of LTLB_WFF equals ( 'not' (( 'not' p) 'Uw' ( 'not' q)));

 correctness ;

 end

 begin

 definition

 :: LTLAXIO1:def10

 func props -> Subset of LTLB_WFF means for x be set holds x in it iff ex n be Element of NAT st x = ( prop n);

 existence

 proof

 defpred P1[ object] means ex n be Element of NAT st $1 = ( prop n);

 consider X be set such that

 A1: for x be object holds (x in X iff x in LTLB_WFF & P1[x]) from XBOOLE_0:sch 1;

 X c= LTLB_WFF by A1;

 then

 reconsider X as Subset of LTLB_WFF ;

 take X;

 thus for x be set holds (x in X iff ex n be Element of NAT st x = ( prop n)) by A1;

 end;

 uniqueness

 proof

 let A,B be Subset of LTLB_WFF such that

 A2: for x be set holds x in A iff ex n be Element of NAT st x = ( prop n) and

 A3: for x be set holds x in B iff ex n be Element of NAT st x = ( prop n);



 A4: B c= A

 proof

 let x be object;

 assume x in B;

 then

 consider n be Element of NAT such that

 A5: x = ( prop n) by A3;

 thus x in A by A2, A5;

 end;

 A c= B

 proof

 let x be object;

 assume x in A;

 then

 consider n be Element of NAT such that

 A6: x = ( prop n) by A2;

 thus x in B by A3, A6;

 end;

 hence A = B by A4, XBOOLE_0:def 10;

 end;

 end

 definition

 mode LTLModel is sequence of ( bool props );

 end

 reserve M for LTLModel;

 definition

 let M be LTLModel;

 :: LTLAXIO1:def11

 func SAT M -> Function of [: NAT , LTLB_WFF :], BOOLEAN means

 : Def11: for n holds (it . [n, TFALSUM ]) = 0 & (for k holds (it . [n, ( prop k)]) = 1 iff ( prop k) in (M . n)) & for p, q holds (it . [n, (p => q)]) = ((it . [n, p]) => (it . [n, q])) & ((it . [n, (p 'U' q)]) = 1 iff ex i st 0 < i & (it . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (it . [(n + j), p]) = 1);

 existence

 proof

 set FNB = ( Funcs ( NAT , BOOLEAN ));

 defpred I[ Element of LTLB_WFF , Element of LTLB_WFF , set, set, set] means ($3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN implies ex s3,s4,s5 be sequence of BOOLEAN st s3 = $3 & s4 = $4 & s5 = $5 & for n holds (s5 . n) = ((s3 . n) => (s4 . n))) & ( not ($3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN ) implies $5 = ( NAT --> FALSE ));

 defpred C[ Element of LTLB_WFF , Element of LTLB_WFF , set, set, set] means ($3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN implies ex s3,s4,s5 be sequence of BOOLEAN st s3 = $3 & s4 = $4 & s5 = $5 & for n holds ((s5 . n) = 1 iff (ex i st 0 FALSE ));

 defpred P1[ Element of NAT , Function] means for n holds (($2 . n) = 1 iff ( prop $1) in (M . n));



 A1: for p, q holds for a,b be set holds ex d be set st C[p, q, a, b, d]

 proof

 let p, q;

 let a,b be set;

 per cases ;

 suppose a is sequence of BOOLEAN & b is sequence of BOOLEAN ;

 then

 reconsider a1 = a, b1 = b as sequence of BOOLEAN ;

 defpred PP[ Element of NAT , Element of BOOLEAN ] means $2 = 1 iff (ex i st 0 < i & (b1 . ($1 + i)) = 1 & for j st 1 <= j & j < i holds (a1 . ($1 + j)) = 1);

 A2:

 now

 let n;

 per cases ;

 suppose ex i st 0 < i & (b1 . (n + i)) = 1 & for j st 1 <= j & j < i holds (a1 . (n + j)) = 1;

 hence ex y be Element of BOOLEAN st PP[n, y];

 end;

 suppose not ex i st 0 < i & (b1 . (n + i)) = 1 & for j st 1 <= j & j < i holds (a1 . (n + j)) = 1;

 then PP[n, FALSE ];

 hence ex y be Element of BOOLEAN st PP[n, y];

 end;

 end;

 consider c be sequence of BOOLEAN such that

 A3: for n holds PP[n, (c . n)] from FUNCT_2:sch 3( A2);

 thus thesis by A3;

 end;

 suppose not (a is sequence of BOOLEAN & b is sequence of BOOLEAN );

 hence thesis;

 end;

 end;



 A4: for p, q holds for a,b,c,d be set st C[p, q, a, b, c] & C[p, q, a, b, d] holds c = d

 proof

 let p, q;

 let a,b,c,d be set;

 assume that

 A5: C[p, q, a, b, c] and

 A6: C[p, q, a, b, d];

 per cases ;

 suppose

 A7: a is sequence of BOOLEAN & b is sequence of BOOLEAN ;

 then

 consider s31,s41,s51 be sequence of BOOLEAN such that

 A8: s31 = a & s41 = b and

 A9: s51 = d and

 A10: for n holds ((s51 . n) = 1 iff ex i st 0 < i & (s41 . (n + i)) = 1 & for j st 1 <= j & j < i holds (s31 . (n + j)) = 1) by A6;

 consider s3,s4,s5 be sequence of BOOLEAN such that

 A11: s3 = a & s4 = b and

 A12: s5 = c and

 A13: for n holds ((s5 . n) = 1 iff ex i st 0 < i & (s4 . (n + i)) = 1 & for j st 1 <= j & j < i holds (s3 . (n + j)) = 1) by A5, A7;

 now

 let x be object;

 assume x in NAT ;

 then

 reconsider x1 = x as Element of NAT ;

 per cases by XBOOLEAN:def 3;

 suppose

 A14: (s5 . x1) = 1;

 then ex i st 0 < i & (s41 . (x1 + i)) = 1 & for j st 1 <= j & j < i holds (s31 . (x1 + j)) = 1 by A11, A13, A8;

 hence (s5 . x) = (s51 . x) by A10, A14;

 end;

 suppose

 A15: (s5 . x1) = 0 ;

 then not ex i st 0 < i & (s41 . (x1 + i)) = 1 & for j st 1 <= j & j < i holds (s31 . (x1 + j)) = 1 by A11, A13, A8;

 hence (s5 . x) = (s51 . x) by A15, XBOOLEAN:def 3, A10;

 end;

 end;

 hence c = d by A12, A9, FUNCT_2: 12;

 end;

 suppose not (a is sequence of BOOLEAN & b is sequence of BOOLEAN );

 hence c = d by A5, A6;

 end;

 end;



 A16: for x be Element of NAT holds ex y be Element of ( Funcs ( NAT , BOOLEAN )) st P1[x, y]

 proof

 let x be Element of NAT ;

 defpred P2[ Element of NAT , Element of BOOLEAN ] means $2 = 1 iff ( prop x) in (M . $1);

 A17:

 now

 let x1 be Element of NAT ;

 per cases ;

 suppose ( prop x) in (M . x1);

 then P2[x1, TRUE ];

 hence ex y1 be Element of BOOLEAN st P2[x1, y1];

 end;

 suppose not ( prop x) in (M . x1);

 then P2[x1, FALSE ];

 hence ex y1 be Element of BOOLEAN st P2[x1, y1];

 end;

 end;

 consider y be sequence of BOOLEAN such that

 A18: for n holds P2[n, (y . n)] from FUNCT_2:sch 3( A17);

 reconsider y as Element of ( Funcs ( NAT , BOOLEAN )) by FUNCT_2: 8;

 P1[x, y] by A18;

 hence ex y be Element of ( Funcs ( NAT , BOOLEAN )) st P1[x, y];

 end;

 consider f1 be sequence of ( Funcs ( NAT , BOOLEAN )) such that

 A19: for k holds P1[k, (f1 . k)] from FUNCT_2:sch 3( A16);



 A20: for p, q holds for a,b,c,d be set st I[p, q, a, b, c] & I[p, q, a, b, d] holds c = d

 proof

 let p, q;

 let a,b,c,d be set;

 assume that

 A21: I[p, q, a, b, c] and

 A22: I[p, q, a, b, d];

 per cases ;

 suppose

 A23: a is sequence of BOOLEAN & b is sequence of BOOLEAN ;

 then

 consider s31,s41,s51 be sequence of BOOLEAN such that

 A24: s31 = a and

 A25: s41 = b and

 A26: s51 = d and

 A27: for n holds (s51 . n) = ((s31 . n) => (s41 . n)) by A22;

 consider s3,s4,s5 be sequence of BOOLEAN such that

 A28: s3 = a and

 A29: s4 = b and

 A30: s5 = c and

 A31: for n holds (s5 . n) = ((s3 . n) => (s4 . n)) by A21, A23;

 now

 let x be object;

 assume x in NAT ;

 then

 reconsider x1 = x as Element of NAT ;



 thus (s5 . x) = ((s31 . x1) => (s4 . x1)) by A28, A31, A24

 .= (s51 . x) by A29, A25, A27;

 end;

 hence c = d by A30, A26, FUNCT_2: 12;

 end;

 suppose not (a is sequence of BOOLEAN & b is sequence of BOOLEAN );

 hence c = d by A21, A22;

 end;

 end;

 deffunc P( Element of NAT ) = (f1 . $1);



 A32: for p, q holds for a,b be set holds ex d be set st I[p, q, a, b, d]

 proof

 let p, q;

 let a,b be set;

 per cases ;

 suppose a is sequence of BOOLEAN & b is sequence of BOOLEAN ;

 then

 reconsider a1 = a, b1 = b as sequence of BOOLEAN ;

 deffunc F3( Element of NAT ) = ( 'not' ((a1 . $1) '&' ( 'not' (b1 . $1))));

 consider d be sequence of BOOLEAN such that

 A33: for n holds (d . n) = F3(n) from FUNCT_2:sch 4;

 for n holds (d . n) = ((a1 . n) => (b1 . n)) by A33;

 hence thesis;

 end;

 suppose not (a is sequence of BOOLEAN & b is sequence of BOOLEAN );

 hence thesis;

 end;

 end;

 consider sat be ManySortedSet of LTLB_WFF such that

 A34: (sat . TFALSUM ) = ( NAT --> FALSE ) & (for n holds (sat . ( prop n)) = P(n)) & for p, q holds C[p, q, (sat . p), (sat . q), (sat . (p 'U' q))] & I[p, q, (sat . p), (sat . q), (sat . (p => q))] from HILBERT2:sch 3( A1, A32, A4, A20);

 A35:

 now

 A36:

 now

 let A, B;



 A37: I[A, B, (sat . A), (sat . B), (sat . (A => B))] by A34;

 per cases ;

 suppose (sat . A) is sequence of BOOLEAN & (sat . B) is sequence of BOOLEAN ;

 then

 consider s3,s4,s5 be sequence of BOOLEAN such that s3 = (sat . A) and s4 = (sat . B) and

 A38: s5 = (sat . (A => B)) and for n holds (s5 . n) = ((s3 . n) => (s4 . n)) by A34;

 thus (sat . (A => B)) in FNB by A38, FUNCT_2: 8;

 end;

 suppose not ((sat . A) is sequence of BOOLEAN & (sat . B) is sequence of BOOLEAN );

 thus (sat . (A => B)) in FNB by A37, FUNCT_2: 8;

 end;

 end;

 A39:

 now

 let A, B;



 A40: C[A, B, (sat . A), (sat . B), (sat . (A 'U' B))] by A34;

 per cases ;

 suppose (sat . A) is sequence of BOOLEAN & (sat . B) is sequence of BOOLEAN ;

 then

 consider s3,s4,s5 be sequence of BOOLEAN such that s3 = (sat . A) and s4 = (sat . B) and

 A41: s5 = (sat . (A 'U' B)) and for n holds ((s5 . n) = 1 iff ex i st 0 < i & (s4 . (n + i)) = 1 & for j st 1 <= j & j < i holds (s3 . (n + j)) = 1) by A34;

 thus (sat . (A 'U' B)) in FNB by A41, FUNCT_2: 8;

 end;

 suppose not ((sat . A) is sequence of BOOLEAN & (sat . B) is sequence of BOOLEAN );

 thus (sat . (A 'U' B)) in FNB by A40, FUNCT_2: 8;

 end;

 end;

 let x be object;

 assume x in LTLB_WFF ;

 then

 reconsider x1 = x as Element of LTLB_WFF ;

 A42:

 now

 let n;

 (sat . ( prop n)) = (f1 . n) by A34;

 hence (sat . ( prop n)) in FNB;

 end;

 per cases by Th4;

 suppose x1 = TFALSUM ;

 hence (sat . x) in FNB by A34, FUNCT_2: 8;

 end;

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

 hence (sat . x) in FNB by A42;

 end;

 suppose ex p,q be Element of LTLB_WFF st x1 = (p 'U' q);

 hence (sat . x) in FNB by A39;

 end;

 suppose ex p,q be Element of LTLB_WFF st x1 = (p => q);

 hence (sat . x) in FNB by A36;

 end;

 end;

 ( dom sat) = LTLB_WFF by PARTFUN1:def 2;

 then

 reconsider sat as Function of LTLB_WFF , ( Funcs ( NAT , BOOLEAN )) by A35, FUNCT_2: 3;

 deffunc satpom( Element of NAT , Element of LTLB_WFF ) = ((sat . $2) . $1);

 consider sat2 be Function of [: NAT , LTLB_WFF :], BOOLEAN such that

 A43: for n, A holds (sat2 . (n,A)) = satpom(n,A) from BINOP_1:sch 4;

 A44:

 now

 let A, n;



 thus (sat2 . [n, A]) = (sat2 . (n,A)) by BINOP_1:def 1

 .= ((sat . A) . n) by A43;

 end;

 A45:

 now

 let k, n;

 (sat2 . [n, ( prop k)]) = ((sat . ( prop k)) . n) by A44

 .= ((f1 . k) . n) by A34;

 hence (sat2 . [n, ( prop k)]) = 1 iff ( prop k) in (M . n) by A19;

 end;

 A46:

 now

 let p, q, n;

 reconsider satp = (sat . p), satq = (sat . q) as sequence of BOOLEAN by FUNCT_2: 66;

 consider s31,s41,s51 be sequence of BOOLEAN such that

 A47: s31 = satp and

 A48: s41 = satq and

 A49: s51 = (sat . (p 'U' q)) and

 A50: for n holds ((s51 . n) = 1 iff ex i st 0 < i & (s41 . (n + i)) = 1 & for j st 1 <= j & j q)) & for n holds (s5 . n) = ((s3 . n) => (s4 . n)) by A34;



 thus (sat2 . [n, (p => q)]) = ((sat . (p => q)) . n) by A44

 .= (((sat . p) . n) => (s4 . n)) by A51, A53

 .= ((sat2 . [n, p]) => ((sat . q) . n)) by A44, A52

 .= ((sat2 . [n, p]) => (sat2 . [n, q])) by A44;

 thus (sat2 . [n, (p 'U' q)]) = 1 iff ex i st 0 < i & (sat2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (sat2 . [(n + j), p]) = 1

 proof

 hereby

 assume (sat2 . [n, (p 'U' q)]) = 1;

 then (s51 . n) = 1 by A44, A49;

 then

 consider i such that

 A54: 0 < i and

 A55: (s41 . (n + i)) = 1 and

 A56: for j st 1 <= j & j < i holds (s31 . (n + j)) = 1 by A50;

 A57:

 now

 let j;

 assume

 A58: 1 <= j & j < i;



 thus (sat2 . [(n + j), p]) = ((sat . p) . (n + j)) by A44

 .= 1 by A47, A56, A58;

 end;

 (sat2 . [(n + i), q]) = 1 by A44, A48, A55;

 hence ex i st 0 < i & (sat2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (sat2 . [(n + j), p]) = 1 by A54, A57;

 end;

 assume ex i st 0 < i & (sat2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (sat2 . [(n + j), p]) = 1;

 then

 consider i such that

 A59: 0 < i and

 A60: (sat2 . [(n + i), q]) = 1 and

 A61: for j st 1 <= j & j < i holds (sat2 . [(n + j), p]) = 1;



 A62: (s41 . (n + i)) = 1 by A44, A48, A60;



 A63: for j st 1 <= j & j < i holds (s31 . (n + j)) = 1

 proof

 let j;

 assume

 A64: 1 <= j & j < i;



 thus (s31 . (n + j)) = (sat2 . [(n + j), p]) by A44, A47

 .= 1 by A61, A64;

 end;



 thus (sat2 . [n, (p 'U' q)]) = (s51 . n) by A44, A49

 .= 1 by A50, A59, A62, A63;

 end;

 end;

 take sat2;

 now

 let n;



 thus (sat2 . [n, TFALSUM ]) = ((sat . TFALSUM ) . n) by A44

 .= 0 by A34, FUNCOP_1: 7;

 end;

 hence thesis by A45, A46;

 end;

 uniqueness

 proof

 let v1,v2 be Function of [: NAT , LTLB_WFF :], BOOLEAN ;

 assume

 A65: for n be Element of NAT holds (v1 . [n, TFALSUM ]) = 0 & (for k holds (v1 . [n, ( prop k)]) = 1 iff ( prop k) in (M . n)) & for p, q holds (v1 . [n, (p => q)]) = ((v1 . [n, p]) => (v1 . [n, q])) & ((v1 . [n, (p 'U' q)]) = 1 iff ex i st 0 < i & (v1 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v1 . [(n + j), p]) = 1);

 assume

 A66: for n be Element of NAT holds (v2 . [n, TFALSUM ]) = 0 & (for k holds (v2 . [n, ( prop k)]) = 1 iff ( prop k) in (M . n)) & for p, q holds (v2 . [n, (p => q)]) = ((v2 . [n, p]) => (v2 . [n, q])) & ((v2 . [n, (p 'U' q)]) = 1 iff ex i st 0 < i & (v2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v2 . [(n + j), p]) = 1);

 thus v1 = v2

 proof

 defpred P1[ Element of LTLB_WFF ] means for n be Element of NAT holds (v1 . [n, $1]) = (v2 . [n, $1]);



 A67: for n be Element of NAT holds P1[( prop n)]

 proof

 let k be Element of NAT ;

 now

 let n be Element of NAT ;

 per cases ;

 suppose

 A68: ( prop k) in (M . n);



 hence (v1 . [n, ( prop k)]) = 1 by A65

 .= (v2 . [n, ( prop k)]) by A66, A68;

 end;

 suppose

 A69: not ( prop k) in (M . n);

 then (v1 . [n, ( prop k)]) = 0 by XBOOLEAN:def 3, A65;

 hence (v1 . [n, ( prop k)]) = (v2 . [n, ( prop k)]) by XBOOLEAN:def 3, A66, A69;

 end;

 end;

 hence P1[( prop k)];

 end;



 A70: for p, q st P1[p] & P1[q] holds P1[(p 'U' q)] & P1[(p => q)]

 proof

 let p, q;

 assume that

 A71: P1[p] and

 A72: P1[q];

 thus P1[(p 'U' q)]

 proof

 let n;

 per cases ;

 suppose

 A73: ex i st 0 < i & (v1 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v1 . [(n + j), p]) = 1;

 then

 consider i such that

 A74: 0 < i and

 A75: (v1 . [(n + i), q]) = 1 and

 A76: for j st 1 <= j & j < i holds (v1 . [(n + j), p]) = 1;



 A77: (v2 . [(n + i), q]) = 1 by A72, A75;

 A78:

 now

 let j;

 assume 1 <= j & j < i;

 then (v1 . [(n + j), p]) = 1 by A76;

 hence (v2 . [(n + j), p]) = 1 by A71;

 end;



 thus (v1 . [n, (p 'U' q)]) = 1 by A65, A73

 .= (v2 . [n, (p 'U' q)]) by A66, A74, A77, A78;

 end;

 suppose

 A79: not ex i st 0 < i & (v1 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v1 . [(n + j), p]) = 1;

 A80:

 now

 let i;

 per cases by A79;

 suppose not 0 < i;

 hence not ( 0 < i & (v2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v2 . [(n + j), p]) = 1);

 end;

 suppose not (v1 . [(n + i), q]) = 1;

 hence not ( 0 < i & (v2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v2 . [(n + j), p]) = 1) by A72;

 end;

 suppose not for j st 1 <= j & j < i holds (v1 . [(n + j), p]) = 1;

 then

 consider j such that

 A81: 1 <= j & j < i and

 A82: not (v1 . [(n + j), p]) = 1;

 not (v2 . [(n + j), p]) = 1 by A71, A82;

 hence not ( 0 < i & (v2 . [(n + i), q]) = 1 & for j st 1 <= j & j < i holds (v2 . [(n + j), p]) = 1) by A81;

 end;

 end;

 (v1 . [n, (p 'U' q)]) = 0 by XBOOLEAN:def 3, A65, A79;

 hence (v1 . [n, (p 'U' q)]) = (v2 . [n, (p 'U' q)]) by A66, XBOOLEAN:def 3, A80;

 end;

 end;

 thus P1[(p => q)]

 proof

 let n be Element of NAT ;



 thus (v1 . [n, (p => q)]) = ((v1 . [n, p]) => (v1 . [n, q])) by A65

 .= ((v2 . [n, p]) => (v1 . [n, q])) by A71

 .= ((v2 . [n, p]) => (v2 . [n, q])) by A72

 .= (v2 . [n, (p => q)]) by A66;

 end;

 end;

 now

 let n be Element of NAT ;



 thus (v1 . [n, TFALSUM ]) = 0 by A65

 .= (v2 . [n, TFALSUM ]) by A66;

 end;

 then

 A83: P1[ TFALSUM ];



 A84: for A holds P1[A] from HILBERT2:sch 2( A83, A67, A70);



 A85: for x be Element of [: NAT , LTLB_WFF :] st x in ( dom v1) holds (v1 . x) = (v2 . x)

 proof

 let x be Element of [: NAT , LTLB_WFF :];

 consider y,z be object such that

 A86: y in NAT and

 A87: z in LTLB_WFF and

 A88: x = [y, z] by ZFMISC_1:def 2;

 reconsider y1 = y as Element of NAT by A86;

 assume x in ( dom v1);

 thus (v1 . x) = (v2 . x) by A84, A86, A87, A88;

 reconsider z1 = z as Element of LTLB_WFF by A87;

 end;

 ( dom v1) = [: NAT , LTLB_WFF :] by FUNCT_2:def 1

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

 hence thesis by A85, PARTFUN1: 5;

 end;

 end;

 end

 theorem :: LTLAXIO1:5



 Th5: (( SAT M) . [n, ( 'not' A)]) = 1 iff (( SAT M) . [n, A]) = 0

 proof

 hereby

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

 then

 A1: ((( SAT M) . [n, A]) => (( SAT M) . [n, TFALSUM ])) = 1 by Def11;

 (( SAT M) . [n, A]) = 1 or (( SAT M) . [n, A]) = 0 by XBOOLEAN:def 3;

 hence (( SAT M) . [n, A]) = 0 by A1, Def11;

 end;

 assume

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



 thus (( SAT M) . [n, ( 'not' A)]) = ((( SAT M) . [n, A]) => (( SAT M) . [n, TFALSUM ])) by Def11

 .= 1 by A2;

 end;

 theorem :: LTLAXIO1:6



 Th6: (( SAT M) . [n, TVERUM ]) = 1

 proof

 assume not (( SAT M) . [n, TVERUM ]) = 1;

 then not (( SAT M) . [n, TFALSUM ]) = 0 by Th5;

 hence contradiction by Def11;

 end;

 theorem :: LTLAXIO1:7



 Th7: (( SAT M) . [n, (A '&&' B)]) = 1 iff (( SAT M) . [n, A]) = 1 & (( SAT M) . [n, B]) = 1

 proof

 hereby

 assume (( SAT M) . [n, (A '&&' B)]) = 1;

 then ((( SAT M) . [n, (A => (B => TFALSUM ))]) => (( SAT M) . [n, TFALSUM ])) = 1 by Def11;

 then ((( SAT M) . [n, (A => (B => TFALSUM ))]) => FALSE ) = 1 by Def11;

 then ((( SAT M) . [n, A]) => (( SAT M) . [n, (B => TFALSUM )])) = 0 by Def11;

 then ((( SAT M) . [n, A]) => ((( SAT M) . [n, B]) => (( SAT M) . [n, TFALSUM ]))) = 0 by Def11;

 then

 A1: ((( SAT M) . [n, A]) => ((( SAT M) . [n, B]) => FALSE )) = 0 by Def11;

 (( SAT M) . [n, A]) = 0 or (( SAT M) . [n, A]) = 1 by XBOOLEAN:def 3;

 hence (( SAT M) . [n, A]) = 1 & (( SAT M) . [n, B]) = 1 by A1;

 end;

 assume that

 A2: (( SAT M) . [n, A]) = 1 and

 A3: (( SAT M) . [n, B]) = 1;

 ((( SAT M) . [n, B]) => (( SAT M) . [n, TFALSUM ])) = 0 by A3, Def11;

 then ((( SAT M) . [n, A]) => (( SAT M) . [n, (B => TFALSUM )])) = 0 by A2, Def11;

 then (( SAT M) . [n, (A => (B => TFALSUM ))]) = 0 by Def11;

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

 hence (( SAT M) . [n, (A '&&' B)]) = 1 by Def11;

 end;

 theorem :: LTLAXIO1:8



 Th8: (( SAT M) . [n, (A 'or' B)]) = 1 iff ((( SAT M) . [n, A]) = 1 or (( SAT M) . [n, B]) = 1)

 proof

 hereby

 assume (( SAT M) . [n, (A 'or' B)]) = 1;

 then

 A1: (( SAT M) . [n, (( 'not' A) '&&' ( 'not' B))]) = 0 by Th5;

 per cases by A1, Th7;

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

 hence (( SAT M) . [n, A]) = 1 or (( SAT M) . [n, B]) = 1 by XBOOLEAN:def 3, Th5;

 end;

 suppose not (( SAT M) . [n, ( 'not' B)]) = 1;

 hence (( SAT M) . [n, A]) = 1 or (( SAT M) . [n, B]) = 1 by XBOOLEAN:def 3, Th5;

 end;

 end;

 assume

 A2: (( SAT M) . [n, A]) = 1 or (( SAT M) . [n, B]) = 1;

 per cases by A2;

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

 then not (( SAT M) . [n, ( 'not' A)]) = 1 by Th5;

 then not (( SAT M) . [n, (( 'not' A) '&&' ( 'not' B))]) = 1 by Th7;

 hence thesis by Th5, XBOOLEAN:def 3;

 end;

 suppose (( SAT M) . [n, B]) = 1;

 then not (( SAT M) . [n, ( 'not' B)]) = 1 by Th5;

 then not (( SAT M) . [n, (( 'not' A) '&&' ( 'not' B))]) = 1 by Th7;

 hence thesis by Th5, XBOOLEAN:def 3;

 end;

 end;

 theorem :: LTLAXIO1:9



 Th9: (( SAT M) . [n, ( 'X' A)]) = (( SAT M) . [(n + 1), A])

 proof

 set f = TFALSUM , sm = ( SAT M);

 per cases by XBOOLEAN:def 3;

 suppose

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

 then

 consider i such that

 A2: 0 < i & (sm . [(n + i), A]) = 1 and

 A3: for j st 1 <= j & j < i holds (sm . [(n + j), f]) = 1 by Def11;

 now

 assume

 A4: 1 < i;

 not (sm . [(n + 1), f]) = 1 by Def11;

 hence contradiction by A3, A4;

 end;

 hence thesis by A1, A2, NAT_1: 25;

 end;

 suppose

 A5: (( SAT M) . [n, (f 'U' A)]) = 0 ;

 now

 assume

 A6: (sm . [(n + 1), A]) = 1;

 not 0 < 1 or not (sm . [(n + 1), A]) = 1 or not for j st 1 <= j & j < 1 holds (sm . [(n + j), f]) = 1 by A5, Def11;

 hence contradiction by A6;

 end;

 hence thesis by A5, XBOOLEAN:def 3;

 end;

 end;

 theorem :: LTLAXIO1:10



 Th10: (( SAT M) . [n, ( 'G' A)]) = 1 iff for i holds (( SAT M) . [(n + i), A]) = 1

 proof

 set f = TFALSUM , t = TVERUM , sm = ( SAT M);

 hereby

 assume (sm . [n, ( 'G' A)]) = 1;

 then

 A1: (sm . [n, (( 'not' A) 'or' (t 'U' ( 'not' A)))]) = 0 by Th5;

 then

 A2: not (sm . [n, ( 'not' A)]) = 1 by Th8;

 let i;



 A3: not (sm . [n, t]) = 1 or not (sm . [n, (t 'U' ( 'not' A))]) = 1 by A1, Th8;

 per cases ;

 suppose i = 0 ;

 hence (sm . [(n + i), A]) = 1 by Th5, XBOOLEAN:def 3, A2;

 end;

 suppose 0 < i;

 then not (sm . [(n + i), ( 'not' A)]) = 1 or ex j st 1 <= j & j < i & not (sm . [(n + j), t]) = 1 by A3, Def11, Th6;

 hence (sm . [(n + i), A]) = 1 by XBOOLEAN:def 3, Th5, Th6;

 end;

 end;

 assume

 A4: for i holds (sm . [(n + i), A]) = 1;

 now

 assume (sm . [n, ( 'G' A)]) = 0 ;

 then not (sm . [n, (( 'not' A) 'or' (t 'U' ( 'not' A)))]) = 0 by Th5;

 per cases by Th8, XBOOLEAN:def 3;

 suppose (sm . [n, ( 'not' A)]) = 1;

 then (sm . [(n + 0 ), A]) = 0 by Th5;

 hence contradiction by A4;

 end;

 suppose (sm . [n, (t 'U' ( 'not' A))]) = 1;

 then

 consider i such that 0 < i and

 A5: (sm . [(n + i), ( 'not' A)]) = 1 and for j st 1 <= j & j < i holds (sm . [(n + j), t]) = 1 by Def11;

 (sm . [(n + i), A]) = 0 by A5, Th5;

 hence contradiction by A4;

 end;

 end;

 hence (sm . [n, ( 'G' A)]) = 1 by XBOOLEAN:def 3;

 end;

 theorem :: LTLAXIO1:11



 Th11: (( SAT M) . [n, ( 'F' A)]) = 1 iff ex i st (( SAT M) . [(n + i), A]) = 1

 proof

 hereby

 assume (( SAT M) . [n, ( 'F' A)]) = 1;

 then (( SAT M) . [n, ( 'G' ( 'not' A))]) = 0 by Th5;

 then

 consider i such that

 A1: not (( SAT M) . [(n + i), ( 'not' A)]) = 1 by Th10;

 not (( SAT M) . [(n + i), A]) = 0 by A1, Th5;

 hence ex i st (( SAT M) . [(n + i), A]) = 1 by XBOOLEAN:def 3;

 end;

 assume ex i st (( SAT M) . [(n + i), A]) = 1;

 then

 consider i such that

 A2: (( SAT M) . [(n + i), A]) = 1;

 not (( SAT M) . [(n + i), ( 'not' A)]) = 1 by A2, Th5;

 then not (( SAT M) . [n, ( 'G' ( 'not' A))]) = 1 by Th10;

 hence (( SAT M) . [n, ( 'F' A)]) = 1 by Th5, XBOOLEAN:def 3;

 end;

 theorem :: LTLAXIO1:12



 Th12: (( SAT M) . [n, (p 'Uw' q)]) = 1 iff ex i st (( SAT M) . [(n + i), q]) = 1 & for j st j < i holds (( SAT M) . [(n + j), p]) = 1

 proof

 set sm = ( SAT M);

 hereby

 assume

 A1: (sm . [n, (p 'Uw' q)]) = 1;

 per cases by A1, Th8;

 suppose

 A2: (sm . [n, q]) = 1;



 A3: for j st j < 0 holds (sm . [(n + j), p]) = 1;

 (sm . [(n + 0 ), q]) = 1 by A2;

 hence ex i st (sm . [(n + i), q]) = 1 & for j st j < i holds (sm . [(n + j), p]) = 1 by A3;

 end;

 suppose

 A4: (sm . [n, (p '&&' (p 'U' q))]) = 1;

 then (sm . [n, (p 'U' q)]) = 1 by Th7;

 then

 consider i such that 0 < i and

 A5: (sm . [(n + i), q]) = 1 and

 A6: for j st 1 <= j & j < i holds (sm . [(n + j), p]) = 1 by Def11;

 now

 let j;

 assume

 A7: j < i;

 per cases ;

 suppose j = 0 ;

 hence (sm . [(n + j), p]) = 1 by A4, Th7;

 end;

 suppose not j = 0 ;

 then 1 <= j by NAT_1: 25;

 hence (sm . [(n + j), p]) = 1 by A6, A7;

 end;

 end;

 hence ex i st (sm . [(n + i), q]) = 1 & for j st j < i holds (sm . [(n + j), p]) = 1 by A5;

 end;

 end;

 assume ex i st (sm . [(n + i), q]) = 1 & for j st j < i holds (sm . [(n + j), p]) = 1;

 then

 consider i such that

 A8: (sm . [(n + i), q]) = 1 and

 A9: for j st j < i holds (sm . [(n + j), p]) = 1;

 per cases ;

 suppose i = 0 ;

 hence (sm . [n, (p 'Uw' q)]) = 1 by A8, Th8;

 end;

 suppose

 A10: not i = 0 ;

 for j st 1 <= j & j < i holds (sm . [(n + j), p]) = 1 by A9;

 then

 A11: (sm . [n, (p 'U' q)]) = 1 by A8, A10, Def11;

 (sm . [(n + 0 ), p]) = 1 by A9, A10;

 then (sm . [n, (p '&&' (p 'U' q))]) = 1 by A11, Th7;

 hence (sm . [n, (p 'Uw' q)]) = 1 by Th8;

 end;

 end;

 theorem :: LTLAXIO1:13

 (( SAT M) . [n, (p 'R' q)]) = 1 iff ((ex i st (( SAT M) . [(n + i), p]) = 1 & for j st j <= i holds (( SAT M) . [(n + j), q]) = 1) or for i holds (( SAT M) . [(n + i), q]) = 1)

 proof

 set sm = ( SAT M), notp = ( 'not' p), notq = ( 'not' q);

 thus (sm . [n, (p 'R' q)]) = 1 implies ((ex i st (sm . [(n + i), p]) = 1 & for j st j <= i holds (sm . [(n + j), q]) = 1) or for i holds (sm . [(n + i), q]) = 1)

 proof

 defpred P[ Nat] means ((sm . [(n + $1), q]) = 1 & (sm . [(n + $1), p]) = 0 );

 assume (sm . [n, (p 'R' q)]) = 1;

 then

 A1: (sm . [n, (( 'not' p) 'Uw' ( 'not' q))]) = 0 by Th5;

 A2:

 now

 let i be Nat;

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

 per cases by A1, Th12;

 suppose not (sm . [(n + ii), ( 'not' q)]) = 1;

 hence not (sm . [(n + i), ( 'not' q)]) = 1 or ex j be Nat st j < i & not (sm . [(n + j), ( 'not' p)]) = 1;

 end;

 suppose ex j st j < i & not (sm . [(n + j), ( 'not' p)]) = 1;

 hence not (sm . [(n + i), ( 'not' q)]) = 1 or ex j be Nat st j < i & not (sm . [(n + j), ( 'not' p)]) = 1;

 end;

 end;

 assume that

 A3: not (ex i st (sm . [(n + i), p]) = 1 & for j st j <= i holds (sm . [(n + j), q]) = 1) and

 A4: not (for i holds (sm . [(n + i), q]) = 1);

 A5:

 now

 let i be Nat;

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

 not (sm . [(n + ii), p]) = 1 or ex j st j <= ii & not (sm . [(n + j), q]) = 1 by A3;

 hence not (sm . [(n + i), p]) = 1 or ex j be Nat st j <= i & not (sm . [(n + j), q]) = 1;

 end;



 A6: for k be Nat st (for m be Nat st m < k holds P[m]) holds P[k]

 proof

 let k be Nat;

 assume

 A7: for m be Nat st m < k holds P[m];

 reconsider nk = (n + k) as Element of NAT by ORDINAL1:def 12;

 now

 assume ex j be Nat st j < k & not (sm . [(n + j), ( 'not' p)]) = 1;

 then

 consider j be Nat such that

 A8: j < k and

 A9: not (sm . [(n + j), ( 'not' p)]) = 1;

 reconsider nj = (n + j) as Element of NAT by ORDINAL1:def 12;

 not (sm . [nj, p]) = 0 by A9, Th5;

 hence contradiction by A7, A8;

 end;

 then not (sm . [(n + k), ( 'not' q)]) = 1 by A2;

 then not (sm . [nk, q]) = 0 by Th5;

 then

 A10: (sm . [(n + k), q]) = 1 by XBOOLEAN:def 3;

 now

 assume ex j be Nat st j <= k & not (sm . [(n + j), q]) = 1;

 then

 consider j be Nat such that

 A11: j <= k and

 A12: not (sm . [(n + j), q]) = 1;

 per cases ;

 suppose j < k;

 hence contradiction by A7, A12;

 end;

 suppose not j < k;

 hence contradiction by A10, A11, A12, XXREAL_0: 1;

 end;

 end;

 hence P[k] by XBOOLEAN:def 3, A5;

 end;

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

 hence contradiction by A4;

 end;

 thus ((ex i st (sm . [(n + i), p]) = 1 & for j st j <= i holds (sm . [(n + j), q]) = 1) or for i holds (sm . [(n + i), q]) = 1) implies (sm . [n, (p 'R' q)]) = 1

 proof

 assume

 A13: (ex i st (sm . [(n + i), p]) = 1 & for j st j <= i holds (sm . [(n + j), q]) = 1) or for i holds (sm . [(n + i), q]) = 1;

 assume not (sm . [n, (p 'R' q)]) = 1;

 then

 A14: (sm . [n, (notp 'Uw' notq)]) = 1 by XBOOLEAN:def 3, Th5;

 per cases by A13;

 suppose ex i st (sm . [(n + i), p]) = 1 & for j st j <= i holds (sm . [(n + j), q]) = 1;

 then

 consider i such that

 A15: (sm . [(n + i), p]) = 1 and

 A16: for j st j <= i holds (sm . [(n + j), q]) = 1;

 consider k such that

 A17: (sm . [(n + k), notq]) = 1 and

 A18: for j st j < k holds (sm . [(n + j), notp]) = 1 by A14, Th12;

 per cases ;

 suppose k <= i;

 then (sm . [(n + k), q]) = 1 by A16;

 hence contradiction by A17, Th5;

 end;

 suppose not k <= i;

 then (sm . [(n + i), notp]) = 1 by A18;

 hence contradiction by A15, Th5;

 end;

 end;

 suppose

 A19: for i holds (sm . [(n + i), q]) = 1;

 consider i such that

 A20: (sm . [(n + i), notq]) = 1 and for j st j < i holds (sm . [(n + j), notp]) = 1 by A14, Th12;

 (sm . [(n + i), q]) = 0 by A20, Th5;

 hence contradiction by A19;

 end;

 end;

 end;

 theorem :: LTLAXIO1:14



 Th14: (( SAT M) . [n, ( 'not' ( 'X' B))]) = (( SAT M) . [n, ( 'X' ( 'not' B))])

 proof



 thus (( SAT M) . [n, ( 'not' ( 'X' B))]) = ((( SAT M) . [n, ( 'X' B)]) => (( SAT M) . [n, TFALSUM ])) by Def11

 .= ((( SAT M) . [(n + 1), B]) => (( SAT M) . [n, TFALSUM ])) by Th9

 .= ((( SAT M) . [(n + 1), B]) => FALSE ) by Def11

 .= ((( SAT M) . [(n + 1), B]) => (( SAT M) . [(n + 1), TFALSUM ])) by Def11

 .= (( SAT M) . [(n + 1), (B => TFALSUM )]) by Def11

 .= (( SAT M) . [n, ( 'X' ( 'not' B))]) by Th9;

 end;

 theorem :: LTLAXIO1:15



 Th15: (( SAT M) . [n, (( 'not' ( 'X' B)) => ( 'X' ( 'not' B)))]) = 1

 proof



 A1: (( SAT M) . [n, ( 'not' ( 'X' B))]) = 0 or (( SAT M) . [n, ( 'not' ( 'X' B))]) = 1 by XBOOLEAN:def 3;



 thus (( SAT M) . [n, (( 'not' ( 'X' B)) => ( 'X' ( 'not' B)))]) = ((( SAT M) . [n, ( 'not' ( 'X' B))]) => (( SAT M) . [n, ( 'X' ( 'not' B))])) by Def11

 .= 1 by A1, Th14;

 end;

 theorem :: LTLAXIO1:16



 Th16: (( SAT M) . [n, (( 'X' ( 'not' B)) => ( 'not' ( 'X' B)))]) = 1

 proof



 A1: (( SAT M) . [n, ( 'not' ( 'X' B))]) = 0 or (( SAT M) . [n, ( 'not' ( 'X' B))]) = 1 by XBOOLEAN:def 3;



 thus (( SAT M) . [n, (( 'X' ( 'not' B)) => ( 'not' ( 'X' B)))]) = ((( SAT M) . [n, ( 'X' ( 'not' B))]) => (( SAT M) . [n, ( 'not' ( 'X' B))])) by Def11

 .= 1 by A1, Th14;

 end;

 theorem :: LTLAXIO1:17



 Th17: (( SAT M) . [n, (( 'X' (B => C)) => (( 'X' B) => ( 'X' C)))]) = 1

 proof



 A1: (( SAT M) . [(n + 1), B]) = 0 or (( SAT M) . [(n + 1), B]) = 1 by XBOOLEAN:def 3;



 A2: (( SAT M) . [(n + 1), C]) = 0 or (( SAT M) . [(n + 1), C]) = 1 by XBOOLEAN:def 3;



 thus (( SAT M) . [n, (( 'X' (B => C)) => (( 'X' B) => ( 'X' C)))]) = ((( SAT M) . [n, ( 'X' (B => C))]) => (( SAT M) . [n, (( 'X' B) => ( 'X' C))])) by Def11

 .= ((( SAT M) . [(n + 1), (B => C)]) => (( SAT M) . [n, (( 'X' B) => ( 'X' C))])) by Th9

 .= ((( SAT M) . [(n + 1), (B => C)]) => ((( SAT M) . [n, ( 'X' B)]) => (( SAT M) . [n, ( 'X' C)]))) by Def11

 .= ((( SAT M) . [(n + 1), (B => C)]) => ((( SAT M) . [(n + 1), B]) => (( SAT M) . [n, ( 'X' C)]))) by Th9

 .= ((( SAT M) . [(n + 1), (B => C)]) => ((( SAT M) . [(n + 1), B]) => (( SAT M) . [(n + 1), C]))) by Th9

 .= 1 by A1, A2, Def11;

 end;

 theorem :: LTLAXIO1:18



 Th18: (( SAT M) . [n, (( 'G' B) => (B '&&' ( 'X' ( 'G' B))))]) = 1

 proof



 A1: (( SAT M) . [n, (( 'G' B) => (B '&&' ( 'X' ( 'G' B))))]) = ((( SAT M) . [n, ( 'G' B)]) => (( SAT M) . [n, (B '&&' ( 'X' ( 'G' B)))])) by Def11;

 per cases by XBOOLEAN:def 3;

 suppose (( SAT M) . [n, ( 'G' B)]) = 0 ;

 hence thesis by A1;

 end;

 suppose

 A2: (( SAT M) . [n, ( 'G' B)]) = 1;

 now

 let i be Element of NAT ;

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

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

 end;

 then (( SAT M) . [(n + 1), ( 'G' B)]) = 1 by Th10;

 then

 A3: (( SAT M) . [n, ( 'X' ( 'G' B))]) = 1 by Th9;

 (( SAT M) . [(n + 0 ), B]) = 1 by A2, Th10;

 then (( SAT M) . [n, (B '&&' ( 'X' ( 'G' B)))]) = 1 by A3, Th7;

 hence thesis by A1;

 end;

 end;

 theorem :: LTLAXIO1:19



 Th19: (( SAT M) . [n, ((B 'U' C) => (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C)))))]) = 1

 proof

 set sm = ( SAT M);

 A1:

 now

 assume that

 A2: (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) = 0 and

 A3: (sm . [n, (B 'U' C)]) = 1;

 consider i such that

 A4: 0 < i and

 A5: (sm . [(n + i), C]) = 1 and

 A6: for j st 1 <= j & j < i holds (sm . [(n + j), B]) = 1 by A3, Def11;



 A7: not (sm . [n, ( 'X' C)]) = 1 by A2, Th8;

 not (sm . [n, ( 'X' (B '&&' (B 'U' C)))]) = 1 by A2, Th8;

 then (sm . [n, ( 'X' (B '&&' (B 'U' C)))]) = 0 by XBOOLEAN:def 3;

 then

 A8: (sm . [(n + 1), (B '&&' (B 'U' C))]) = 0 by Th9;

 per cases by A4, NAT_1: 25;

 suppose i = 1;

 hence contradiction by A5, A7, Th9;

 end;

 suppose

 A9: i > 1;

 A10:

 now

 let j;

 assume that

 A11: 1 <= j and

 A12: j < (i -' 1);

 (j + 1) < ((i -' 1) + 1) by A12, XREAL_1: 8;

 then

 A13: (j + 1) < ((i - 1) + 1) by A12, XREAL_0:def 2;

 1 <= (j + 1) by A11, NAT_1: 19;

 then (sm . [(n + (j + 1)), B]) = 1 by A6, A13;

 hence (sm . [((n + 1) + j), B]) = 1;

 end;



 A14: not (sm . [(n + 1), B]) = 1 or not (sm . [(n + 1), (B 'U' C)]) = 1 by A8, Th7;



 A15: (i + ( - 1)) > (1 + ( - 1)) by A9, XREAL_1: 8;

 (n + i) = ((n + 1) + (i - 1))

 .= ((n + 1) + (i -' 1)) by A15, XREAL_0:def 2;

 hence contradiction by A5, A6, A9, A15, A10, A14, Def11;

 end;

 end;

 (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) = 0 or (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) = 1 by XBOOLEAN:def 3;

 then ((sm . [n, (B 'U' C)]) => (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))])) = 1 by A1, XBOOLEAN:def 3;

 hence thesis by Def11;

 end;

 theorem :: LTLAXIO1:20



 Th20: (( SAT M) . [n, ((( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C)))) => (B 'U' C))]) = 1

 proof

 set sm = ( SAT M);

 A1:

 now

 assume that

 A2: (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) = 1 and

 A3: (sm . [n, (B 'U' C)]) = 0 ;

 per cases by A2, Th8;

 suppose

 A4: (sm . [n, ( 'X' C)]) = 1;



 A5: for j st 1 <= j & j < 1 holds (sm . [(n + j), B]) = 1;

 (sm . [(n + 1), C]) = 1 by A4, Th9;

 hence contradiction by A3, A5, Def11;

 end;

 suppose (sm . [n, ( 'X' (B '&&' (B 'U' C)))]) = 1;

 then

 A6: (sm . [(n + 1), (B '&&' (B 'U' C))]) = 1 by Th9;

 then (sm . [(n + 1), (B 'U' C)]) = 1 by Th7;

 then

 consider i such that i > 0 and

 A7: (sm . [((n + 1) + i), C]) = 1 and

 A8: for j st 1 <= j & j < i holds (sm . [((n + 1) + j), B]) = 1 by Def11;

 A9:

 now

 let j;

 assume

 A10: 1 <= j & j < (1 + i);

 per cases by A10, NAT_1: 25;

 suppose 1 = j;

 hence (sm . [(n + j), B]) = 1 by A6, Th7;

 end;

 suppose

 A11: 1 < j & j < (i + 1);

 then

 A12: (1 + ( - 1)) < (j + ( - 1)) by XREAL_1: 8;

 then (j - 1) > 0 ;

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

 then

 A13: 1 <= (j -' 1) by NAT_1: 25;



 A14: (((n + j) + 1) - 1) = ((n + 1) + (j - 1))

 .= ((n + 1) + (j -' 1)) by A12, XREAL_0:def 2;

 (j + ( - 1)) < ((i + 1) + ( - 1)) by A11, XREAL_1: 8;

 hence (sm . [(n + j), B]) = 1 by A8, A14, A13;

 end;

 end;

 (sm . [(n + (1 + i)), C]) = 1 by A7;

 hence contradiction by A3, A9, Def11;

 end;

 end;

 (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) = 0 or (sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) = 1 by XBOOLEAN:def 3;

 then ((sm . [n, (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C))))]) => (sm . [n, (B 'U' C)])) = 1 by A1, XBOOLEAN:def 3;

 hence thesis by Def11;

 end;

 theorem :: LTLAXIO1:21



 Th21: (( SAT M) . [n, ((B 'U' C) => ( 'X' ( 'F' C)))]) = 1

 proof

 set sm = ( SAT M);

 A1:

 now

 assume that

 A2: (sm . [n, (B 'U' C)]) = 1 and

 A3: (sm . [n, ( 'X' ( 'F' C))]) = 0 ;

 consider i such that

 A4: 0 = (1 + ( - 1)) by A4, NAT_1: 25, XREAL_1: 6;



 then

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

 .= (n + i);

 (sm . [(n + 1), ( 'F' C)]) = 0 by A3, Th9;

 hence contradiction by A5, A6, Th11;

 end;

 (sm . [n, (B 'U' C)]) = 0 or (sm . [n, (B 'U' C)]) = 1 by XBOOLEAN:def 3;

 then ((sm . [n, (B 'U' C)]) => (sm . [n, ( 'X' ( 'F' C))])) = 1 by A1, XBOOLEAN:def 3;

 hence thesis by Def11;

 end;

 begin

 definition

 let M, p;

 :: LTLAXIO1:def12

 pred M |= p means

 : Def12: for n be Element of NAT holds (( SAT M) . [n, p]) = 1;

 end

 definition

 let M, F;

 :: LTLAXIO1:def13

 pred M |= F means for p st p in F holds M |= p;

 end

 definition

 let F, p;

 :: LTLAXIO1:def14

 pred F |= p means for M holds (M |= F implies M |= p);

 end

 theorem :: LTLAXIO1:22



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

 proof

 hereby

 assume

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

 thus M |= (F \/ G)

 proof

 let p;

 assume p in (F \/ G);

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

 hence M |= p by A1;

 end;

 end;

 assume

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

 thus M |= F

 proof

 let p;

 assume p in F;

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

 hence M |= p by A2;

 end;

 thus M |= G

 proof

 let p;

 assume p in G;

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

 hence M |= p by A2;

 end;

 end;

 theorem :: LTLAXIO1:23



 Th23: M |= A iff M |= {A}

 proof

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

 A in {A} by TARSKI:def 1;

 hence thesis;

 end;

 theorem :: LTLAXIO1:24



 Th24: F |= A & F |= (A => B) implies F |= B

 proof

 assume that

 A1: F |= A and

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

 let M;

 assume

 A3: M |= F;

 let n be Element of NAT ;

 (( SAT M) . [n, (A => B)]) = 1 by Def12, A2, A3;

 then

 A4: ((( SAT M) . [n, A]) => (( SAT M) . [n, B])) = 1 by Def11;

 (( SAT M) . [n, A]) = 1 by Def12, A1, A3;

 hence (( SAT M) . [n, B]) = 1 by A4;

 end;

 theorem :: LTLAXIO1:25



 Th25: F |= A implies F |= ( 'X' A)

 proof

 assume

 A1: F |= A;

 let M;

 assume

 A2: M |= F;

 let n be Element of NAT ;



 thus (( SAT M) . [n, ( 'X' A)]) = (( SAT M) . [(n + 1), A]) by Th9

 .= 1 by A2, Def12, A1;

 end;

 theorem :: LTLAXIO1:26

 F |= A implies F |= ( 'G' A)

 proof

 assume

 A1: F |= A;

 let M;

 assume

 A2: M |= F;

 let n be Element of NAT ;

 for i be Element of NAT holds (( SAT M) . [(n + i), A]) = 1 by Def12, A1, A2;

 hence (( SAT M) . [n, ( 'G' A)]) = 1 by Th10;

 end;

 theorem :: LTLAXIO1:27



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

 proof

 assume that

 A1: F |= (A => B) and

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

 let M;

 assume

 A3: M |= F;

 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;

 (( SAT M) . [(n + kk), (A => ( 'X' A))]) = 1 by A2, A3, Def12;

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

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

 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 ;

 (( SAT M) . [(n + i), (A => B)]) = 1 by A3, A1, Def12;

 then

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

 (( 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 Th10;

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

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

 end;

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

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

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

 end;

 end;

 theorem :: LTLAXIO1:28



 Th28: (( SAT (M ^\ i)) . [j, A]) = (( SAT M) . [(i + j), A])

 proof

 defpred P1[ Element of LTLB_WFF ] means for k holds (( SAT (M ^\ i)) . [k, $1]) = (( SAT M) . [(i + k), $1]);



 A1: for n be Element of NAT holds P1[( prop n)]

 proof

 let n, k;

 per cases ;

 suppose

 A2: ( prop n) in ((M ^\ i) . k);

 then

 A3: ( prop n) in (M . (i + k)) by NAT_1:def 3;



 thus (( SAT (M ^\ i)) . [k, ( prop n)]) = 1 by A2, Def11

 .= (( SAT M) . [(i + k), ( prop n)]) by A3, Def11;

 end;

 suppose

 A4: not ( prop n) in ((M ^\ i) . k);

 then not ( prop n) in (M . (i + k)) by NAT_1:def 3;

 then

 A5: not (( SAT M) . [(i + k), ( prop n)]) = 1 by Def11;

 not (( SAT (M ^\ i)) . [k, ( prop n)]) = 1 by A4, Def11;



 hence (( SAT (M ^\ i)) . [k, ( prop n)]) = 0 by XBOOLEAN:def 3

 .= (( SAT M) . [(i + k), ( prop n)]) by A5, XBOOLEAN:def 3;

 end;

 end;



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

 proof

 let r,s be Element of LTLB_WFF ;

 assume that

 A7: P1[r] and

 A8: P1[s];

 thus P1[(r 'U' s)]

 proof

 let k;



 A9: (( SAT (M ^\ i)) . [k, (r 'U' s)]) = 1 iff (( SAT M) . [(i + k), (r 'U' s)]) = 1

 proof

 hereby

 assume (( SAT (M ^\ i)) . [k, (r 'U' s)]) = 1;

 then

 consider m be Element of NAT such that

 A10: 0 < m and

 A11: (( SAT (M ^\ i)) . [(k + m), s]) = 1 and

 A12: for j st 1 <= j & j < m holds (( SAT (M ^\ i)) . [(k + j), r]) = 1 by Def11;

 A13:

 now

 let j;

 assume 1 <= j & j < m;

 then (( SAT (M ^\ i)) . [(k + j), r]) = 1 by A12;

 then (( SAT M) . [(i + (k + j)), r]) = 1 by A7;

 hence (( SAT M) . [((i + k) + j), r]) = 1;

 end;

 (( SAT M) . [(i + (k + m)), s]) = 1 by A8, A11;

 then (( SAT M) . [((i + k) + m), s]) = 1;

 hence (( SAT M) . [(i + k), (r 'U' s)]) = 1 by A10, A13, Def11;

 end;

 assume (( SAT M) . [(i + k), (r 'U' s)]) = 1;

 then

 consider m be Element of NAT such that

 A14: 0 < m and

 A15: (( SAT M) . [((i + k) + m), s]) = 1 and

 A16: for j st 1 <= j & j < m holds (( SAT M) . [((i + k) + j), r]) = 1 by Def11;

 A17:

 now

 let j;

 assume 1 <= j & j < m;

 then (( SAT M) . [((i + k) + j), r]) = 1 by A16;

 then (( SAT M) . [(i + (k + j)), r]) = 1;

 hence (( SAT (M ^\ i)) . [(k + j), r]) = 1 by A7;

 end;

 (( SAT M) . [(i + (k + m)), s]) = 1 by A15;

 then (( SAT (M ^\ i)) . [(k + m), s]) = 1 by A8;

 hence (( SAT (M ^\ i)) . [k, (r 'U' s)]) = 1 by A14, A17, Def11;

 end;

 per cases ;

 suppose (( SAT (M ^\ i)) . [k, (r 'U' s)]) = 1;

 hence thesis by A9;

 end;

 suppose not (( SAT (M ^\ i)) . [k, (r 'U' s)]) = 1;

 then (( SAT (M ^\ i)) . [k, (r 'U' s)]) = 0 by XBOOLEAN:def 3;

 hence thesis by A9, XBOOLEAN:def 3;

 end;

 end;

 thus P1[(r => s)]

 proof

 let k be Element of NAT ;



 thus (( SAT (M ^\ i)) . [k, (r => s)]) = ((( SAT (M ^\ i)) . [k, r]) => (( SAT (M ^\ i)) . [k, s])) by Def11

 .= ((( SAT M) . [(i + k), r]) => (( SAT (M ^\ i)) . [k, s])) by A7

 .= ((( SAT M) . [(i + k), r]) => (( SAT M) . [(i + k), s])) by A8

 .= (( SAT M) . [(i + k), (r => s)]) by Def11;

 end;

 end;

 now

 let k;



 thus (( SAT (M ^\ i)) . [k, TFALSUM ]) = 0 by Def11

 .= (( SAT M) . [(i + k), TFALSUM ]) by Def11;

 end;

 then

 A18: P1[ TFALSUM ];

 for r be Element of LTLB_WFF holds P1[r] from HILBERT2:sch 2( A18, A1, A6);

 hence (( SAT (M ^\ i)) . [j, A]) = (( SAT M) . [(i + j), A]);

 end;

 theorem :: LTLAXIO1:29



 Th29: M |= F implies (M ^\ i) |= F

 proof

 assume

 A1: M |= F;

 thus (M ^\ i) |= F

 proof

 let p;

 assume

 A2: p in F;

 thus (M ^\ i) |= p

 proof

 let n;

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

 hence (( SAT (M ^\ i)) . [n, p]) = 1 by Th28;

 end;

 end;

 end;

 theorem :: LTLAXIO1:30

 (F \/ {A}) |= B iff F |= (( 'G' A) => B)

 proof

 hereby

 assume

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

 thus F |= (( 'G' A) => B)

 proof

 let M;

 assume

 A2: M |= F;

 thus M |= (( 'G' A) => B)

 proof

 let n;

 per cases by XBOOLEAN:def 3;

 suppose

 A3: (( SAT M) . [n, ( 'G' A)]) = 0 ;



 thus (( SAT M) . [n, (( 'G' A) => B)]) = ((( SAT M) . [n, ( 'G' A)]) => (( SAT M) . [n, B])) by Def11

 .= 1 by A3;

 end;

 suppose

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

 now

 let j;

 (( SAT M) . [(n + j), A]) = 1 by A4, Th10;

 hence (( SAT (M ^\ n)) . [j, A]) = 1 by Th28;

 end;

 then

 A5: (M ^\ n) |= {A} by Th23, Def12;

 (M ^\ n) |= F by A2, Th29;

 then (M ^\ n) |= (F \/ {A}) by A5, Th22;

 then (( SAT (M ^\ n)) . [ 0 , B]) = 1 by Def12, A1;

 then

 A6: (( SAT M) . [(n + 0 ), B]) = 1 by Th28;



 thus (( SAT M) . [n, (( 'G' A) => B)]) = ((( SAT M) . [n, ( 'G' A)]) => (( SAT M) . [n, B])) by Def11

 .= 1 by A6;

 end;

 end;

 end;

 end;

 assume

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

 let M;

 assume

 A8: M |= (F \/ {A});

 let i;

 M |= {A} by A8, Th22;

 then for j holds (( SAT M) . [(i + j), A]) = 1 by Def12, Th23;

 then

 A9: (( SAT M) . [i, ( 'G' A)]) = 1 by Th10;

 M |= F by A8, Th22;

 then (( SAT M) . [i, (( 'G' A) => B)]) = 1 by Def12, A7;

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

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

 end;

 definition

 let f be Function of LTLB_WFF , BOOLEAN ;

 :: LTLAXIO1:def15

 func VAL f -> Function of LTLB_WFF , BOOLEAN means

 : Def15: (it . TFALSUM ) = 0 & (it . ( prop n)) = (f . ( prop n)) & (it . (A => B)) = ((it . A) => (it . B)) & (it . (A 'U' B)) = (f . (A 'U' B));

 existence

 proof

 defpred P3[ Element of LTLB_WFF , Element of LTLB_WFF , set, set, set] means ($3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex a,b,c be Element of BOOLEAN st a = $3 & b = $4 & c = $5 & c = (a => b)) & ( not $3 is Element of BOOLEAN or not $4 is Element of BOOLEAN implies $5 = {} );

 defpred P1[ Element of LTLB_WFF , Element of LTLB_WFF , set, set, set] means $5 = (f . ($1 'U' $2));

 deffunc F2( Element of NAT ) = (f . ( prop $1));



 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;

 let x,y be set;

 per cases ;

 suppose that

 A2: x is Element of BOOLEAN and

 A3: y is Element of BOOLEAN ;

 reconsider b = y as Element of BOOLEAN by A3;

 reconsider a = x as Element of BOOLEAN by A2;

 per cases by XBOOLEAN:def 3;

 suppose

 A4: a = 0 ;

 set c = TRUE ;

 c = (a => b) by A4;

 hence thesis;

 end;

 suppose

 A5: a = 1;

 per cases by XBOOLEAN:def 3;

 suppose

 A6: b = 0 ;

 set c = FALSE ;

 c = (a => b) by A5, A6;

 hence thesis;

 end;

 suppose

 A7: b = 1;

 set c = TRUE ;

 c = (a => b) by A7;

 hence thesis;

 end;

 end;

 end;

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

 hence thesis;

 end;

 end;



 A8: 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;



 A9: 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;



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

 consider val be ManySortedSet of LTLB_WFF such that

 A11: (val . TFALSUM ) = 0 & (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( A10, A1, A8, A9);

 A12:

 now

 A13:

 now

 let A, B;

 per cases ;

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

 then

 consider a,b,c be Element of BOOLEAN such that a = (val . A) and b = (val . B) and

 A14: c = (val . (A => B)) and c = (a => b) by A11;

 thus (val . (A => B)) in BOOLEAN by A14;

 end;

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

 then (val . (A => B)) = FALSE by A11;

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

 end;

 end;

 let x be object;

 assume x in LTLB_WFF ;

 then

 reconsider x1 = x as Element of LTLB_WFF ;

 A15:

 now

 let n;

 (val . ( prop n)) = (f . ( prop n)) by A11;

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

 end;

 A16:

 now

 let A, B;

 (val . (A 'U' B)) = (f . (A 'U' B)) by A11;

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

 end;

 per cases by Th4;

 suppose x1 = TFALSUM ;

 hence (val . x) in BOOLEAN by A11, TARSKI:def 2;

 end;

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

 hence (val . x) in BOOLEAN by A15;

 end;

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

 hence (val . x) in BOOLEAN by A16;

 end;

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

 hence (val . x) in BOOLEAN by A13;

 end;

 end;

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

 then

 reconsider val as Function of LTLB_WFF , BOOLEAN by A12, FUNCT_2: 3;

 take val;

 now

 let A, B;

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

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

 end;

 hence thesis by A11;

 end;

 uniqueness

 proof

 let v1,v2 be Function of LTLB_WFF , BOOLEAN ;

 assume

 A17: (v1 . TFALSUM ) = 0 & (v1 . ( prop n)) = (f . ( prop n)) & (v1 . (A => B)) = ((v1 . A) => (v1 . B)) & (v1 . (A 'U' B)) = (f . (A 'U' B));

 assume

 A18: (v2 . TFALSUM ) = 0 & (v2 . ( prop n)) = (f . ( prop n)) & (v2 . (A => B)) = ((v2 . A) => (v2 . B)) & (v2 . (A 'U' B)) = (f . (A 'U' B));

 thus v1 = v2

 proof

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



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

 proof

 let n;

 (v1 . ( prop n)) = (f . ( 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)) = (f . (r 'U' s)) by A17

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

 (v1 . (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 LTLB_WFF holds P1[x] from HILBERT2:sch 2( A23, A19, A20);

 then

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

 ( dom v1) = LTLB_WFF by FUNCT_2:def 1

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

 hence thesis by A24, PARTFUN1: 5;

 end;

 end;

 end

 theorem :: LTLAXIO1:31



 Th31: for f be Function of LTLB_WFF , BOOLEAN , p, q holds (( VAL f) . (p '&&' q)) = ((( VAL f) . p) '&' (( VAL f) . q))

 proof

 let f be Function of LTLB_WFF , BOOLEAN , p, q;



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



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



 thus (( VAL f) . (p '&&' q)) = ((( VAL f) . (p => (q => TFALSUM ))) => (( VAL f) . TFALSUM )) by Def15

 .= (((( VAL f) . p) => (( VAL f) . (q => TFALSUM ))) => (( VAL f) . TFALSUM )) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . TFALSUM ))) => (( VAL f) . TFALSUM )) by Def15

 .= (((( VAL f) /. p) => ((( VAL f) . q) => FALSE )) => (( VAL f) . TFALSUM )) by Def15

 .= ((( VAL f) . p) '&' (( VAL f) . q)) by A1, A2, Def15;

 end;

 theorem :: LTLAXIO1:32



 Th32: for f be Function of LTLB_WFF , BOOLEAN st (for B be object st B in LTLB_WFF holds (f . B) = (( SAT M) . [n, B])) holds (( VAL f) . A) = (( SAT M) . [n, A])

 proof

 let f be Function of LTLB_WFF , BOOLEAN ;

 defpred P1[ Element of LTLB_WFF ] means (( VAL f) . $1) = (( SAT M) . [n, $1]);

 assume

 A1: for B be object st B in LTLB_WFF holds (f . B) = (( SAT M) . [n, B]);



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

 proof

 let k;

 (( SAT M) . [n, ( prop k)]) = (f . ( prop k)) by A1

 .= (( VAL f) . ( prop k)) by Def15;

 hence thesis;

 end;



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

 proof

 let r, s;

 assume

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

 (( VAL f) . (r 'U' s)) = (f . (r 'U' s)) by Def15

 .= (( SAT M) . [n, (r 'U' s)]) by A1;

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

 (( SAT M) . [n, (r => s)]) = ((( SAT M) . [n, r]) => (( SAT M) . [n, s])) by Def11

 .= (( VAL f) . (r => s)) by A4, Def15;

 hence P1[(r => s)];

 end;

 (( SAT M) . [n, TFALSUM ]) = 0 by Def11

 .= (( VAL f) . TFALSUM ) by Def15;

 then

 A5: P1[ TFALSUM ];

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

 hence (( VAL f) . A) = (( SAT M) . [n, A]);

 end;

 definition

 let p;

 :: LTLAXIO1:def16

 attr p is LTL_TAUT_OF_PL means for f be Function of LTLB_WFF , BOOLEAN holds (( VAL f) . p) = 1;

 end

 theorem :: LTLAXIO1:33



 Th33: A is LTL_TAUT_OF_PL implies F |= A

 proof

 assume

 A1: A is LTL_TAUT_OF_PL;

 let M be LTLModel;

 assume M |= F;

 let n;

 defpred P[ object, object] means $2 = (( SAT M) . [n, $1]);



 A2: for x be object st x in LTLB_WFF holds ex y be object st y in BOOLEAN & P[x, y]

 proof

 let x be object;

 set y = (( SAT M) . [n, x]);

 assume x in LTLB_WFF ;

 then

 reconsider x1 = x as Element of LTLB_WFF ;

 take y;

 (( SAT M) . [n, x1]) in BOOLEAN ;

 hence y in BOOLEAN & P[x, y];

 end;

 consider f be Function of LTLB_WFF , BOOLEAN such that

 A3: for B be object st B in LTLB_WFF holds P[B, (f . B)] from FUNCT_2:sch 1( A2);



 thus (( SAT M) . [n, A]) = (( VAL f) . A) by A3, Th32

 .= 1 by A1;

 end;

 begin

 definition

 let D be set;

 :: LTLAXIO1:def17

 attr D is with_LTL_axioms means

 : Def17: for p, q holds (p is LTL_TAUT_OF_PL implies p in D) & (( 'not' ( 'X' p)) => ( 'X' ( 'not' p))) in D & (( 'X' ( 'not' p)) => ( 'not' ( 'X' p))) in D & (( 'X' (p => q)) => (( 'X' p) => ( 'X' q))) in D & (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) in D & ((p 'U' q) => (( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q))))) in D & ((( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q)))) => (p 'U' q)) in D & ((p 'U' q) => ( 'X' ( 'F' q))) in D;

 end

 definition

 :: LTLAXIO1:def18

 func LTL_axioms -> Subset of LTLB_WFF means

 : Def18: it is with_LTL_axioms & for D be Subset of LTLB_WFF st D is with_LTL_axioms holds it c= D;

 existence

 proof

 defpred S1[ object] means for D be set st D is with_LTL_axioms holds $1 in D;

 consider D0 be set such that

 A1: for x be object holds (x in D0 iff x in LTLB_WFF & S1[x]) from XBOOLE_0:sch 1;

 D0 c= LTLB_WFF by A1;

 then

 reconsider D0 as Subset of LTLB_WFF ;

 take D0;

 thus D0 is with_LTL_axioms

 proof

 let p,q be Element of LTLB_WFF ;

 thus p is LTL_TAUT_OF_PL implies p in D0

 proof

 assume p is LTL_TAUT_OF_PL;

 then for D be set st D is with_LTL_axioms holds p in D;

 hence thesis by A1;

 end;

 for D be set st D is with_LTL_axioms holds (( 'not' ( 'X' p)) => ( 'X' ( 'not' p))) in D;

 hence (( 'not' ( 'X' p)) => ( 'X' ( 'not' p))) in D0 by A1;

 for D be set st D is with_LTL_axioms holds (( 'X' ( 'not' p)) => ( 'not' ( 'X' p))) in D;

 hence (( 'X' ( 'not' p)) => ( 'not' ( 'X' p))) in D0 by A1;

 for D be set st D is with_LTL_axioms holds (( 'X' (p => q)) => (( 'X' p) => ( 'X' q))) in D;

 hence (( 'X' (p => q)) => (( 'X' p) => ( 'X' q))) in D0 by A1;

 for D be set st D is with_LTL_axioms holds (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) in D;

 hence (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) in D0 by A1;

 for D be set st D is with_LTL_axioms holds ((p 'U' q) => (( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q))))) in D;

 hence ((p 'U' q) => (( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q))))) in D0 by A1;

 for D be set st D is with_LTL_axioms holds ((( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q)))) => (p 'U' q)) in D;

 hence ((( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q)))) => (p 'U' q)) in D0 by A1;

 for D be set st D is with_LTL_axioms holds ((p 'U' q) => ( 'X' ( 'F' q))) in D;

 hence ((p 'U' q) => ( 'X' ( 'F' q))) in D0 by A1;

 end;

 let D be Subset of LTLB_WFF ;

 assume

 A2: D is with_LTL_axioms;

 let x be object;

 assume x in D0;

 hence x in D by A1, A2;

 end;

 uniqueness

 proof

 let D1,D2 be Subset of LTLB_WFF ;

 assume (D1 is with_LTL_axioms) & (for D be Subset of LTLB_WFF st D is with_LTL_axioms holds D1 c= D) & D2 is with_LTL_axioms & for D be Subset of LTLB_WFF st D is with_LTL_axioms holds D2 c= D;

 then D1 c= D2 & D2 c= D1;

 hence D1 = D2 by XBOOLE_0:def 10;

 end;

 end

 registration

 cluster LTL_axioms -> with_LTL_axioms;

 coherence by Def18;

 end

 theorem :: LTLAXIO1:34



 Th34: (p => (q => p)) in LTL_axioms

 proof

 (p => (q => p)) is LTL_TAUT_OF_PL

 proof

 let f be Function of LTLB_WFF , BOOLEAN ;



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



 thus (( VAL f) . (p => (q => p))) = ((( VAL f) . p) => (( VAL f) . (q => p))) by Def15

 .= ((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . p))) by Def15

 .= 1 by A1;

 end;

 hence (p => (q => p)) in LTL_axioms by Def17;

 end;

 theorem :: LTLAXIO1:35



 Th35: ((p => (q => r)) => ((p => q) => (p => r))) in LTL_axioms

 proof

 ((p => (q => r)) => ((p => q) => (p => r))) is LTL_TAUT_OF_PL

 proof

 let f be Function of LTLB_WFF , BOOLEAN ;



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



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



 A3: (( VAL f) . r) = 0 or (( VAL f) . r) = 1 by XBOOLEAN:def 3;



 thus (( VAL f) . ((p => (q => r)) => ((p => q) => (p => r)))) = ((( VAL f) . (p => (q => r))) => (( VAL f) . ((p => q) => (p => r)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . (q => r))) => (( VAL f) . ((p => q) => (p => r)))) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) => (( VAL f) . ((p => q) => (p => r)))) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) => ((( VAL f) . (p => q)) => (( VAL f) . (p => r)))) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) => (((( VAL f) . p) => (( VAL f) . q)) => (( VAL f) . (p => r)))) by Def15

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

 end;

 hence ((p => (q => r)) => ((p => q) => (p => r))) in LTL_axioms by Def17;

 end;

 definition

 let p, q;

 :: LTLAXIO1:def19

 pred p NEX_rule q means q = ( 'X' p);

 let r;

 :: LTLAXIO1:def20

 pred p,q MP_rule r means q = (p => r);

 :: LTLAXIO1:def21

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

 end

 registration

 cluster LTL_axioms -> non empty;

 coherence by Def17;

 end

 definition

 let A;

 :: LTLAXIO1:def22

 attr A is axltl1 means

 : Def22: ex B st A = (( 'not' ( 'X' B)) => ( 'X' ( 'not' B)));

 :: LTLAXIO1:def23

 attr A is axltl1a means

 : Def23: ex B st A = (( 'X' ( 'not' B)) => ( 'not' ( 'X' B)));

 :: LTLAXIO1:def24

 attr A is axltl2 means

 : Def24: ex B, C st A = (( 'X' (B => C)) => (( 'X' B) => ( 'X' C)));

 :: LTLAXIO1:def25

 attr A is axltl3 means

 : Def25: ex B st A = (( 'G' B) => (B '&&' ( 'X' ( 'G' B))));

 :: LTLAXIO1:def26

 attr A is axltl4 means

 : Def26: ex B, C st A = ((B 'U' C) => (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C)))));

 :: LTLAXIO1:def27

 attr A is axltl5 means

 : Def27: ex B, C st A = ((( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C)))) => (B 'U' C));

 :: LTLAXIO1:def28

 attr A is axltl6 means

 : Def28: ex B, C st A = ((B 'U' C) => ( 'X' ( 'F' C)));

 end

 theorem :: LTLAXIO1:36



 Th36: for A be Element of LTL_axioms holds (A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6)

 proof

 defpred P1[ Element of LTL_axioms ] means $1 is LTL_TAUT_OF_PL or $1 is axltl1 or $1 is axltl1a or $1 is axltl2 or $1 is axltl3 or $1 is axltl4 or $1 is axltl5 or $1 is axltl6;

 set X = { p where p be Element of LTL_axioms : P1[p] };

 X c= LTLB_WFF

 proof

 let x be object;

 assume x in X;

 then ex p be Element of LTL_axioms st x = p & P1[p];

 hence x in LTLB_WFF ;

 end;

 then

 reconsider X as Subset of LTLB_WFF ;

 let A be Element of LTL_axioms ;

 X is with_LTL_axioms

 proof

 let p, q;

 thus p is LTL_TAUT_OF_PL implies p in X

 proof

 assume

 A1: p is LTL_TAUT_OF_PL;

 then

 reconsider p1 = p as Element of LTL_axioms by Def17;

 P1[p1] by A1;

 hence thesis;

 end;

 thus (( 'not' ( 'X' p)) => ( 'X' ( 'not' p))) in X

 proof

 reconsider pp = (( 'not' ( 'X' p)) => ( 'X' ( 'not' p))) as Element of LTL_axioms by Def17;

 P1[pp] by Def22;

 hence thesis;

 end;

 thus (( 'X' ( 'not' p)) => ( 'not' ( 'X' p))) in X

 proof

 reconsider pp = (( 'X' ( 'not' p)) => ( 'not' ( 'X' p))) as Element of LTL_axioms by Def17;

 P1[pp] by Def23;

 hence thesis;

 end;

 thus (( 'X' (p => q)) => (( 'X' p) => ( 'X' q))) in X

 proof

 reconsider pp = (( 'X' (p => q)) => (( 'X' p) => ( 'X' q))) as Element of LTL_axioms by Def17;

 P1[pp] by Def24;

 hence thesis;

 end;

 thus (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) in X

 proof

 reconsider pp = (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) as Element of LTL_axioms by Def17;

 P1[pp] by Def25;

 hence thesis;

 end;

 thus ((p 'U' q) => (( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q))))) in X

 proof

 reconsider pp = ((p 'U' q) => (( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q))))) as Element of LTL_axioms by Def17;

 P1[pp] by Def26;

 hence thesis;

 end;

 thus ((( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q)))) => (p 'U' q)) in X

 proof

 reconsider pp = ((( 'X' q) 'or' ( 'X' (p '&&' (p 'U' q)))) => (p 'U' q)) as Element of LTL_axioms by Def17;

 P1[pp] by Def27;

 hence thesis;

 end;

 thus ((p 'U' q) => ( 'X' ( 'F' q))) in X

 proof

 reconsider pp = ((p 'U' q) => ( 'X' ( 'F' q))) as Element of LTL_axioms by Def17;

 P1[pp] by Def28;

 hence thesis;

 end;

 end;

 then A in LTL_axioms & LTL_axioms c= X by Def18;

 then A in X;

 then ex p be Element of LTL_axioms st A = p & P1[p];

 hence P1[A];

 end;

 theorem :: LTLAXIO1:37



 Th37: A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 implies F |= A

 proof

 assume

 A1: A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6;

 let M;

 assume M |= F;

 let n be Element of NAT ;

 per cases by A1;

 suppose A is axltl1;

 then

 consider B be Element of LTLB_WFF such that

 A2: A = (( 'not' ( 'X' B)) => ( 'X' ( 'not' B)));

 thus thesis by A2, Th15;

 end;

 suppose A is axltl1a;

 then

 consider B be Element of LTLB_WFF such that

 A3: A = (( 'X' ( 'not' B)) => ( 'not' ( 'X' B)));

 thus thesis by A3, Th16;

 end;

 suppose A is axltl2;

 then

 consider B,C be Element of LTLB_WFF such that

 A4: A = (( 'X' (B => C)) => (( 'X' B) => ( 'X' C)));

 thus thesis by A4, Th17;

 end;

 suppose A is axltl3;

 then

 consider B be Element of LTLB_WFF such that

 A5: A = (( 'G' B) => (B '&&' ( 'X' ( 'G' B))));

 thus thesis by A5, Th18;

 end;

 suppose A is axltl4;

 then

 consider B, C such that

 A6: A = ((B 'U' C) => (( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C)))));

 thus thesis by A6, Th19;

 end;

 suppose A is axltl5;

 then

 consider B, C such that

 A7: A = ((( 'X' C) 'or' ( 'X' (B '&&' (B 'U' C)))) => (B 'U' C));

 thus thesis by A7, Th20;

 end;

 suppose A is axltl6;

 then

 consider B, C such that

 A8: A = ((B 'U' C) => ( 'X' ( 'F' C)));

 thus thesis by A8, Th21;

 end;

 end;

 definition

 let i be Nat, f, X;

 :: LTLAXIO1:def29

 pred prc f,X,i means

 : Def29: (f . i) in LTL_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)) IND_rule (f /. i))) or ex j be Nat st 1 <= j & j < i & (f /. j) NEX_rule (f /. i);

 end

 definition

 let X, p;

 :: LTLAXIO1:def30

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

 end

 theorem :: LTLAXIO1:38



 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 prc (f,X,i) implies prc (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: prc (f,X,i);

 per cases by A7;

 suppose (f . i) in LTL_axioms ;

 then (f2 . (i + n)) in LTL_axioms by A2, A3, A4;

 hence prc (f2,X,(i + n));

 end;

 suppose (f . i) in X;

 then (f2 . (i + n)) in X by A2, A3, A4;

 hence prc (f2,X,(i + n));

 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

 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)) IND_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 prc (f2,X,(i + n)) by A6, A12, A13, A19, A18;

 end;

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

 then

 consider j be Nat such that

 A20: 1 <= j and

 A21: j < i and

 A22: (f /. j) NEX_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 prc (f2,X,(i + n)) by A6, A22, A23;

 end;

 end;

 theorem :: LTLAXIO1:39



 Th39: f2 = (f ^ f1) & 1 <= ( len f) & 1 <= ( len f1) & (for i be Nat st 1 <= i & i <= ( len f) holds prc (f,X,i)) & (for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,X,i)) implies for i be Nat st 1 <= i & i <= ( len f2) holds prc (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 prc (f,X,i) and

 A3: for i be Nat st 1 <= i & i <= ( len f1) holds prc (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 LTL_axioms ;

 then (f2 . i) in LTL_axioms by A1, A6, A8, FINSEQ_1: 64;

 hence prc (f2,X,i);

 end;

 suppose (f . i) in X;

 then (f2 . i) in X by A1, A6, A8, FINSEQ_1: 64;

 hence prc (f2,X,i);

 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

 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)) IND_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 prc (f2,X,i) by A9, A10, A11, A12, A13, A14, A17;

 end;

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

 then

 consider j be Nat such that

 A20: 1 <= j and

 A21: j < i and

 A22: (f /. j) NEX_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 prc (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 prc (f2,X,(i1 + ( len f))) by A3, A4, A5, A26, Th38;

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

 end;

 end;

 theorem :: LTLAXIO1:40



 Th40: (f = (f1 ^ <*p*>) & 1 <= ( len f1) & for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,X,i)) & prc (f,X,( len f)) implies (for i be Nat st 1 <= i & i <= ( len f) holds prc (f,X,i)) & X |- 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 prc (f1,X,i);



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

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

 assume

 A4: prc (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 prc (f,X,(i + 0 )) by A2, A5, A7, A10, Th38;

 hence prc (f,X,i);

 end;

 suppose i = ( len f);

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

 end;

 end;

 hence for i be Nat st 1 <= i & i <= ( len f) holds prc (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 |- p by A3, XREAL_1: 31, A6;

 end;

 theorem :: LTLAXIO1:41

 F |- A implies F |= A

 proof

 assume F |- 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,F,i);

 defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies F |= (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 LTL_axioms ;

 then

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

 per cases by A8, Th36;

 suppose (f /. i) is LTL_TAUT_OF_PL;

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

 end;

 suppose (f /. i) is axltl1 or (f /. i) is axltl1a or (f /. i) is axltl2 or (f /. i) is axltl3 or (f /. i) is axltl4 or (f /. i) is axltl5 or (f /. i) is axltl6;

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

 end;

 end;

 suppose (f . i) in F;

 then

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

 thus F |= (f /. i)

 proof

 let M;

 assume M |= F;

 hence M |= (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)) IND_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)) IND_rule (f /. i);

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

 then

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



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

 per cases by A14;

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

 then F |= ((f /. j) => (f /. i)) by A15;

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

 end;

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

 then

 consider A, B such that

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

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

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

 hence F |= (f /. i) by A15, A18, Th27;

 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

 A19: 1 <= j and

 A20: j < i and

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

 P[j] by A5, A20;

 then F |= ( 'X' (f /. j)) by A7, A19, A20, Th25, XXREAL_0: 2;

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

 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 |= A by A2, A22;

 end;

 begin

 theorem :: LTLAXIO1:42



 Th42: p in LTL_axioms or p in X implies X |- p

 proof

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



 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) by FINSEQ_1: 2, TARSKI:def 1;

 then

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

 assume

 A5: p in LTL_axioms or p in X;

 for j be Nat st 1 <= j & j <= ( len g) holds prc (g,X,j)

 proof

 let j be Nat;

 assume

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

 per cases by A5;

 suppose p in LTL_axioms ;

 then (g . j) in LTL_axioms by A3, A4, A6, XXREAL_0: 1;

 hence thesis;

 end;

 suppose p in X;

 then (g . j) in X by A3, A4, A6, XXREAL_0: 1;

 hence thesis;

 end;

 end;

 hence X |- p by A3, A4;

 end;

 theorem :: LTLAXIO1:43



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

 proof

 assume X |- p;

 then

 consider f such that

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

 A2: 1 <= ( len f) and

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

 set j = ( len f);

 assume X |- (p => q);

 then

 consider f1 such that

 A4: (f1 . ( len f1)) = (p => q) and

 A5: 1 <= ( len f1) and

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



 A7: 1 <= (( len f) + ( len f1)) by A2, NAT_1: 12;

 set g = ((f ^ f1) ^ <*q*>);



 A8: g = (f ^ (f1 ^ <*q*>)) by FINSEQ_1: 32;



 A9: for i be Nat st 1 <= i & i <= ( len f1) holds (g . (( len f) + i)) = (f1 . i)

 proof

 let i be Nat;

 assume that

 A10: 1 <= i and

 A11: i <= ( len f1);

 ( len (f1 ^ <*q*>)) = (( len f1) + ( len <*q*>)) by FINSEQ_1: 22

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

 then i <= ( len (f1 ^ <*q*>)) by A11, NAT_1: 12;



 hence (g . (( len f) + i)) = ((f1 ^ <*q*>) . i) by A8, A10, FINSEQ_1: 65

 .= (f1 . i) by A10, A11, FINSEQ_1: 64;

 end;



 A12: ( len g) = (( len (f ^ f1)) + ( len <*q*>)) by FINSEQ_1: 22

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

 then

 A13: ( len g) = ((( len f) + ( len f1)) + 1) by FINSEQ_1: 22;

 then ( len g) = (( len f) + (( len f1) + 1));

 then

 A14: j < ( len g) by NAT_1: 16;



 then

 A15: (g /. j) = (g . j) by A2, Lm1

 .= p by A1, A2, A8, FINSEQ_1: 64;

 set k = (( len f) + ( len f1));



 A16: 1 <= k by A2, NAT_1: 12;

 (g . ( len g)) = q & 1 <= ( len g) by A12, FINSEQ_1: 42, NAT_1: 11;

 then

 A17: (g /. ( len g)) = q by Lm1;



 A18: k < ( len g) by A13, NAT_1: 16;



 then (g /. k) = (g . k) by A2, Lm1, NAT_1: 12

 .= (p => q) by A4, A5, A9;

 then ((g /. j),(g /. k)) MP_rule (g /. ( len g)) by A15, A17;

 then

 A19: ( len (f ^ f1)) = (( len f) + ( len f1)) & prc (g,X,( len g)) by A2, A14, A16, A18, FINSEQ_1: 22;

 for i be Nat st 1 <= i & i <= ( len (f ^ f1)) holds prc ((f ^ f1),X,i) by A2, A3, A5, A6, Th39;

 hence X |- q by A7, A19, Th40;

 end;

 theorem :: LTLAXIO1:44



 Th44: X |- p implies X |- ( 'X' p)

 proof

 assume X |- p;

 then

 consider f such that

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

 A2: 1 <= ( len f) and

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

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



 A4: ( len g) = (( len f) + ( len <*( 'X' p)*>)) 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

 .= p by A1, A2, FINSEQ_1: 64;

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



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

 .= ( 'X' (g /. ( len f))) by A4, A6, FINSEQ_1: 42;

 then (g /. ( len f)) NEX_rule (g /. ( len g));

 then prc (g,X,( len g)) by A2, A5;

 hence X |- ( 'X' p) by A2, A3, Th40;

 end;

 theorem :: LTLAXIO1:45



 Th45: X |- (p => q) & X |- (p => ( 'X' p)) implies X |- (p => ( 'G' q))

 proof

 assume that

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

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

 consider f such that

 A3: (f . ( len f)) = (p => q) and

 A4: 1 <= ( len f) and

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

 consider g such that

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

 A7: 1 <= ( len g) and

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



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

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



 A10: h = (f ^ (g ^ <*(p => ( 'G' q))*>)) 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 <*(p => ( 'G' q))*>)) 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

 .= (p => ( 'G' q)) 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

 .= (p => q) 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

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

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

 then prc (h,X,( len h)) by A4, A12, A15, A17;

 hence X |- (p => ( 'G' q)) by A12, A9, Th40;

 end;

 theorem :: LTLAXIO1:46



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

 proof

 assume

 A1: X |- (r => (p '&&' q));

 set A = ((r => (p '&&' q)) => (r => p));

 A is LTL_TAUT_OF_PL

 proof

 let f be Function of LTLB_WFF , BOOLEAN ;



 thus (( VAL f) . A) = ((( VAL f) . (r => (p '&&' q))) => (( VAL f) . (r => p))) by Def15

 .= (((( VAL f) . r) => (( VAL f) . (p '&&' q))) => (( VAL f) . (r => p))) by Def15

 .= (((( VAL f) . r) => ((( VAL f) . p) '&' (( VAL f) . q))) => (( VAL f) . (r => p))) by Th31

 .= (((( VAL f) . r) => ((( VAL f) . p) '&' (( VAL f) . q))) => ((( VAL f) . r) => (( VAL f) . p))) by Def15

 .= 1 by Th1;

 end;

 then A in LTL_axioms by Def17;

 then X |- A by Th42;

 hence X |- (r => p) by A1, Th43;

 set A = ((r => (p '&&' q)) => (r => q));

 A is LTL_TAUT_OF_PL

 proof

 let f be Function of LTLB_WFF , BOOLEAN ;



 thus (( VAL f) . A) = ((( VAL f) . (r => (p '&&' q))) => (( VAL f) . (r => q))) by Def15

 .= (((( VAL f) . r) => (( VAL f) . (p '&&' q))) => (( VAL f) . (r => q))) by Def15

 .= (((( VAL f) . r) => ((( VAL f) . p) '&' (( VAL f) . q))) => (( VAL f) . (r => q))) by Th31

 .= (((( VAL f) . r) => ((( VAL f) . p) '&' (( VAL f) . q))) => ((( VAL f) . r) => (( VAL f) . q))) by Def15

 .= 1 by Th1;

 end;

 then A in LTL_axioms by Def17;

 then X |- A by Th42;

 hence X |- (r => q) by A1, Th43;

 end;

 theorem :: LTLAXIO1:47



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

 proof

 assume that

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

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

 set A = ((p => q) => ((q => r) => (p => r)));

 now

 let f be Function of LTLB_WFF , BOOLEAN ;



 thus (( VAL f) . A) = ((( VAL f) . (p => q)) => (( VAL f) . ((q => r) => (p => r)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (( VAL f) . ((q => r) => (p => r)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => ((( VAL f) . (q => r)) => (( VAL f) . (p => r)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (((( VAL f) . q) => (( VAL f) . r)) => (( VAL f) . (p => r)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (((( VAL f) . q) => (( VAL f) . r)) => ((( VAL f) . p) => (( VAL f) . r)))) by Def15

 .= 1 by XBOOLEAN: 106;

 end;

 then ((p => q) => ((q => r) => (p => r))) is LTL_TAUT_OF_PL;

 then ((p => q) => ((q => r) => (p => r))) in LTL_axioms by Def17;

 then X |- ((p => q) => ((q => r) => (p => r))) by Th42;

 then X |- ((q => r) => (p => r)) by A1, Th43;

 hence X |- (p => r) by A2, Th43;

 end;

 theorem :: LTLAXIO1:48



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

 proof

 set A = ((p => (q => r)) => ((p '&&' q) => r));

 now

 let f be Function of LTLB_WFF , BOOLEAN ;



 thus (( VAL f) . A) = ((( VAL f) . (p => (q => r))) => (( VAL f) . ((p '&&' q) => r))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . (q => r))) => (( VAL f) . ((p '&&' q) => r))) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) => (( VAL f) . ((p '&&' q) => r))) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) => ((( VAL f) . (p '&&' q)) => (( VAL f) . r))) by Def15

 .= (((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) => (((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r))) by Th31

 .= 1 by Th2;

 end;

 then A is LTL_TAUT_OF_PL;

 then A in LTL_axioms by Def17;

 then

 A1: X |- A by Th42;

 assume X |- (p => (q => r));

 hence X |- ((p '&&' q) => r) by A1, Th43;

 end;

 theorem :: LTLAXIO1:49



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

 proof

 set A = (((p '&&' q) => r) => (p => (q => r)));

 now

 let f be Function of LTLB_WFF , BOOLEAN ;



 thus (( VAL f) . A) = ((( VAL f) . ((p '&&' q) => r)) => (( VAL f) . (p => (q => r)))) by Def15

 .= (((( VAL f) . (p '&&' q)) => (( VAL f) . r)) => (( VAL f) . (p => (q => r)))) by Def15

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => (( VAL f) . (p => (q => r)))) by Th31

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => ((( VAL f) . p) => (( VAL f) . (q => r)))) by Def15

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => ((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r)))) by Def15

 .= 1 by Th3;

 end;

 then A is LTL_TAUT_OF_PL;

 then A in LTL_axioms by Def17;

 then

 A1: X |- A by Th42;

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

 hence X |- (p => (q => r)) by A1, Th43;

 end;

 theorem :: LTLAXIO1:50



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

 proof

 assume that

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

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

 set A = (((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r))));

 now

 let f be Function of LTLB_WFF , BOOLEAN ;



 A3: (( VAL f) . p) = 0 or (( VAL f) . p) = 1 by XBOOLEAN:def 3;



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



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



 A6: (( VAL f) . r) = 0 or (( VAL f) . r) = 1 by XBOOLEAN:def 3;



 thus (( VAL f) . A) = ((( VAL f) . ((p '&&' q) => r)) => (( VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r))))) by Def15

 .= (((( VAL f) . (p '&&' q)) => (( VAL f) . r)) => (( VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r))))) by Def15

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => (( VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r))))) by Th31

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => ((( VAL f) . (p => s)) => (( VAL f) . ((p '&&' q) => (s '&&' r))))) by Def15

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => (((( VAL f) . p) => (( VAL f) . s)) => (( VAL f) . ((p '&&' q) => (s '&&' r))))) by Def15

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => (((( VAL f) . p) => (( VAL f) . s)) => ((( VAL f) . (p '&&' q)) => (( VAL f) . (s '&&' r))))) by Def15

 .= ((((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . r)) => (((( VAL f) . p) => (( VAL f) . s)) => (((( VAL f) . p) '&' (( VAL f) . q)) => (( VAL f) . (s '&&' r))))) by Th31

 .= 1 by A3, A4, A6, A5, Th31;

 end;

 then A is LTL_TAUT_OF_PL;

 then A in LTL_axioms by Def17;

 then X |- A by Th42;

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

 hence thesis by A2, Th43;

 end;

 theorem :: LTLAXIO1:51



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

 proof

 assume that

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

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

 set A = ((p => (q => r)) => ((r => s) => (p => (q => s))));

 now

 let f be Function of LTLB_WFF , BOOLEAN ;



 A3: (( VAL f) . p) = 0 or (( VAL f) . p) = 1 by XBOOLEAN:def 3;



 A4: (( VAL f) . r) = 0 or (( VAL f) . r) = 1 by XBOOLEAN:def 3;

 set B = (( VAL f) . (p => (q => r))), C = (( VAL f) . (r => s)), D = (( VAL f) . (p => (q => s)));



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



 A6: (( VAL f) . s) = 0 or (( VAL f) . s) = 1 by XBOOLEAN:def 3;



 A7: (( VAL f) . (p => (q => s))) = ((( VAL f) . p) => (( VAL f) . (q => s))) by Def15

 .= ((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . s))) by Def15;



 A8: (( VAL f) . (p => (q => r))) = ((( VAL f) . p) => (( VAL f) . (q => r))) by Def15

 .= ((( VAL f) . p) => ((( VAL f) . q) => (( VAL f) . r))) by Def15;



 thus (( VAL f) . A) = (B => (( VAL f) . ((r => s) => (p => (q => s))))) by Def15

 .= (B => (C => D)) by Def15

 .= 1 by A3, A5, A4, A6, A8, A7, Def15;

 end;

 then A is LTL_TAUT_OF_PL;

 then A in LTL_axioms by Def17;

 then X |- A by Th42;

 then X |- ((r => s) => (p => (q => s))) by A1, Th43;

 hence X |- (p => (q => s)) by A2, Th43;

 end;

 theorem :: LTLAXIO1:52



 Th52: X |- (p => q) implies X |- (( 'not' q) => ( 'not' p))

 proof

 set A = ((p => q) => (( 'not' q) => ( 'not' p)));

 now

 let f be Function of LTLB_WFF , BOOLEAN ;



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



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



 thus (( VAL f) . A) = ((( VAL f) . (p => q)) => (( VAL f) . (( 'not' q) => ( 'not' p)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (( VAL f) . (( 'not' q) => ( 'not' p)))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => ((( VAL f) . (q => TFALSUM )) => (( VAL f) . (p => TFALSUM )))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (((( VAL f) . q) => (( VAL f) . TFALSUM )) => (( VAL f) . (p => TFALSUM )))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (((( VAL f) . q) => FALSE ) => (( VAL f) . (p => TFALSUM )))) by Def15

 .= (((( VAL f) . p) => (( VAL f) . q)) => (((( VAL f) . q) => FALSE ) => ((( VAL f) . p) => (( VAL f) . TFALSUM )))) by Def15

 .= 1 by A1, A2;

 end;

 then A is LTL_TAUT_OF_PL;

 then A in LTL_axioms by Def17;

 then

 A3: X |- A by Th42;

 assume X |- (p => q);

 hence thesis by A3, Th43;

 end;

 theorem :: LTLAXIO1:53



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

 proof

 set Xp = ( 'X' p), nq = ( 'not' q), nXq = ( 'not' ( 'X' q)), Xnq = ( 'X' ( 'not' q));

 (Xnq => nXq) in LTL_axioms by Def17;

 then

 A1: X |- (Xnq => nXq) by Th42;

 (( 'not' ( 'X' (p => nq))) => ( 'X' ( 'not' (p => nq)))) in LTL_axioms by Def17;

 then

 A2: X |- (( 'not' ( 'X' (p => nq))) => ( 'X' ( 'not' (p => nq)))) by Th42;

 (( 'X' (p => nq)) => (Xp => Xnq)) in LTL_axioms by Def17;

 then X |- (( 'X' (p => nq)) => (Xp => Xnq)) by Th42;

 then X |- (( 'X' (p => nq)) => (Xp => nXq)) by A1, Th51;

 then X |- (( 'not' (Xp => nXq)) => ( 'not' ( 'X' (p => nq)))) by Th52;

 hence thesis by A2, Th47;

 end;

 theorem :: LTLAXIO1:54



 Th54: F |- p implies F |- ( 'G' p)

 proof

 assume

 A1: F |- p;

 (p => (p => p)) in LTL_axioms by Th34;

 then F |- (p => (p => p)) by Th42;

 then

 A2: F |- (p => p) by A1, Th43;

 (( 'X' p) => (p => ( 'X' p))) in LTL_axioms by Th34;

 then

 A3: F |- (( 'X' p) => (p => ( 'X' p))) by Th42;

 F |- ( 'X' p) by A1, Th44;

 then F |- (p => ( 'X' p)) by A3, Th43;

 then F |- (p => ( 'G' p)) by A2, Th45;

 hence F |- ( 'G' p) by A1, Th43;

 end;

 theorem :: LTLAXIO1:55



 Th55: (p => q) in F implies (F \/ {p}) |- ( 'G' q)

 proof

 p in {p} by TARSKI:def 1;

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

 then

 A1: (F \/ {p}) |- p by Th42;

 assume (p => q) in F;

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

 then (F \/ {p}) |- (p => q) by Th42;

 then (F \/ {p}) |- q by A1, Th43;

 hence (F \/ {p}) |- ( 'G' q) by Th54;

 end;

 theorem :: LTLAXIO1:56



 Th56: F |- q implies (F \/ {p}) |- q

 proof

 assume F |- q;

 then

 consider f such that

 A1: (f . ( len f)) = q & 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);

 then (f . i) in LTL_axioms or (f . i) in F 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) by Def29, A2;

 then (f . i) in LTL_axioms or (f . i) in (F \/ {p}) 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) by XBOOLE_0:def 3;

 hence prc (f,(F \/ {p}),i);

 end;

 hence (F \/ {p}) |- q by A1;

 end;

 theorem :: LTLAXIO1:57



 Th57: (F \/ {p}) |- q implies F |- (( 'G' p) => q)

 proof

 set G = (F \/ {p});

 assume G |- q;

 then

 consider f such that

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

 A2: 1 <= ( len f) and

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

 defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies F |- (( 'G' p) => (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 LTL_axioms ;

 set t = (f /. i);

 (t => (( 'G' p) => t)) in LTL_axioms by Th34;

 then

 A9: F |- (t => (( 'G' p) => t)) by Th42;

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

 then F |- t by Th42;

 hence thesis by A9, Th43;

 end;

 suppose

 A10: (f . i) in G;

 per cases by A10, XBOOLE_0:def 3;

 suppose

 A11: (f . i) in F;

 set t = (f /. i);

 (t => (( 'G' p) => t)) in LTL_axioms by Th34;

 then

 A12: F |- (t => (( 'G' p) => t)) by Th42;

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

 then F |- t by Th42;

 hence thesis by A12, Th43;

 end;

 suppose

 A13: (f . i) in {p};

 (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) in LTL_axioms by Def17;

 then

 A14: F |- (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) by Th42;

 (f . i) = p by A13, TARSKI:def 1;

 then (f /. i) = p by A6, A7, Lm1;

 hence thesis by A14, Th46;

 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)) 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: F |- (( 'G' p) => (f /. j)) by A5, A15, A16;

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

 then

 A21: F |- (( 'G' p) => (f /. k)) by A5, A17, A18;

 per cases by A19;

 suppose

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

 set t3 = ((( 'G' p) => ((f /. j) => (f /. i))) => ((( 'G' p) => (f /. j)) => (( 'G' p) => (f /. i))));

 t3 in LTL_axioms by Th35;

 then

 A23: F |- t3 by Th42;

 F |- (( 'G' p) => ((f /. j) => (f /. i))) by A21, A22;

 then F |- ((( 'G' p) => (f /. j)) => (( 'G' p) => (f /. i))) by A23, Th43;

 hence F |- (( 'G' p) => (f /. i)) by A20, Th43;

 end;

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

 then

 consider A, B such that

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

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

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

 set Gp = ( 'G' p), XGp = ( 'X' ( 'G' p)), XA = ( 'X' A), Xq = ( 'X' q), GB = ( 'G' B);

 (Gp => (p '&&' XGp)) in LTL_axioms by Def17;

 then F |- (Gp => (p '&&' XGp)) by Th42;

 then

 A27: F |- (Gp => XGp) by Th46;

 F |- ((Gp '&&' A) => XA) by A21, A25, Th48;

 then

 A28: F |- ((Gp '&&' A) => (XGp '&&' XA)) by A27, Th50;

 F |- ((XGp '&&' XA) => ( 'X' (Gp '&&' A))) by Th53;

 then

 A29: F |- ((Gp '&&' A) => ( 'X' (Gp '&&' A))) by A28, Th47;

 F |- ((Gp '&&' A) => B) by A20, A24, Th48;

 then F |- ((Gp '&&' A) => GB) by A29, Th45;

 hence thesis by A26, Th49;

 end;

 end;

 suppose

 A30: ex j be Nat st 1 <= j & j (p '&&' ( 'X' ( 'G' p)))) in LTL_axioms by Def17;

 then F |- (( 'G' p) => (p '&&' ( 'X' ( 'G' p)))) by Th42;

 then

 A31: F |- (( 'G' p) => ( 'X' ( 'G' p))) by Th46;

 consider j be Nat, q, r such that

 A32: 1 <= j and

 A33: j (f /. j))) => (( 'X' ( 'G' p)) => ( 'X' (f /. j)))) in LTL_axioms by Def17;

 then

 A35: F |- (( 'X' (( 'G' p) => (f /. j))) => (( 'X' ( 'G' p)) => ( 'X' (f /. j)))) by Th42;

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

 then F |- ( 'X' (( 'G' p) => (f /. j))) by A5, A32, A33, Th44;

 then

 A36: F |- (( 'X' ( 'G' p)) => ( 'X' (f /. j))) by A35, Th43;

 (f /. i) = ( 'X' (f /. j)) by A34;

 hence thesis by A36, A31, Th47;

 end;

 end;

 end;



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

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

 hence F |- (( 'G' p) => q) by A2, A37;

 end;

 theorem :: LTLAXIO1:58

 F |- (p => q) implies (F \/ {p}) |- q

 proof

 p in {p} by TARSKI:def 1;

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

 then

 A1: (F \/ {p}) |- p by Th42;

 assume F |- (p => q);

 then (F \/ {p}) |- (p => q) by Th56;

 hence (F \/ {p}) |- q by A1, Th43;

 end;

 theorem :: LTLAXIO1:59

 F |- (( 'G' p) => q) implies (F \/ {p}) |- q

 proof

 p in {p} by TARSKI:def 1;

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

 then (F \/ {p}) |- p by Th42;

 then

 A1: (F \/ {p}) |- ( 'G' p) by Th54;

 assume F |- (( 'G' p) => q);

 then (F \/ {p}) |- (( 'G' p) => q) by Th56;

 hence (F \/ {p}) |- q by A1, Th43;

 end;

 theorem :: LTLAXIO1:60

 F |- (( 'G' (p => q)) => (( 'G' p) => ( 'G' q)))

 proof

 reconsider G = ((F \/ {(p => q)}) \/ {p}) as Subset of LTLB_WFF ;

 (p => q) in {(p => q)} by TARSKI:def 1;

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

 then G |- ( 'G' q) by Th55;

 then (F \/ {(p => q)}) |- (( 'G' p) => ( 'G' q)) by Th57;

 hence thesis by Th57;

 end;