:: The Properties of Sets of Temporal Logic Subformulas
:: by Mariusz Giero
::
:: Received May 7, 2012
:: Copyright (c) 2012 Association of Mizar Users


begin

set l = LTLB_WFF ;

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

theorem Th1: :: LTLAXIO3:1
for X being non empty set
for t being FinSequence of X
for k being Nat st k + 1 <= len t holds
t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1))
proof end;

theorem Th2: :: LTLAXIO3:2
NAT --> {} is LTLModel
proof end;

definition
let X be Subset of LTLB_WFF;
attr X is without_implication means :Def1: :: LTLAXIO3:def 1
for p being Element of LTLB_WFF st p in X holds
not p is conditional ;
end;

:: deftheorem Def1 defines without_implication LTLAXIO3:def 1 :
for X being Subset of LTLB_WFF holds
( X is without_implication iff for p being Element of LTLB_WFF st p in X holds
not p is conditional );

definition
let D be set ;
func D ** -> set means :Def2: :: LTLAXIO3:def 2
for x being set holds
( x in it iff x is one-to-one FinSequence of D );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is one-to-one FinSequence of D )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is one-to-one FinSequence of D ) ) & ( for x being set holds
( x in b2 iff x is one-to-one FinSequence of D ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ** LTLAXIO3:def 2 :
for D, b2 being set holds
( b2 = D ** iff for x being set holds
( x in b2 iff x is one-to-one FinSequence of D ) );

registration
let D be set ;
cluster D ** -> non empty ;
coherence
not D ** is empty
proof end;
end;

registration
let D be finite set ;
cluster D ** -> finite ;
coherence
D ** is finite
proof end;
end;

theorem Th3: :: LTLAXIO3:3
for D1, D2 being set st D1 c= D2 holds
D1 ** c= D2 **
proof end;

definition
let a1 be set ;
let a2 be Subset of a1;
:: original: **
redefine func a2 ** -> non empty Subset of (a1 **);
coherence
a2 ** is non empty Subset of (a1 **)
by Th3;
end;

theorem Th4: :: LTLAXIO3:4
for F, G being one-to-one FinSequence st rng F misses rng G holds
F ^ G is one-to-one
proof end;

definition
let X be set ;
let f, g be one-to-one FinSequence of X;
assume A1: rng f misses rng g ;
func f ^^ g -> one-to-one FinSequence of X equals :Def3: :: LTLAXIO3:def 3
f ^ g;
coherence
f ^ g is one-to-one FinSequence of X
by Th4, A1;
end;

:: deftheorem Def3 defines ^^ LTLAXIO3:def 3 :
for X being set
for f, g being one-to-one FinSequence of X st rng f misses rng g holds
f ^^ g = f ^ g;

begin

definition
func tau1 -> Function of LTLB_WFF,(bool LTLB_WFF) means :Def4: :: LTLAXIO3:def 4
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( it . TFALSUM = {TFALSUM} & it . (prop n) = {(prop n)} & it . (A => B) = ({(A => B)} \/ (it . A)) \/ (it . B) & it . (A 'Us' B) = {(A 'Us' B)} );
existence
ex b1 being Function of LTLB_WFF,(bool LTLB_WFF) st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = {TFALSUM} & b1 . (prop n) = {(prop n)} & b1 . (A => B) = ({(A => B)} \/ (b1 . A)) \/ (b1 . B) & b1 . (A 'Us' B) = {(A 'Us' B)} )
proof end;
uniqueness
for b1, b2 being Function of LTLB_WFF,(bool LTLB_WFF) st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = {TFALSUM} & b1 . (prop n) = {(prop n)} & b1 . (A => B) = ({(A => B)} \/ (b1 . A)) \/ (b1 . B) & b1 . (A 'Us' B) = {(A 'Us' B)} ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b2 . TFALSUM = {TFALSUM} & b2 . (prop n) = {(prop n)} & b2 . (A => B) = ({(A => B)} \/ (b2 . A)) \/ (b2 . B) & b2 . (A 'Us' B) = {(A 'Us' B)} ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines tau1 LTLAXIO3:def 4 :
for b1 being Function of LTLB_WFF,(bool LTLB_WFF) holds
( b1 = tau1 iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = {TFALSUM} & b1 . (prop n) = {(prop n)} & b1 . (A => B) = ({(A => B)} \/ (b1 . A)) \/ (b1 . B) & b1 . (A 'Us' B) = {(A 'Us' B)} ) );

theorem Th5: :: LTLAXIO3:5
for A being Element of LTLB_WFF st not A is conditional holds
tau1 . A = {A}
proof end;

theorem Th6: :: LTLAXIO3:6
for p being Element of LTLB_WFF holds p in tau1 . p
proof end;

registration
let p be Element of LTLB_WFF ;
cluster tau1 . p -> non empty finite ;
coherence
( not tau1 . p is empty & tau1 . p is finite )
proof end;
end;

theorem Th7: :: LTLAXIO3:7
for p, q, r being Element of LTLB_WFF st p => q in tau1 . r holds
( p in tau1 . r & q in tau1 . r )
proof end;

theorem Th8: :: LTLAXIO3:8
for p, q being Element of LTLB_WFF st p in tau1 . q holds
tau1 . p c= tau1 . q
proof end;

theorem Th9: :: LTLAXIO3:9
for A, p, q being Element of LTLB_WFF st p 'Us' q in tau1 . ('not' A) holds
p 'Us' q in tau1 . A
proof end;

theorem Th10: :: LTLAXIO3:10
for A, B, p, q being Element of LTLB_WFF holds
( not p 'Us' q in tau1 . (A '&&' B) or p 'Us' q in tau1 . A or p 'Us' q in tau1 . B )
proof end;

theorem :: LTLAXIO3:11
for p, q being Element of LTLB_WFF st p in tau1 . q & p <> q holds
len p < len q
proof end;

theorem Th12: :: LTLAXIO3:12
for p being Element of LTLB_WFF holds tau1 . p c= tau1 . ('not' p)
proof end;

theorem Th13: :: LTLAXIO3:13
for p, q being Element of LTLB_WFF holds tau1 . q c= tau1 . (p '&&' q)
proof end;

theorem Th14: :: LTLAXIO3:14
for p, q being Element of LTLB_WFF holds tau1 . q c= tau1 . (p 'or' q)
proof end;

definition
let X be Subset of LTLB_WFF;
func tau X -> Subset of LTLB_WFF means :Def5: :: LTLAXIO3:def 5
for x being set holds
( x in it iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) );
existence
ex b1 being Subset of LTLB_WFF st
for x being set holds
( x in b1 iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) )
proof end;
uniqueness
for b1, b2 being Subset of LTLB_WFF st ( for x being set holds
( x in b1 iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) ) & ( for x being set holds
( x in b2 iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines tau LTLAXIO3:def 5 :
for X, b2 being Subset of LTLB_WFF holds
( b2 = tau X iff for x being set holds
( x in b2 iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) );

theorem Th15: :: LTLAXIO3:15
for X being Subset of LTLB_WFF holds tau X = union { (tau1 . p) where p is Element of LTLB_WFF : p in X }
proof end;

theorem Th16: :: LTLAXIO3:16
for X being Subset of LTLB_WFF holds X c= tau X
proof end;

registration
let X be empty Subset of LTLB_WFF;
cluster tau X -> empty ;
coherence
tau X is empty
proof end;
end;

registration
let X be finite Subset of LTLB_WFF;
cluster tau X -> finite ;
coherence
tau X is finite
proof end;
end;

registration
let X be non empty Subset of LTLB_WFF;
cluster tau X -> non empty ;
coherence
not tau X is empty
proof end;
end;

theorem Th17: :: LTLAXIO3:17
for X being Subset of LTLB_WFF holds tau (tau X) = tau X
proof end;

theorem :: LTLAXIO3:18
for X being Subset of LTLB_WFF st X is without_implication holds
tau X = X
proof end;

theorem Th19: :: LTLAXIO3:19
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st p => q in tau X holds
( p in tau X & q in tau X )
proof end;

theorem Th20: :: LTLAXIO3:20
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st p '&&' q in tau X holds
( p in tau X & q in tau X )
proof end;

theorem Th21: :: LTLAXIO3:21
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st p 'or' q in tau X holds
( p in tau X & q in tau X )
proof end;

theorem :: LTLAXIO3:22
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st untn (p,q) in tau X holds
( p in tau X & q in tau X & p 'Us' q in tau X )
proof end;

theorem :: LTLAXIO3:23
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF st p in tau X holds
tau1 . p c= tau X
proof end;

begin

definition
func Sub -> Function of LTLB_WFF,(bool LTLB_WFF) means :Def6: :: LTLAXIO3:def 6
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( it . TFALSUM = {TFALSUM} & it . (prop n) = {(prop n)} & it . (A => B) = ({(A => B)} \/ (it . A)) \/ (it . B) & it . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (it . A)) \/ (it . B) );
existence
ex b1 being Function of LTLB_WFF,(bool LTLB_WFF) st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = {TFALSUM} & b1 . (prop n) = {(prop n)} & b1 . (A => B) = ({(A => B)} \/ (b1 . A)) \/ (b1 . B) & b1 . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b1 . A)) \/ (b1 . B) )
proof end;
uniqueness
for b1, b2 being Function of LTLB_WFF,(bool LTLB_WFF) st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = {TFALSUM} & b1 . (prop n) = {(prop n)} & b1 . (A => B) = ({(A => B)} \/ (b1 . A)) \/ (b1 . B) & b1 . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b1 . A)) \/ (b1 . B) ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b2 . TFALSUM = {TFALSUM} & b2 . (prop n) = {(prop n)} & b2 . (A => B) = ({(A => B)} \/ (b2 . A)) \/ (b2 . B) & b2 . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b2 . A)) \/ (b2 . B) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Sub LTLAXIO3:def 6 :
for b1 being Function of LTLB_WFF,(bool LTLB_WFF) holds
( b1 = Sub iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = {TFALSUM} & b1 . (prop n) = {(prop n)} & b1 . (A => B) = ({(A => B)} \/ (b1 . A)) \/ (b1 . B) & b1 . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b1 . A)) \/ (b1 . B) ) );

theorem Th24: :: LTLAXIO3:24
for p, q being Element of LTLB_WFF holds p 'Us' q in Sub . (p 'Us' q)
proof end;

theorem Th25: :: LTLAXIO3:25
for p being Element of LTLB_WFF holds tau1 . p c= Sub . p
proof end;

registration
let p be Element of LTLB_WFF ;
cluster Sub . p -> non empty finite ;
coherence
( not Sub . p is empty & Sub . p is finite )
proof end;
end;

theorem :: LTLAXIO3:26
for A, B, p, q being Element of LTLB_WFF st p in Sub . (A 'Us' B) & A 'Us' B in Sub . q holds
p in Sub . q
proof end;

definition
let X be Subset of LTLB_WFF;
func Subt X -> Subset of (bool LTLB_WFF) equals :: LTLAXIO3:def 7
{ (Sub . A) where A is Element of LTLB_WFF : A in X } ;
correctness
coherence
{ (Sub . A) where A is Element of LTLB_WFF : A in X } is Subset of (bool LTLB_WFF)
;
proof end;
end;

:: deftheorem defines Subt LTLAXIO3:def 7 :
for X being Subset of LTLB_WFF holds Subt X = { (Sub . A) where A is Element of LTLB_WFF : A in X } ;

registration
let X be finite Subset of LTLB_WFF;
cluster Subt X -> finite finite-membered ;
coherence
( Subt X is finite & Subt X is finite-membered )
proof end;
end;

begin

definition
mode PNPair is Element of [:(LTLB_WFF **),(LTLB_WFF **):];
end;

set pairs = [:(LTLB_WFF **),(LTLB_WFF **):];

definition
let P be PNPair;
:: original: `1
redefine func P `1 -> one-to-one FinSequence of LTLB_WFF ;
coherence
P `1 is one-to-one FinSequence of LTLB_WFF
proof end;
:: original: `2
redefine func P `2 -> one-to-one FinSequence of LTLB_WFF ;
coherence
P `2 is one-to-one FinSequence of LTLB_WFF
proof end;
end;

definition
let P be PNPair;
func rng P -> finite Subset of LTLB_WFF equals :: LTLAXIO3:def 8
(rng (P `1)) \/ (rng (P `2));
correctness
coherence
(rng (P `1)) \/ (rng (P `2)) is finite Subset of LTLB_WFF
;
;
end;

:: deftheorem defines rng LTLAXIO3:def 8 :
for P being PNPair holds rng P = (rng (P `1)) \/ (rng (P `2));

definition
let fp, fm be one-to-one FinSequence of LTLB_WFF ;
:: original: [
redefine func [fp,fm] -> PNPair;
coherence
[fp,fm] is PNPair
proof end;
end;

definition
let P be PNPair;
func P ^ -> Element of LTLB_WFF equals :: LTLAXIO3:def 9
((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2)))));
correctness
coherence
((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2))))) is Element of LTLB_WFF
;
;
end;

:: deftheorem defines ^ LTLAXIO3:def 9 :
for P being PNPair holds P ^ = ((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2)))));

theorem Th28: :: LTLAXIO3:27
[(<*> LTLB_WFF),(<*> LTLB_WFF)] ^ = TVERUM '&&' TVERUM
proof end;

theorem Th29: :: LTLAXIO3:28
for A being Element of LTLB_WFF
for P being PNPair st A in rng (P `1) holds
{} LTLB_WFF |- (P ^) => A
proof end;

theorem Th30: :: LTLAXIO3:29
for A being Element of LTLB_WFF
for P being PNPair st A in rng (P `2) holds
{} LTLB_WFF |- (P ^) => ('not' A)
proof end;

definition
let P be PNPair;
attr P is Inconsistent means :Def10: :: LTLAXIO3:def 10
{} LTLB_WFF |- 'not' (P ^);
end;

:: deftheorem Def10 defines Inconsistent LTLAXIO3:def 10 :
for P being PNPair holds
( P is Inconsistent iff {} LTLB_WFF |- 'not' (P ^) );

notation
let P be PNPair;
antonym consistent P for Inconsistent ;
end;

definition
let P be PNPair;
attr P is complete means :Def11: :: LTLAXIO3:def 11
tau (rng P) = rng P;
end;

:: deftheorem Def11 defines complete LTLAXIO3:def 11 :
for P being PNPair holds
( P is complete iff tau (rng P) = rng P );

registration
cluster [(<*> LTLB_WFF),(<*> LTLB_WFF)] -> consistent for PNPair;
coherence
for b1 being PNPair st b1 = [(<*> LTLB_WFF),(<*> LTLB_WFF)] holds
not b1 is Inconsistent
proof end;
end;

registration
cluster [(<*> LTLB_WFF),(<*> LTLB_WFF)] -> complete for PNPair;
coherence
for b1 being PNPair st b1 = [(<*> LTLB_WFF),(<*> LTLB_WFF)] holds
b1 is complete
proof end;
end;

registration
cluster consistent complete for Element of [:(LTLB_WFF **),(LTLB_WFF **):];
existence
ex b1 being PNPair st
( b1 is consistent & b1 is complete )
proof end;
end;

registration
let P be consistent PNPair;
cluster [(P `1),(P `2)] -> consistent for PNPair;
coherence
for b1 being PNPair st b1 = [(P `1),(P `2)] holds
not b1 is Inconsistent
proof end;
end;

begin

theorem :: LTLAXIO3:30
for P being consistent PNPair holds rng (P `1) misses rng (P `2)
proof end;

theorem Th32: :: LTLAXIO3:31
for A being Element of LTLB_WFF
for P being consistent PNPair holds
( A in rng P or [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
proof end;

theorem :: LTLAXIO3:32
for P being consistent PNPair holds not TFALSUM in rng (P `1)
proof end;

theorem :: LTLAXIO3:33
for A, B being Element of LTLB_WFF
for P being consistent PNPair st A in rng P & B in rng P & A => B in rng P holds
( A => B in rng (P `1) iff ( A in rng (P `2) or B in rng (P `1) ) )
proof end;

theorem :: LTLAXIO3:34
for P being consistent PNPair ex P1 being consistent complete PNPair st
( rng (P `1) c= rng (P1 `1) & rng (P `2) c= rng (P1 `2) & tau (rng P) = rng P1 )
proof end;