:: The Axiomatization of Propositional Linear Time Temporal Logic
:: by Mariusz Giero
::
:: Received November 20, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users


begin

Th1: for X being set
for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
proof end;

theorem Th2: :: LTLAXIO1:1
for a, b, c being boolean number holds (a => (b '&' c)) => (a => b) = 1
proof end;

theorem Th3: :: LTLAXIO1:2
for a, b, c being boolean number holds (a => (b => c)) => ((a '&' b) => c) = 1
proof end;

theorem Th4: :: LTLAXIO1:3
for a, b, c being boolean number holds ((a '&' b) => c) => (a => (b => c)) = 1
proof end;

begin

notation
synonym LTLB_WFF for HP-WFF ;
end;

notation
synonym TFALSUM for VERUM ;
end;

notation
let p, q be Element of LTLB_WFF ;
synonym p 'Us' q for p '&' q;
end;

theorem Th5: :: LTLAXIO1:4
for A being Element of LTLB_WFF holds
( A = TFALSUM or ex n being Element of NAT st
( A = prop n or ex p, q being Element of LTLB_WFF st
( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'Us' q ) ) )
proof end;

definition
let p be Element of LTLB_WFF ;
func 'not' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 1
p => TFALSUM;
correctness
coherence
p => TFALSUM is Element of LTLB_WFF
;
;
func 'X' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 2
TFALSUM 'Us' p;
correctness
coherence
TFALSUM 'Us' p is Element of LTLB_WFF
;
;
end;

:: deftheorem defines 'not' LTLAXIO1:def 1 :
for p being Element of LTLB_WFF holds 'not' p = p => TFALSUM;

:: deftheorem defines 'X' LTLAXIO1:def 2 :
for p being Element of LTLB_WFF holds 'X' p = TFALSUM 'Us' p;

definition
func TVERUM -> Element of LTLB_WFF equals :: LTLAXIO1:def 3
'not' TFALSUM;
correctness
coherence
'not' TFALSUM is Element of LTLB_WFF
;
;
end;

:: deftheorem defines TVERUM LTLAXIO1:def 3 :
TVERUM = 'not' TFALSUM;

definition
let p, q be Element of LTLB_WFF ;
func p '&&' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 4
(p => (q => TFALSUM)) => TFALSUM;
correctness
coherence
(p => (q => TFALSUM)) => TFALSUM is Element of LTLB_WFF
;
;
end;

:: deftheorem defines '&&' LTLAXIO1:def 4 :
for p, q being Element of LTLB_WFF holds p '&&' q = (p => (q => TFALSUM)) => TFALSUM;

definition
let p, q be Element of LTLB_WFF ;
func p 'or' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 5
'not' (('not' p) '&&' ('not' q));
correctness
coherence
'not' (('not' p) '&&' ('not' q)) is Element of LTLB_WFF
;
;
end;

:: deftheorem defines 'or' LTLAXIO1:def 5 :
for p, q being Element of LTLB_WFF holds p 'or' q = 'not' (('not' p) '&&' ('not' q));

definition
let p be Element of LTLB_WFF ;
func 'G' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 6
'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p))));
correctness
coherence
'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p)))) is Element of LTLB_WFF
;
;
end;

:: deftheorem defines 'G' LTLAXIO1:def 6 :
for p being Element of LTLB_WFF holds 'G' p = 'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p))));

definition
let p be Element of LTLB_WFF ;
func 'F' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 7
'not' ('G' ('not' p));
correctness
coherence
'not' ('G' ('not' p)) is Element of LTLB_WFF
;
;
end;

:: deftheorem defines 'F' LTLAXIO1:def 7 :
for p being Element of LTLB_WFF holds 'F' p = 'not' ('G' ('not' p));

definition
let p, q be Element of LTLB_WFF ;
func p 'U' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 8
q 'or' (p '&&' (p 'Us' q));
correctness
coherence
q 'or' (p '&&' (p 'Us' q)) is Element of LTLB_WFF
;
;
end;

:: deftheorem defines 'U' LTLAXIO1:def 8 :
for p, q being Element of LTLB_WFF holds p 'U' q = q 'or' (p '&&' (p 'Us' q));

definition
let p, q be Element of LTLB_WFF ;
func p 'R' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 9
'not' (('not' p) 'U' ('not' q));
correctness
coherence
'not' (('not' p) 'U' ('not' q)) is Element of LTLB_WFF
;
;
end;

:: deftheorem defines 'R' LTLAXIO1:def 9 :
for p, q being Element of LTLB_WFF holds p 'R' q = 'not' (('not' p) 'U' ('not' q));

begin

definition
func props -> Subset of LTLB_WFF means :: LTLAXIO1:def 10
for x being set holds
( x in it iff ex n being Element of NAT st x = prop n );
existence
ex b1 being Subset of LTLB_WFF st
for x being set holds
( x in b1 iff ex n being Element of NAT st x = prop n )
proof end;
uniqueness
for b1, b2 being Subset of LTLB_WFF st ( for x being set holds
( x in b1 iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds
( x in b2 iff ex n being Element of NAT st x = prop n ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines props LTLAXIO1:def 10 :
for b1 being Subset of LTLB_WFF holds
( b1 = props iff for x being set holds
( x in b1 iff ex n being Element of NAT st x = prop n ) );

definition
mode LTLModel is sequence of (bool props);
end;

definition
let M be LTLModel;
func SAT M -> Function of [:NAT,LTLB_WFF:],BOOLEAN means :Def12: :: LTLAXIO1:def 11
for n being Element of NAT holds
( it . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( it . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( it . [n,(p => q)] = (it . [n,p]) => (it . [n,q]) & ( it . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & it . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
it . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & it . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
it . [(n + j),p] = 1 ) ) implies it . [n,(p 'Us' q)] = 1 ) ) ) );
existence
ex b1 being Function of [:NAT,LTLB_WFF:],BOOLEAN st
for n being Element of NAT holds
( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'Us' q)] = 1 ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN st ( for n being Element of NAT holds
( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'Us' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds
( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'Us' q)] = 1 ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines SAT LTLAXIO1:def 11 :
for M being LTLModel
for b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN holds
( b2 = SAT M iff for n being Element of NAT holds
( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'Us' q)] = 1 ) ) ) ) );

theorem Th6: :: LTLAXIO1:5
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
proof end;

theorem Th7: :: LTLAXIO1:6
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,TVERUM] = 1
proof end;

theorem Th8: :: LTLAXIO1:7
for A, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
proof end;

theorem Th9: :: LTLAXIO1:8
for A, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
proof end;

theorem Th10: :: LTLAXIO1:9
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
proof end;

theorem Th11: :: LTLAXIO1:10
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )
proof end;

theorem Th12: :: LTLAXIO1:11
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
proof end;

theorem Th13: :: LTLAXIO1:12
for p, q being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) )
proof end;

theorem :: LTLAXIO1:13
for p, q being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
proof end;

theorem Th15: :: LTLAXIO1:14
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]
proof end;

theorem Th16: :: LTLAXIO1:15
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
proof end;

theorem Th17: :: LTLAXIO1:16
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1
proof end;

theorem Th18: :: LTLAXIO1:17
for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
proof end;

theorem Th19: :: LTLAXIO1:18
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
proof end;

theorem Th20: :: LTLAXIO1:19
for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1
proof end;

theorem Th21: :: LTLAXIO1:20
for C, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1
proof end;

theorem Th22: :: LTLAXIO1:21
for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1
proof end;

begin

definition
let M be LTLModel;
let p be Element of LTLB_WFF ;
pred M |= p means :Def13: :: LTLAXIO1:def 12
for n being Element of NAT holds (SAT M) . [n,p] = 1;
end;

:: deftheorem Def13 defines |= LTLAXIO1:def 12 :
for M being LTLModel
for p being Element of LTLB_WFF holds
( M |= p iff for n being Element of NAT holds (SAT M) . [n,p] = 1 );

definition
let M be LTLModel;
let F be Subset of LTLB_WFF;
pred M |= F means :Def14: :: LTLAXIO1:def 13
for p being Element of LTLB_WFF st p in F holds
M |= p;
end;

:: deftheorem Def14 defines |= LTLAXIO1:def 13 :
for M being LTLModel
for F being Subset of LTLB_WFF holds
( M |= F iff for p being Element of LTLB_WFF st p in F holds
M |= p );

definition
let F be Subset of LTLB_WFF;
let p be Element of LTLB_WFF ;
pred F |= p means :Def15: :: LTLAXIO1:def 14
for M being LTLModel st M |= F holds
M |= p;
end;

:: deftheorem Def15 defines |= LTLAXIO1:def 14 :
for F being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( F |= p iff for M being LTLModel st M |= F holds
M |= p );

theorem Th23: :: LTLAXIO1:22
for F, G being Subset of LTLB_WFF
for M being LTLModel holds
( ( M |= F & M |= G ) iff M |= F \/ G )
proof end;

theorem Th24: :: LTLAXIO1:23
for A being Element of LTLB_WFF
for M being LTLModel holds
( M |= A iff M |= {A} )
proof end;

theorem Th25: :: LTLAXIO1:24
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & F |= A => B holds
F |= B
proof end;

theorem Th26: :: LTLAXIO1:25
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A holds
F |= 'X' A
proof end;

theorem :: LTLAXIO1:26
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A holds
F |= 'G' A
proof end;

theorem Th28: :: LTLAXIO1:27
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds
F |= A => ('G' B)
proof end;

theorem Th29: :: LTLAXIO1:28
for A being Element of LTLB_WFF
for i, j being Element of NAT
for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]
proof end;

theorem Th30: :: LTLAXIO1:29
for F being Subset of LTLB_WFF
for i being Element of NAT
for M being LTLModel st M |= F holds
M ^\ i |= F
proof end;

theorem :: LTLAXIO1:30
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F \/ {A} |= B iff F |= ('G' A) => B )
proof end;

definition
let f be Function of LTLB_WFF,BOOLEAN;
func VAL f -> Function of LTLB_WFF,BOOLEAN means :Def16: :: LTLAXIO1:def 15
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( it . TFALSUM = 0 & it . (prop n) = f . (prop n) & it . (A => B) = (it . A) => (it . B) & it . (A 'Us' B) = f . (A 'Us' B) );
existence
ex b1 being Function of LTLB_WFF,BOOLEAN st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = 0 & b1 . (prop n) = f . (prop n) & b1 . (A => B) = (b1 . A) => (b1 . B) & b1 . (A 'Us' B) = f . (A 'Us' B) )
proof end;
uniqueness
for b1, b2 being Function of LTLB_WFF,BOOLEAN st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = 0 & b1 . (prop n) = f . (prop n) & b1 . (A => B) = (b1 . A) => (b1 . B) & b1 . (A 'Us' B) = f . (A 'Us' B) ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b2 . TFALSUM = 0 & b2 . (prop n) = f . (prop n) & b2 . (A => B) = (b2 . A) => (b2 . B) & b2 . (A 'Us' B) = f . (A 'Us' B) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines VAL LTLAXIO1:def 15 :
for f, b2 being Function of LTLB_WFF,BOOLEAN holds
( b2 = VAL f iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b2 . TFALSUM = 0 & b2 . (prop n) = f . (prop n) & b2 . (A => B) = (b2 . A) => (b2 . B) & b2 . (A 'Us' B) = f . (A 'Us' B) ) );

theorem Th32: :: LTLAXIO1:31
for f being Function of LTLB_WFF,BOOLEAN
for p, q being Element of LTLB_WFF holds (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)
proof end;

theorem Th33: :: LTLAXIO1:32
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
proof end;

definition
let p be Element of LTLB_WFF ;
attr p is LTL_TAUT_OF_PL means :Def17: :: LTLAXIO1:def 16
for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1;
end;

:: deftheorem Def17 defines LTL_TAUT_OF_PL LTLAXIO1:def 16 :
for p being Element of LTLB_WFF holds
( p is LTL_TAUT_OF_PL iff for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1 );

theorem Th34: :: LTLAXIO1:33
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A is LTL_TAUT_OF_PL holds
F |= A
proof end;

begin

definition
let D be set ;
attr D is with_LTL_axioms means :Def18: :: LTLAXIO1:def 17
for p, q being Element of LTLB_WFF 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 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D & (p 'Us' q) => ('X' ('F' q)) in D );
end;

:: deftheorem Def18 defines with_LTL_axioms LTLAXIO1:def 17 :
for D being set holds
( D is with_LTL_axioms iff for p, q being Element of LTLB_WFF 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 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D & (p 'Us' q) => ('X' ('F' q)) in D ) );

definition
func LTL_axioms -> Subset of LTLB_WFF means :Def19: :: LTLAXIO1:def 18
( it is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
it c= D ) );
existence
ex b1 being Subset of LTLB_WFF st
( b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being Subset of LTLB_WFF st b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b1 c= D ) & b2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines LTL_axioms LTLAXIO1:def 18 :
for b1 being Subset of LTLB_WFF holds
( b1 = LTL_axioms iff ( b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b1 c= D ) ) );

registration
cluster LTL_axioms -> with_LTL_axioms ;
coherence
LTL_axioms is with_LTL_axioms
by Def19;
end;

theorem Th36: :: LTLAXIO1:34
for p, q being Element of LTLB_WFF holds p => (q => p) in LTL_axioms
proof end;

theorem Th37: :: LTLAXIO1:35
for p, q, r being Element of LTLB_WFF holds (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms
proof end;

definition
let p, q be Element of LTLB_WFF ;
pred p NEX_rule q means :Def20: :: LTLAXIO1:def 19
q = 'X' p;
let r be Element of LTLB_WFF ;
pred p,q MP_rule r means :Def21: :: LTLAXIO1:def 20
q = p => r;
pred p,q IND_rule r means :Def22: :: LTLAXIO1:def 21
ex A, B being Element of LTLB_WFF st
( p = A => B & q = A => ('X' A) & r = A => ('G' B) );
end;

:: deftheorem Def20 defines NEX_rule LTLAXIO1:def 19 :
for p, q being Element of LTLB_WFF holds
( p NEX_rule q iff q = 'X' p );

:: deftheorem Def21 defines MP_rule LTLAXIO1:def 20 :
for p, q, r being Element of LTLB_WFF holds
( p,q MP_rule r iff q = p => r );

:: deftheorem Def22 defines IND_rule LTLAXIO1:def 21 :
for p, q, r being Element of LTLB_WFF holds
( p,q IND_rule r iff ex A, B being Element of LTLB_WFF st
( p = A => B & q = A => ('X' A) & r = A => ('G' B) ) );

registration
cluster LTL_axioms -> non empty ;
coherence
not LTL_axioms is empty
by Def18;
end;

definition
let A be Element of LTLB_WFF ;
attr A is axltl1 means :Def23: :: LTLAXIO1:def 22
ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B));
attr A is axltl1a means :Def24: :: LTLAXIO1:def 23
ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B));
attr A is axltl2 means :Def25: :: LTLAXIO1:def 24
ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C));
attr A is axltl3 means :Def26: :: LTLAXIO1:def 25
ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B)));
attr A is axltl4 means :Def27: :: LTLAXIO1:def 26
ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C))));
attr A is axltl5 means :Def28: :: LTLAXIO1:def 27
ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C);
attr A is axltl6 means :Def29: :: LTLAXIO1:def 28
ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => ('X' ('F' C));
end;

:: deftheorem Def23 defines axltl1 LTLAXIO1:def 22 :
for A being Element of LTLB_WFF holds
( A is axltl1 iff ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B)) );

:: deftheorem Def24 defines axltl1a LTLAXIO1:def 23 :
for A being Element of LTLB_WFF holds
( A is axltl1a iff ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B)) );

:: deftheorem Def25 defines axltl2 LTLAXIO1:def 24 :
for A being Element of LTLB_WFF holds
( A is axltl2 iff ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C)) );

:: deftheorem Def26 defines axltl3 LTLAXIO1:def 25 :
for A being Element of LTLB_WFF holds
( A is axltl3 iff ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B))) );

:: deftheorem Def27 defines axltl4 LTLAXIO1:def 26 :
for A being Element of LTLB_WFF holds
( A is axltl4 iff ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) );

:: deftheorem Def28 defines axltl5 LTLAXIO1:def 27 :
for A being Element of LTLB_WFF holds
( A is axltl5 iff ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C) );

:: deftheorem Def29 defines axltl6 LTLAXIO1:def 28 :
for A being Element of LTLB_WFF holds
( A is axltl6 iff ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => ('X' ('F' C)) );

theorem Th38: :: LTLAXIO1:36
for A being 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 end;

theorem Th39: :: LTLAXIO1:37
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st ( 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 ) holds
F |= A
proof end;

definition
let i be Nat;
let f be FinSequence of LTLB_WFF ;
let X be Subset of LTLB_WFF;
pred prc f,X,i means :Def30: :: LTLAXIO1:def 29
( f . i in LTL_axioms or f . i in X or ex j, k being 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 being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) );
end;

:: deftheorem Def30 defines prc LTLAXIO1:def 29 :
for i being Nat
for f being FinSequence of LTLB_WFF
for X being Subset of LTLB_WFF holds
( prc f,X,i iff ( f . i in LTL_axioms or f . i in X or ex j, k being 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 being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) );

definition
let X be Subset of LTLB_WFF;
let p be Element of LTLB_WFF ;
pred X |- p means :Def31: :: LTLAXIO1:def 30
ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) );
end;

:: deftheorem Def31 defines |- LTLAXIO1:def 30 :
for X being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( X |- p iff ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) ) );

theorem Th40: :: LTLAXIO1:38
for X being Subset of LTLB_WFF
for f, f2 being FinSequence of LTLB_WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,X,i holds
prc f2,X,i + n
proof end;

theorem Th41: :: LTLAXIO1:39
for X being Subset of LTLB_WFF
for f2, f, f1 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i
proof end;

theorem Th42: :: LTLAXIO1:40
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF
for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
proof end;

theorem :: LTLAXIO1:41
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- A holds
F |= A
proof end;

begin

theorem Th44: :: LTLAXIO1:42
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds
X |- p
proof end;

theorem Th45: :: LTLAXIO1:43
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p & X |- p => q holds
X |- q
proof end;

theorem Th46: :: LTLAXIO1:44
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p holds
X |- 'X' p
proof end;

theorem Th47: :: LTLAXIO1:45
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => q & X |- p => ('X' p) holds
X |- p => ('G' q)
proof end;

theorem Th48: :: LTLAXIO1:46
for r, p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- r => (p '&&' q) holds
( X |- r => p & X |- r => q )
proof end;

theorem Th49: :: LTLAXIO1:47
for p, q, r being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => q & X |- q => r holds
X |- p => r
proof end;

theorem Th50: :: LTLAXIO1:48
for p, q, r being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => (q => r) holds
X |- (p '&&' q) => r
proof end;

theorem Th51: :: LTLAXIO1:49
for p, q, r being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- (p '&&' q) => r holds
X |- p => (q => r)
proof end;

theorem Th52: :: LTLAXIO1:50
for p, q, r, s being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- (p '&&' q) => r & X |- p => s holds
X |- (p '&&' q) => (s '&&' r)
proof end;

theorem Th53: :: LTLAXIO1:51
for p, q, r, s being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => (q => r) & X |- r => s holds
X |- p => (q => s)
proof end;

theorem Th54: :: LTLAXIO1:52
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => q holds
X |- ('not' q) => ('not' p)
proof end;

theorem Th55: :: LTLAXIO1:53
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF holds X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))
proof end;

theorem Th56: :: LTLAXIO1:54
for p being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- p holds
F |- 'G' p
proof end;

theorem Th57: :: LTLAXIO1:55
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st p => q in F holds
F \/ {p} |- 'G' q
proof end;

theorem Th58: :: LTLAXIO1:56
for q, p being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- q holds
F \/ {p} |- q
proof end;

theorem Th59: :: LTLAXIO1:57
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F \/ {p} |- q holds
F |- ('G' p) => q
proof end;

theorem :: LTLAXIO1:58
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- p => q holds
F \/ {p} |- q
proof end;

theorem :: LTLAXIO1:59
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- ('G' p) => q holds
F \/ {p} |- q
proof end;

theorem :: LTLAXIO1:60
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q))
proof end;