:: The Derivations of Temporal Logic Formulas
:: by Mariusz Giero
::
:: Received May 7, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

set l = LTLB_WFF ;

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

proof end;

registration

let f be FinSequence;
let x be empty set ;

cluster f . x -> empty ;

coherence
f . x is empty by Lm1;

end;

theorem Th1: :: LTLAXIO2:1

for n being Element of NAT
for f being FinSequence st len f > 0 & n > 0 holds
len (f | n) > 0

proof end;

theorem Th2: :: LTLAXIO2:2

for n being Element of NAT
for f being FinSequence st len f = 0 holds
f /^ n = f

proof end;

theorem Th3: :: LTLAXIO2:3

for f, g being FinSequence st rng f = rng g holds
( len f = 0 iff len g = 0 )

proof end;

definition

let A, B be Element of LTLB_WFF ;

func untn (A,B) -> Element of LTLB_WFF equals :: LTLAXIO2:def 1
B 'or' (A '&&' (A 'U' B));

coherence
B 'or' (A '&&' (A 'U' B)) is Element of LTLB_WFF ;

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

theorem Th4: :: LTLAXIO2:4

for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . TVERUM = 1

proof end;

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)

proof end;

notation

let p be Element of LTLB_WFF ;
synonym ctaut p for LTL_TAUT_OF_PL ;

end;

definition

let f be FinSequence of LTLB_WFF ;

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 f > 0 implies ex b₁ being FinSequence of LTLB_WFF st
( len b₁ = len f & b₁ . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) '&&' (f /. (i + 1)) ) ) ) & ( not len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st b₁ = <*TVERUM*> ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of LTLB_WFF holds
( ( len f > 0 & len b₁ = len f & b₁ . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) '&&' (f /. (i + 1)) ) & len b₂ = len f & b₂ . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₂ . (i + 1) = (b₂ /. i) '&&' (f /. (i + 1)) ) implies b₁ = b₂ ) & ( not len f > 0 & b₁ = <*TVERUM*> & b₂ = <*TVERUM*> implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being FinSequence of LTLB_WFF holds verum ;

end;

:: deftheorem Def2 defines con LTLAXIO2:def 2 :
for f, b₂ being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b₂ = con f iff ( len b₂ = len f & b₂ . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₂ . (i + 1) = (b₂ /. i) '&&' (f /. (i + 1)) ) ) ) ) & ( not len f > 0 implies ( b₂ = con f iff b₂ = <*TVERUM*> ) ) );

definition

let f be FinSequence of LTLB_WFF ;
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 f > 0 implies ex b₁ being FinSequence of LTLB_WFF st
( len b₁ = len f & b₁ . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₁ . (i + 1) = ('G' (f /. (i + 1))) => (b₁ /. i) ) ) ) & ( not len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st b₁ = <*> LTLB_WFF ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of LTLB_WFF holds
( ( len f > 0 & len b₁ = len f & b₁ . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₁ . (i + 1) = ('G' (f /. (i + 1))) => (b₁ /. i) ) & len b₂ = len f & b₂ . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₂ . (i + 1) = ('G' (f /. (i + 1))) => (b₂ /. i) ) implies b₁ = b₂ ) & ( not len f > 0 & b₁ = <*> LTLB_WFF & b₂ = <*> LTLB_WFF implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being FinSequence of LTLB_WFF holds verum ;

end;

:: deftheorem defines impg LTLAXIO2:def 3 :
for f being FinSequence of LTLB_WFF
for A being Element of LTLB_WFF
for b₃ being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b₃ = impg (f,A) iff ( len b₃ = len f & b₃ . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₃ . (i + 1) = ('G' (f /. (i + 1))) => (b₃ /. i) ) ) ) ) & ( not len f > 0 implies ( b₃ = impg (f,A) iff b₃ = <*> LTLB_WFF ) ) );

definition

let f be FinSequence of LTLB_WFF ;

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
ex b₁ being FinSequence of LTLB_WFF st
( len b₁ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₁ . i = 'not' (f /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of LTLB_WFF st len b₁ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₁ . i = 'not' (f /. i) ) & len b₂ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₂ . i = 'not' (f /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines nega LTLAXIO2:def 4 :
for f, b₂ being FinSequence of LTLB_WFF holds
( b₂ = nega f iff ( len b₂ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₂ . i = 'not' (f /. i) ) ) );

deffunc H₁( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = 'not' ((con (nega $1)) /. (len (con (nega $1))));

deffunc H₂( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = (con $1) /. (len (con $1));

definition

let f be FinSequence of LTLB_WFF ;

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
ex b₁ being FinSequence of LTLB_WFF st
( len b₁ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₁ . i = 'X' (f /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of LTLB_WFF st len b₁ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₁ . i = 'X' (f /. i) ) & len b₂ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₂ . i = 'X' (f /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines nex LTLAXIO2:def 5 :
for f, b₂ being FinSequence of LTLB_WFF holds
( b₂ = nex f iff ( len b₂ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₂ . i = 'X' (f /. i) ) ) );

theorem Th6: :: LTLAXIO2:6

for f being FinSequence of LTLB_WFF st len f > 0 holds
(con f) /. 1 = f /. 1

proof end;

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

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)

proof end;

theorem :: LTLAXIO2:9

for f being FinSequence of LTLB_WFF
for i being Nat st i in dom f holds
(nex f) /. i = 'X' (f /. i)

proof end;

theorem Th10: :: LTLAXIO2:10

(con (<*> LTLB_WFF)) /. (len (con (<*> LTLB_WFF))) = TVERUM

proof end;

theorem Th11: :: LTLAXIO2:11

for A being Element of LTLB_WFF holds (con <*A*>) /. (len (con <*A*>)) = A

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

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

proof end;

theorem :: LTLAXIO2:14

for A being Element of LTLB_WFF holds nega <*A*> = <*('not' A)*>

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

proof end;

theorem :: LTLAXIO2:16

for f, f1 being FinSequence of LTLB_WFF holds nega (f ^ f1) = (nega f) ^ (nega f1)

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

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

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 )

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 )

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

proof end;

theorem Th22: :: LTLAXIO2:22

for p being Element of LTLB_WFF holds p => TVERUM is ctaut

proof end;

theorem Th23: :: LTLAXIO2:23

for p being Element of LTLB_WFF holds ('not' TVERUM) => p is ctaut

proof end;

theorem Th24: :: LTLAXIO2:24

for p being Element of LTLB_WFF holds p => p is ctaut

proof end;

theorem Th25: :: LTLAXIO2:25

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

proof end;

theorem Th26: :: LTLAXIO2:26

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

proof end;

theorem :: LTLAXIO2:27

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

proof end;

theorem :: LTLAXIO2:28

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

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

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

proof end;

theorem Th31: :: LTLAXIO2:31

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

proof end;

theorem Th32: :: LTLAXIO2:32

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

proof end;

theorem :: LTLAXIO2:33

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

proof end;

theorem Th34: :: LTLAXIO2:34

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

proof end;

theorem Th35: :: LTLAXIO2:35

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

proof end;

theorem :: LTLAXIO2:36

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

proof end;

theorem :: LTLAXIO2:37

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

proof end;

theorem :: LTLAXIO2:38

for A being Element of LTLB_WFF holds ('not' (TVERUM '&&' ('not' A))) => A 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 Th40: :: LTLAXIO2:40

for p, r, s being Element of LTLB_WFF holds (p => r) => ((p => s) => (p => (r '&&' 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 Th43: :: LTLAXIO2:43

for p, q being Element of LTLB_WFF holds (p => (q '&&' ('not' q))) => ('not' p) 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 Th49: :: LTLAXIO2:49

for p, q, r being Element of LTLB_WFF holds (p => r) => ((q => r) => ((p 'or' q) => r)) 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)

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)

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

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

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

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

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

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

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

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

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

proof end;