:: by Mariusz Giero

::

:: Received May 7, 2012

:: Copyright (c) 2012-2019 Association of Mizar Users

set l = LTLB_WFF ;

Lm1: for f being FinSequence holds f . 0 = 0

proof end;

registration
end;

definition
end;

:: deftheorem defines untn LTLAXIO2:def 1 :

for A, B being Element of LTLB_WFF holds untn (A,B) = B 'or' (A '&&' (A 'U' B));

for A, B being Element of LTLB_WFF holds untn (A,B) = B 'or' (A '&&' (A 'U' B));

set tf = TFALSUM ;

theorem Th5: :: LTLAXIO2:5

for p, q being Element of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . (p 'or' q) = ((VAL g) . p) 'or' ((VAL g) . q)

for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . (p 'or' q) = ((VAL g) . p) 'or' ((VAL g) . q)

proof end;

definition

let f be FinSequence of LTLB_WFF ;

( ( len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st

( len b_{1} = len f & b_{1} . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . (i + 1) = (b_{1} /. i) '&&' (f /. (i + 1)) ) ) ) & ( not len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st b_{1} = <*TVERUM*> ) )

for b_{1}, b_{2} being FinSequence of LTLB_WFF holds

( ( len f > 0 & len b_{1} = len f & b_{1} . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . (i + 1) = (b_{1} /. i) '&&' (f /. (i + 1)) ) & len b_{2} = len f & b_{2} . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{2} . (i + 1) = (b_{2} /. i) '&&' (f /. (i + 1)) ) implies b_{1} = b_{2} ) & ( not len f > 0 & b_{1} = <*TVERUM*> & b_{2} = <*TVERUM*> implies b_{1} = b_{2} ) )

for b_{1} being FinSequence of LTLB_WFF holds verum
;

end;
func con f -> FinSequence of LTLB_WFF means :Def2: :: LTLAXIO2:def 2

( len it = len f & it . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds

it . (i + 1) = (it /. i) '&&' (f /. (i + 1)) ) ) if len f > 0

otherwise it = <*TVERUM*>;

existence ( len it = len f & it . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds

it . (i + 1) = (it /. i) '&&' (f /. (i + 1)) ) ) if len f > 0

otherwise it = <*TVERUM*>;

( ( len f > 0 implies ex b

( len b

b

proof end;

uniqueness for b

( ( len f > 0 & len b

b

b

proof end;

consistency for b

:: deftheorem Def2 defines con LTLAXIO2:def 2 :

for f, b_{2} being FinSequence of LTLB_WFF holds

( ( len f > 0 implies ( b_{2} = con f iff ( len b_{2} = len f & b_{2} . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{2} . (i + 1) = (b_{2} /. i) '&&' (f /. (i + 1)) ) ) ) ) & ( not len f > 0 implies ( b_{2} = con f iff b_{2} = <*TVERUM*> ) ) );

for f, b

( ( len f > 0 implies ( b

b

definition

let f be FinSequence of LTLB_WFF ;

let A be Element of LTLB_WFF ;

( ( len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st

( len b_{1} = len f & b_{1} . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{1} . (i + 1) = ('G' (f /. (i + 1))) => (b_{1} /. i) ) ) ) & ( not len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st b_{1} = <*> LTLB_WFF ) )

for b_{1}, b_{2} being FinSequence of LTLB_WFF holds

( ( len f > 0 & len b_{1} = len f & b_{1} . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{1} . (i + 1) = ('G' (f /. (i + 1))) => (b_{1} /. i) ) & len b_{2} = len f & b_{2} . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{2} . (i + 1) = ('G' (f /. (i + 1))) => (b_{2} /. i) ) implies b_{1} = b_{2} ) & ( not len f > 0 & b_{1} = <*> LTLB_WFF & b_{2} = <*> LTLB_WFF implies b_{1} = b_{2} ) )

for b_{1} being FinSequence of LTLB_WFF holds verum
;

end;
let A be Element of LTLB_WFF ;

func impg (f,A) -> FinSequence of LTLB_WFF means :: LTLAXIO2:def 3

( len it = len f & it . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

it . (i + 1) = ('G' (f /. (i + 1))) => (it /. i) ) ) if len f > 0

otherwise it = <*> LTLB_WFF;

existence ( len it = len f & it . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

it . (i + 1) = ('G' (f /. (i + 1))) => (it /. i) ) ) if len f > 0

otherwise it = <*> LTLB_WFF;

( ( len f > 0 implies ex b

( len b

b

proof end;

uniqueness for b

( ( len f > 0 & len b

b

b

proof end;

consistency for b

:: deftheorem defines impg LTLAXIO2:def 3 :

for f being FinSequence of LTLB_WFF

for A being Element of LTLB_WFF

for b_{3} being FinSequence of LTLB_WFF holds

( ( len f > 0 implies ( b_{3} = impg (f,A) iff ( len b_{3} = len f & b_{3} . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{3} . (i + 1) = ('G' (f /. (i + 1))) => (b_{3} /. i) ) ) ) ) & ( not len f > 0 implies ( b_{3} = impg (f,A) iff b_{3} = <*> LTLB_WFF ) ) );

for f being FinSequence of LTLB_WFF

for A being Element of LTLB_WFF

for b

( ( len f > 0 implies ( b

b

definition

let f be FinSequence of LTLB_WFF ;

ex b_{1} being FinSequence of LTLB_WFF st

( len b_{1} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{1} . i = 'not' (f /. i) ) )

for b_{1}, b_{2} being FinSequence of LTLB_WFF st len b_{1} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{1} . i = 'not' (f /. i) ) & len b_{2} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{2} . i = 'not' (f /. i) ) holds

b_{1} = b_{2}

end;
func nega f -> FinSequence of LTLB_WFF means :Def4: :: LTLAXIO2:def 4

( len it = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

it . i = 'not' (f /. i) ) );

existence ( len it = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

it . i = 'not' (f /. i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines nega LTLAXIO2:def 4 :

for f, b_{2} being FinSequence of LTLB_WFF holds

( b_{2} = nega f iff ( len b_{2} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{2} . i = 'not' (f /. i) ) ) );

for f, b

( b

b

deffunc H

deffunc H

definition

let f be FinSequence of LTLB_WFF ;

ex b_{1} being FinSequence of LTLB_WFF st

( len b_{1} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{1} . i = 'X' (f /. i) ) )

for b_{1}, b_{2} being FinSequence of LTLB_WFF st len b_{1} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{1} . i = 'X' (f /. i) ) & len b_{2} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{2} . i = 'X' (f /. i) ) holds

b_{1} = b_{2}

end;
func nex f -> FinSequence of LTLB_WFF means :Def5: :: LTLAXIO2:def 5

( len it = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

it . i = 'X' (f /. i) ) );

existence ( len it = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

it . i = 'X' (f /. i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines nex LTLAXIO2:def 5 :

for f, b_{2} being FinSequence of LTLB_WFF holds

( b_{2} = nex f iff ( len b_{2} = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds

b_{2} . i = 'X' (f /. i) ) ) );

for f, b

( b

b

theorem Th7: :: LTLAXIO2:7

for f being FinSequence of LTLB_WFF

for i being Nat st 1 <= i & i < len f holds

(con f) /. (i + 1) = ((con f) /. i) '&&' (f /. (i + 1))

for i being Nat st 1 <= i & i < len f holds

(con f) /. (i + 1) = ((con f) /. i) '&&' (f /. (i + 1))

proof end;

theorem Th8: :: LTLAXIO2:8

for f being FinSequence of LTLB_WFF

for i being Nat st i in dom f holds

(nega f) /. i = 'not' (f /. i)

for i being Nat st i in dom f holds

(nega f) /. i = 'not' (f /. i)

proof end;

theorem Th12: :: LTLAXIO2:12

for f being FinSequence of LTLB_WFF

for k, n being Nat st n <= k holds

(con f) . n = (con (f | k)) . n

for k, n being Nat st n <= k holds

(con f) . n = (con (f | k)) . n

proof end;

theorem Th13: :: LTLAXIO2:13

for f being FinSequence of LTLB_WFF

for k, n being Nat st n <= k & 1 <= n & n <= len f holds

(con f) /. n = (con (f | k)) /. n

for k, n being Nat st n <= k & 1 <= n & n <= len f holds

(con f) /. n = (con (f | k)) /. n

proof end;

theorem :: LTLAXIO2:15

for A being Element of LTLB_WFF

for f being FinSequence of LTLB_WFF holds nega (f ^ <*A*>) = (nega f) ^ <*('not' A)*>

for f being FinSequence of LTLB_WFF holds nega (f ^ <*A*>) = (nega f) ^ <*('not' A)*>

proof end;

theorem Th17: :: LTLAXIO2:17

for f, f1 being FinSequence of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . ((con (f ^ f1)) /. (len (con (f ^ f1)))) = ((VAL g) . ((con f) /. (len (con f)))) '&' ((VAL g) . ((con f1) /. (len (con f1))))

for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . ((con (f ^ f1)) /. (len (con (f ^ f1)))) = ((VAL g) . ((con f) /. (len (con f)))) '&' ((VAL g) . ((con f1) /. (len (con f1))))

proof end;

theorem :: LTLAXIO2:18

for n being Element of NAT

for f being FinSequence of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN st n in dom f holds

(VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n)))))

for f being FinSequence of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN st n in dom f holds

(VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n)))))

proof end;

theorem Th19: :: LTLAXIO2:19

for f being FinSequence of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN holds

( (VAL g) . ((con f) /. (len (con f))) = 1 iff for i being Nat st i in dom f holds

(VAL g) . (f /. i) = 1 )

for g being Function of LTLB_WFF,BOOLEAN holds

( (VAL g) . ((con f) /. (len (con f))) = 1 iff for i being Nat st i in dom f holds

(VAL g) . (f /. i) = 1 )

proof end;

theorem Th20: :: LTLAXIO2:20

for f being FinSequence of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN holds

( (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0 iff for i being Nat st i in dom f holds

(VAL g) . (f /. i) = 0 )

for g being Function of LTLB_WFF,BOOLEAN holds

( (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0 iff for i being Nat st i in dom f holds

(VAL g) . (f /. i) = 0 )

proof end;

theorem :: LTLAXIO2:21

for f, f1 being FinSequence of LTLB_WFF

for g being Function of LTLB_WFF,BOOLEAN st rng f = rng f1 holds

(VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

for g being Function of LTLB_WFF,BOOLEAN st rng f = rng f1 holds

(VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

proof end;

theorem :: LTLAXIO2:29

for f being FinSequence of LTLB_WFF

for k being Nat st k in dom f holds

(f /. k) => ('not' ((con (nega f)) /. (len (con (nega f))))) is ctaut

for k being Nat st k in dom f holds

(f /. k) => ('not' ((con (nega f)) /. (len (con (nega f))))) is ctaut

proof end;

theorem :: LTLAXIO2:30

for f, f1 being FinSequence of LTLB_WFF st rng f c= rng f1 holds

('not' ((con (nega f)) /. (len (con (nega f))))) => ('not' ((con (nega f1)) /. (len (con (nega f1))))) is ctaut

('not' ((con (nega f)) /. (len (con (nega f))))) => ('not' ((con (nega f1)) /. (len (con (nega f1))))) is ctaut

proof end;

theorem :: LTLAXIO2:39

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

proof end;

theorem :: LTLAXIO2:41

for p, q, r, s being Element of LTLB_WFF holds ('not' (p '&&' s)) => ('not' ((r '&&' s) '&&' (p '&&' q))) is ctaut

proof end;

theorem :: LTLAXIO2:42

for p, q, r, s being Element of LTLB_WFF holds ('not' (p '&&' s)) => ('not' ((p '&&' q) '&&' (r '&&' s))) is ctaut

proof end;

theorem Th44: :: LTLAXIO2:44

for p, q, r, s being Element of LTLB_WFF holds (q => (p '&&' r)) => ((p => s) => (q => (s '&&' r))) is ctaut

proof end;

theorem Th45: :: LTLAXIO2:45

for p, q, r, s being Element of LTLB_WFF holds (p => q) => ((r => s) => ((p '&&' r) => (q '&&' s))) is ctaut

proof end;

theorem Th46: :: LTLAXIO2:46

for p, q, r being Element of LTLB_WFF holds (p => q) => ((p => r) => ((r => p) => (r => q))) is ctaut

proof end;

theorem Th47: :: LTLAXIO2:47

for p, q, r being Element of LTLB_WFF holds (p => q) => ((p => ('not' r)) => (p => ('not' (q => r)))) is ctaut

proof end;

theorem Th48: :: LTLAXIO2:48

for p, q, r, s being Element of LTLB_WFF holds (p => (q 'or' r)) => ((r => s) => (p => (q 'or' s))) is ctaut

proof end;

theorem :: LTLAXIO2:50

for p, q, r being Element of LTLB_WFF holds (r => (untn (p,q))) => ((r => (('not' p) '&&' ('not' q))) => ('not' r)) is ctaut

proof end;

theorem :: LTLAXIO2:51

for p, q, r being Element of LTLB_WFF holds (r => (untn (p,q))) => ((r => (('not' q) '&&' ('not' (p 'U' q)))) => ('not' r)) is ctaut

proof end;

theorem :: LTLAXIO2:52

for p, q, r being Element of LTLB_WFF

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

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

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

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

proof end;

theorem Th53: :: LTLAXIO2:53

for p, q, r, s being Element of LTLB_WFF

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

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

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

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

proof end;

theorem Th54: :: LTLAXIO2:54

for p, q, r being Element of LTLB_WFF

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

X |- r => q

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

X |- r => q

proof end;

theorem :: LTLAXIO2:55

for p, q being Element of LTLB_WFF

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

X |- 'not' p

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

X |- 'not' p

proof end;

theorem :: LTLAXIO2:56

for p being Element of LTLB_WFF

for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds

{} LTLB_WFF |- p => (f /. i) ) holds

{} LTLB_WFF |- p => ((con f) /. (len (con f)))

for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds

{} LTLB_WFF |- p => (f /. i) ) holds

{} LTLB_WFF |- p => ((con f) /. (len (con f)))

proof end;

theorem :: LTLAXIO2:57

for p being Element of LTLB_WFF

for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds

{} LTLB_WFF |- (f /. i) => p ) holds

{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p

for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds

{} LTLB_WFF |- (f /. i) => p ) holds

{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => p

proof end;

theorem Th58: :: LTLAXIO2:58

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 Th59: :: LTLAXIO2:59

for p, q being Element of LTLB_WFF

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

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

proof end;

theorem :: LTLAXIO2:60

for f being FinSequence of LTLB_WFF holds {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f))))

proof end;

theorem :: LTLAXIO2:61

for p, q being Element of LTLB_WFF

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

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

proof end;

theorem Th62: :: LTLAXIO2:62

for p, q being Element of LTLB_WFF

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

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

proof end;

theorem :: LTLAXIO2:63

for A, B being Element of LTLB_WFF

for X being Subset of LTLB_WFF holds X |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B))))

for X being Subset of LTLB_WFF holds X |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B))))

proof end;