:: The Derivations of Temporal Logic Formulas
:: by Mariusz Giero
::
:: 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 = ;
existence
( ( len f > 0 implies ex b1 being FinSequence of LTLB_WFF st
( len b1 = len f & b1 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b1 . (i + 1) = (b1 /. i) '&&' (f /. (i + 1)) ) ) ) & ( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = ) )
proof end;
uniqueness
for b1, b2 being FinSequence of LTLB_WFF holds
( ( len f > 0 & len b1 = len f & b1 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b1 . (i + 1) = (b1 /. i) '&&' (f /. (i + 1)) ) & len b2 = len f & b2 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b2 . (i + 1) = (b2 /. i) '&&' (f /. (i + 1)) ) implies b1 = b2 ) & ( not len f > 0 & b1 = & b2 = implies b1 = b2 ) )
proof end;
consistency
for b1 being FinSequence of LTLB_WFF holds verum
;
end;

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

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 b1 being FinSequence of LTLB_WFF st
( len b1 = len f & b1 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b1 . (i + 1) = ('G' (f /. (i + 1))) => (b1 /. i) ) ) ) & ( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = <*> LTLB_WFF ) )
proof end;
uniqueness
for b1, b2 being FinSequence of LTLB_WFF holds
( ( len f > 0 & len b1 = len f & b1 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b1 . (i + 1) = ('G' (f /. (i + 1))) => (b1 /. i) ) & len b2 = len f & b2 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b2 . (i + 1) = ('G' (f /. (i + 1))) => (b2 /. i) ) implies b1 = b2 ) & ( not len f > 0 & b1 = <*> LTLB_WFF & b2 = <*> LTLB_WFF implies b1 = b2 ) )
proof end;
consistency
for b1 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 b3 being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b3 = impg (f,A) iff ( len b3 = len f & b3 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b3 . (i + 1) = ('G' (f /. (i + 1))) => (b3 /. i) ) ) ) ) & ( not len f > 0 implies ( b3 = impg (f,A) iff b3 = <*> 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 b1 being FinSequence of LTLB_WFF st
( len b1 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b1 . i = 'not' (f /. i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of LTLB_WFF st len b1 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b1 . i = 'not' (f /. i) ) & len b2 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b2 . i = 'not' (f /. i) ) holds
b1 = b2
proof end;
end;

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

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

deffunc H2( 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 b1 being FinSequence of LTLB_WFF st
( len b1 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b1 . i = 'X' (f /. i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of LTLB_WFF st len b1 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b1 . i = 'X' (f /. i) ) & len b2 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b2 . i = 'X' (f /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines nex LTLAXIO2:def 5 :
for f, b2 being FinSequence of LTLB_WFF holds
( b2 = nex f iff ( len b2 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b2 . 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
() /. (len ()) = TVERUM
proof end;

theorem Th11: :: LTLAXIO2:11
for A being Element of LTLB_WFF holds () /. (len ()) = 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*> = <*()*>
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) ^ <*()*>
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 () => 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' ()) => p is ctaut
proof end;

theorem Th26: :: LTLAXIO2:26
for p being Element of LTLB_WFF holds p => ('not' ()) 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)) => () 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)) => (() 'or' ()) is ctaut
proof end;

theorem :: LTLAXIO2:36
for p, q being Element of LTLB_WFF holds ('not' (p 'or' q)) => (() '&&' ()) is ctaut
proof end;

theorem :: LTLAXIO2:37
for p, q being Element of LTLB_WFF holds ('not' (p '&&' q)) => (p => ()) is ctaut
proof end;

theorem :: LTLAXIO2:38
for A being Element of LTLB_WFF holds ('not' (TVERUM '&&' ())) => A is ctaut
proof end;

theorem :: LTLAXIO2:39
for p, q, s being Element of LTLB_WFF holds ('not' (s '&&' q)) => ((p => q) => (p => ())) 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 '&&' ())) => () 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 => ()) => (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 => (() '&&' ())) => ()) is ctaut
proof end;

theorem :: LTLAXIO2:51
for p, q, r being Element of LTLB_WFF holds (r => (untn (p,q))) => ((r => (() '&&' ('not' (p 'U' q)))) => ()) 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 '&&' ()) 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;