:: by Mariusz Giero

::

:: Received November 20, 2010

:: Copyright (c) 2010-2018 Association of Mizar Users

Lm1: 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 Th4: :: 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 'U' q ) ) )

( 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 'U' q ) ) )

proof end;

definition

let p be Element of LTLB_WFF ;

correctness

coherence

p => TFALSUM is Element of LTLB_WFF ;

;

correctness

coherence

TFALSUM 'U' p is Element of LTLB_WFF ;

;

end;
correctness

coherence

p => TFALSUM is Element of LTLB_WFF ;

;

correctness

coherence

TFALSUM 'U' p is Element of LTLB_WFF ;

;

:: deftheorem defines 'not' LTLAXIO1:def 1 :

for p being Element of LTLB_WFF holds 'not' p = p => TFALSUM;

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 'U' p;

for p being Element of LTLB_WFF holds 'X' p = TFALSUM 'U' p;

definition

let p, q be Element of LTLB_WFF ;

correctness

coherence

'not' (p => ('not' q)) is Element of LTLB_WFF ;

;

end;
correctness

coherence

'not' (p => ('not' q)) is Element of LTLB_WFF ;

;

:: deftheorem defines '&&' LTLAXIO1:def 4 :

for p, q being Element of LTLB_WFF holds p '&&' q = 'not' (p => ('not' q));

for p, q being Element of LTLB_WFF holds p '&&' q = 'not' (p => ('not' q));

definition

let p, q be Element of LTLB_WFF ;

correctness

coherence

'not' (('not' p) '&&' ('not' q)) is Element of LTLB_WFF ;

;

end;
correctness

coherence

'not' (('not' p) '&&' ('not' q)) is Element of LTLB_WFF ;

;

:: deftheorem defines 'or' LTLAXIO1:def 5 :

for p, q being Element of LTLB_WFF holds p 'or' q = 'not' (('not' p) '&&' ('not' q));

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 ;

coherence

'not' (('not' p) 'or' (TVERUM 'U' ('not' p))) is Element of LTLB_WFF ;

;

end;
func 'G' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 6

'not' (('not' p) 'or' (TVERUM 'U' ('not' p)));

correctness 'not' (('not' p) 'or' (TVERUM 'U' ('not' p)));

coherence

'not' (('not' p) 'or' (TVERUM 'U' ('not' p))) is Element of LTLB_WFF ;

;

:: deftheorem defines 'G' LTLAXIO1:def 6 :

for p being Element of LTLB_WFF holds 'G' p = 'not' (('not' p) 'or' (TVERUM 'U' ('not' p)));

for p being Element of LTLB_WFF holds 'G' p = 'not' (('not' p) 'or' (TVERUM 'U' ('not' p)));

definition

let p be Element of LTLB_WFF ;

correctness

coherence

'not' ('G' ('not' p)) is Element of LTLB_WFF ;

;

end;
correctness

coherence

'not' ('G' ('not' p)) is Element of LTLB_WFF ;

;

:: deftheorem defines 'F' LTLAXIO1:def 7 :

for p being Element of LTLB_WFF holds 'F' p = 'not' ('G' ('not' p));

for p being Element of LTLB_WFF holds 'F' p = 'not' ('G' ('not' p));

definition

let p, q be Element of LTLB_WFF ;

correctness

coherence

q 'or' (p '&&' (p 'U' q)) is Element of LTLB_WFF ;

;

end;
correctness

coherence

q 'or' (p '&&' (p 'U' q)) is Element of LTLB_WFF ;

;

:: deftheorem defines 'Uw' LTLAXIO1:def 8 :

for p, q being Element of LTLB_WFF holds p 'Uw' q = q 'or' (p '&&' (p 'U' q));

for p, q being Element of LTLB_WFF holds p 'Uw' q = q 'or' (p '&&' (p 'U' q));

definition

let p, q be Element of LTLB_WFF ;

correctness

coherence

'not' (('not' p) 'Uw' ('not' q)) is Element of LTLB_WFF ;

;

end;
correctness

coherence

'not' (('not' p) 'Uw' ('not' q)) is Element of LTLB_WFF ;

;

:: deftheorem defines 'R' LTLAXIO1:def 9 :

for p, q being Element of LTLB_WFF holds p 'R' q = 'not' (('not' p) 'Uw' ('not' q));

for p, q being Element of LTLB_WFF holds p 'R' q = 'not' (('not' p) 'Uw' ('not' q));

definition

ex b_{1} being Subset of LTLB_WFF st

for x being set holds

( x in b_{1} iff ex n being Element of NAT st x = prop n )

for b_{1}, b_{2} being Subset of LTLB_WFF st ( for x being set holds

( x in b_{1} iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds

( x in b_{2} iff ex n being Element of NAT st x = prop n ) ) holds

b_{1} = b_{2}
end;

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 for x being set holds

( x in it iff ex n being Element of NAT st x = prop n );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem defines props LTLAXIO1:def 10 :

for b_{1} being Subset of LTLB_WFF holds

( b_{1} = props iff for x being set holds

( x in b_{1} iff ex n being Element of NAT st x = prop n ) );

for b

( b

( x in b

definition

let M be LTLModel;

ex b_{1} being Function of [:NAT,LTLB_WFF:],BOOLEAN st

for n being Element of NAT holds

( b_{1} . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( b_{1} . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( b_{1} . [n,(p => q)] = (b_{1} . [n,p]) => (b_{1} . [n,q]) & ( b_{1} . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & b_{1} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{1} . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & b_{1} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{1} . [(n + j),p] = 1 ) ) implies b_{1} . [n,(p 'U' q)] = 1 ) ) ) )

for b_{1}, b_{2} being Function of [:NAT,LTLB_WFF:],BOOLEAN st ( for n being Element of NAT holds

( b_{1} . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( b_{1} . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( b_{1} . [n,(p => q)] = (b_{1} . [n,p]) => (b_{1} . [n,q]) & ( b_{1} . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & b_{1} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{1} . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & b_{1} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{1} . [(n + j),p] = 1 ) ) implies b_{1} . [n,(p 'U' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds

( b_{2} . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( b_{2} . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( b_{2} . [n,(p => q)] = (b_{2} . [n,p]) => (b_{2} . [n,q]) & ( b_{2} . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & b_{2} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{2} . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & b_{2} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{2} . [(n + j),p] = 1 ) ) implies b_{2} . [n,(p 'U' q)] = 1 ) ) ) ) ) holds

b_{1} = b_{2}

end;
func SAT M -> Function of [:NAT,LTLB_WFF:],BOOLEAN means :Def11: :: 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 'U' 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 'U' q)] = 1 ) ) ) );

existence 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 'U' 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 'U' q)] = 1 ) ) ) );

ex b

for n being Element of NAT holds

( b

( b

( b

( 0 < i & b

b

( 0 < i & b

b

proof end;

uniqueness for b

( b

( b

( b

( 0 < i & b

b

( 0 < i & b

b

( b

( b

( b

( 0 < i & b

b

( 0 < i & b

b

b

proof end;

:: deftheorem Def11 defines SAT LTLAXIO1:def 11 :

for M being LTLModel

for b_{2} being Function of [:NAT,LTLB_WFF:],BOOLEAN holds

( b_{2} = SAT M iff for n being Element of NAT holds

( b_{2} . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( b_{2} . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( b_{2} . [n,(p => q)] = (b_{2} . [n,p]) => (b_{2} . [n,q]) & ( b_{2} . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & b_{2} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{2} . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & b_{2} . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

b_{2} . [(n + j),p] = 1 ) ) implies b_{2} . [n,(p 'U' q)] = 1 ) ) ) ) );

for M being LTLModel

for b

( b

( b

( b

( b

( 0 < i & b

b

( 0 < i & b

b

theorem Th5: :: 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 )

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: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 ) )

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 Th8: :: 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 ) )

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 Th9: :: 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]

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]

proof end;

theorem Th10: :: 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 )

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 Th11: :: 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 )

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 Th12: :: 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 'Uw' 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 ) ) )

for n being Element of NAT

for M being LTLModel holds

( (SAT M) . [n,(p 'Uw' 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 ) )

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 Th14: :: 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))]

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 Th15: :: 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

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1

proof end;

theorem Th16: :: 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

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1

proof end;

theorem Th17: :: 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

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 Th18: :: 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

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

proof end;

theorem Th19: :: 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 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C)))))] = 1

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,((B 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C)))))] = 1

proof end;

theorem Th20: :: LTLAXIO1:20

for B, C 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 'U' C)))) => (B 'U' C))] = 1

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'U' C)))) => (B 'U' C))] = 1

proof end;

theorem Th21: :: 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 'U' C) => ('X' ('F' C)))] = 1

for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1

proof end;

:: deftheorem Def12 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 );

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 );

:: deftheorem 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 );

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 );

:: deftheorem 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 );

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 Th22: :: LTLAXIO1:22

for F, G being Subset of LTLB_WFF

for M being LTLModel holds

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

for M being LTLModel holds

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

proof end;

theorem Th24: :: 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

for F being Subset of LTLB_WFF st F |= A & F |= A => B holds

F |= B

proof end;

theorem Th27: :: 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)

for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds

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

proof end;

theorem Th28: :: 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]

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 Th29: :: 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

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 )

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;

ex b_{1} being Function of LTLB_WFF,BOOLEAN st

for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{1} . TFALSUM = 0 & b_{1} . (prop n) = f . (prop n) & b_{1} . (A => B) = (b_{1} . A) => (b_{1} . B) & b_{1} . (A 'U' B) = f . (A 'U' B) )

for b_{1}, b_{2} being Function of LTLB_WFF,BOOLEAN st ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{1} . TFALSUM = 0 & b_{1} . (prop n) = f . (prop n) & b_{1} . (A => B) = (b_{1} . A) => (b_{1} . B) & b_{1} . (A 'U' B) = f . (A 'U' B) ) ) & ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{2} . TFALSUM = 0 & b_{2} . (prop n) = f . (prop n) & b_{2} . (A => B) = (b_{2} . A) => (b_{2} . B) & b_{2} . (A 'U' B) = f . (A 'U' B) ) ) holds

b_{1} = b_{2}

end;
func VAL f -> Function of LTLB_WFF,BOOLEAN means :Def15: :: 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 'U' B) = f . (A 'U' B) );

existence 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 'U' B) = f . (A 'U' B) );

ex b

for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b

proof end;

uniqueness for b

for n being Element of NAT holds

( b

for n being Element of NAT holds

( b

b

proof end;

:: deftheorem Def15 defines VAL LTLAXIO1:def 15 :

for f, b_{2} being Function of LTLB_WFF,BOOLEAN holds

( b_{2} = VAL f iff for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{2} . TFALSUM = 0 & b_{2} . (prop n) = f . (prop n) & b_{2} . (A => B) = (b_{2} . A) => (b_{2} . B) & b_{2} . (A 'U' B) = f . (A 'U' B) ) );

for f, b

( b

for n being Element of NAT holds

( b

theorem Th31: :: 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)

for p, q being Element of LTLB_WFF holds (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)

proof end;

theorem Th32: :: 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 object st B in LTLB_WFF holds

f . B = (SAT M) . [n,B] ) holds

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

for n being Element of NAT

for M being LTLModel

for f being Function of LTLB_WFF,BOOLEAN st ( for B being object 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 ;

end;
attr p is LTL_TAUT_OF_PL means :: LTLAXIO1:def 16

for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1;

for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1;

:: deftheorem 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 );

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 );

definition

let D be set ;

end;
attr D is with_LTL_axioms means :Def17: :: 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 '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 );

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 '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 );

:: deftheorem Def17 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 '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 ) );

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 '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 ) );

definition

ex b_{1} being Subset of LTLB_WFF st

( b_{1} is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

b_{1} c= D ) )

for b_{1}, b_{2} being Subset of LTLB_WFF st b_{1} is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

b_{1} c= D ) & b_{2} is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

b_{2} c= D ) holds

b_{1} = b_{2}
end;

func LTL_axioms -> Subset of LTLB_WFF means :Def18: :: 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 ( it is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines LTL_axioms LTLAXIO1:def 18 :

for b_{1} being Subset of LTLB_WFF holds

( b_{1} = LTL_axioms iff ( b_{1} is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

b_{1} c= D ) ) );

for b

( b

b

registration
end;

:: deftheorem defines NEX_rule LTLAXIO1:def 19 :

for p, q being Element of LTLB_WFF holds

( p NEX_rule q iff q = 'X' p );

for p, q being Element of LTLB_WFF holds

( p NEX_rule q iff q = 'X' p );

:: deftheorem 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 );

for p, q, r being Element of LTLB_WFF holds

( p,q MP_rule r iff q = p => r );

:: deftheorem 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) ) );

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) ) );

definition

let A be Element of LTLB_WFF ;

end;
attr A is axltl1 means :Def22: :: LTLAXIO1:def 22

ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B));

ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B));

attr A is axltl1a means :Def23: :: LTLAXIO1:def 23

ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B));

ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B));

attr A is axltl2 means :Def24: :: LTLAXIO1:def 24

ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C));

ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C));

attr A is axltl3 means :Def25: :: LTLAXIO1:def 25

ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B)));

ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B)));

attr A is axltl4 means :Def26: :: LTLAXIO1:def 26

ex B, C being Element of LTLB_WFF st A = (B 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C))));

ex B, C being Element of LTLB_WFF st A = (B 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C))));

:: deftheorem Def22 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)) );

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 Def23 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)) );

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 Def24 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)) );

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 Def25 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))) );

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 Def26 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 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C)))) );

for A being Element of LTLB_WFF holds

( A is axltl4 iff ex B, C being Element of LTLB_WFF st A = (B 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C)))) );

:: deftheorem Def27 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 'U' C)))) => (B 'U' C) );

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 'U' C)))) => (B 'U' C) );

:: deftheorem Def28 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 'U' C) => ('X' ('F' C)) );

for A being Element of LTLB_WFF holds

( A is axltl6 iff ex B, C being Element of LTLB_WFF st A = (B 'U' C) => ('X' ('F' C)) );

theorem Th36: :: 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 )

( 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 Th37: :: 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

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;

:: deftheorem Def29 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 ) ) );

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 ) ) );

:: deftheorem 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 ) ) );

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 Th38: :: 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

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 Th39: :: LTLAXIO1:39

for X being Subset of LTLB_WFF

for f, f1, f2 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

for f, f1, f2 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 Th40: :: 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 )

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 Th42: :: 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

for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds

X |- p

proof end;

theorem Th43: :: 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

for X being Subset of LTLB_WFF st X |- p & X |- p => q holds

X |- q

proof end;

theorem Th45: :: 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)

for X being Subset of LTLB_WFF st X |- p => q & X |- p => ('X' p) holds

X |- p => ('G' q)

proof end;

theorem Th46: :: LTLAXIO1:46

for p, q, r being Element of LTLB_WFF

for X being Subset of LTLB_WFF st X |- r => (p '&&' q) holds

( X |- r => p & X |- r => q )

for X being Subset of LTLB_WFF st X |- r => (p '&&' q) holds

( X |- r => p & X |- r => q )

proof end;

theorem Th47: :: 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

for X being Subset of LTLB_WFF st X |- p => q & X |- q => r holds

X |- p => r

proof end;

theorem Th48: :: 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

for X being Subset of LTLB_WFF st X |- p => (q => r) holds

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

proof end;

theorem Th49: :: 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)

for X being Subset of LTLB_WFF st X |- (p '&&' q) => r holds

X |- p => (q => r)

proof end;

theorem Th50: :: 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)

for X being Subset of LTLB_WFF st X |- (p '&&' q) => r & X |- p => s holds

X |- (p '&&' q) => (s '&&' r)

proof end;

theorem Th51: :: 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)

for X being Subset of LTLB_WFF st X |- p => (q => r) & X |- r => s holds

X |- p => (q => s)

proof end;

theorem Th52: :: 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)

for X being Subset of LTLB_WFF st X |- p => q holds

X |- ('not' q) => ('not' p)

proof end;

theorem Th53: :: 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))

for X being Subset of LTLB_WFF holds X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))

proof end;

theorem Th55: :: 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

for F being Subset of LTLB_WFF st p => q in F holds

F \/ {p} |- 'G' q

proof end;

theorem Th57: :: 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

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

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

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))

for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q))

proof end;