:: 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 b₁ being Subset of LTLB_WFF st
for x being set holds
( x in b₁ iff ex n being Element of NAT st x = prop n )

proof end;

uniqueness
for b₁, b₂ being Subset of LTLB_WFF st ( for x being set holds
( x in b₁ iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds
( x in b₂ iff ex n being Element of NAT st x = prop n ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines props LTLAXIO1:def 10 :
for b₁ being Subset of LTLB_WFF holds
( b₁ = props iff for x being set holds
( x in b₁ 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 b₁ being Function of [:NAT,LTLB_WFF:],BOOLEAN st
for n being Element of NAT holds
( b₁ . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b₁ . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b₁ . [n,(p => q)] = (b₁ . [n,p]) => (b₁ . [n,q]) & ( b₁ . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b₁ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₁ . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b₁ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₁ . [(n + j),p] = 1 ) ) implies b₁ . [n,(p 'Us' q)] = 1 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT,LTLB_WFF:],BOOLEAN st ( for n being Element of NAT holds
( b₁ . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b₁ . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b₁ . [n,(p => q)] = (b₁ . [n,p]) => (b₁ . [n,q]) & ( b₁ . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b₁ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₁ . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b₁ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₁ . [(n + j),p] = 1 ) ) implies b₁ . [n,(p 'Us' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds
( b₂ . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b₂ . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b₂ . [n,(p => q)] = (b₂ . [n,p]) => (b₂ . [n,q]) & ( b₂ . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b₂ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₂ . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b₂ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₂ . [(n + j),p] = 1 ) ) implies b₂ . [n,(p 'Us' q)] = 1 ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines SAT LTLAXIO1:def 11 :
for M being LTLModel
for b₂ being Function of [:NAT,LTLB_WFF:],BOOLEAN holds
( b₂ = SAT M iff for n being Element of NAT holds
( b₂ . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b₂ . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b₂ . [n,(p => q)] = (b₂ . [n,p]) => (b₂ . [n,q]) & ( b₂ . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b₂ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₂ . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b₂ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₂ . [(n + j),p] = 1 ) ) implies b₂ . [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 b₁ being Function of LTLB_WFF,BOOLEAN st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = 0 & b₁ . (prop n) = f . (prop n) & b₁ . (A => B) = (b₁ . A) => (b₁ . B) & b₁ . (A 'Us' B) = f . (A 'Us' B) )

proof end;

uniqueness
for b₁, b₂ being Function of LTLB_WFF,BOOLEAN st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = 0 & b₁ . (prop n) = f . (prop n) & b₁ . (A => B) = (b₁ . A) => (b₁ . B) & b₁ . (A 'Us' B) = f . (A 'Us' B) ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₂ . TFALSUM = 0 & b₂ . (prop n) = f . (prop n) & b₂ . (A => B) = (b₂ . A) => (b₂ . B) & b₂ . (A 'Us' B) = f . (A 'Us' B) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines VAL LTLAXIO1:def 15 :
for f, b₂ being Function of LTLB_WFF,BOOLEAN holds
( b₂ = VAL f iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₂ . TFALSUM = 0 & b₂ . (prop n) = f . (prop n) & b₂ . (A => B) = (b₂ . A) => (b₂ . B) & b₂ . (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 b₁ being Subset of LTLB_WFF st
( b₁ is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ being Subset of LTLB_WFF st b₁ is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b₁ c= D ) & b₂ is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b₂ c= D ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines LTL_axioms LTLAXIO1:def 18 :
for b₁ being Subset of LTLB_WFF holds
( b₁ = LTL_axioms iff ( b₁ is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b₁ 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;