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

set l = LTLB_WFF ;

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

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 :: LTLAXIO3:def 1
for p being Element of LTLB_WFF st p in X holds
not p is conditional ;

end;

:: deftheorem 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 b₁ being set st
for x being set holds
( x in b₁ iff x is one-to-one FinSequence of D )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is one-to-one FinSequence of D ) ) & ( for x being set holds
( x in b₂ iff x is one-to-one FinSequence of D ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ** LTLAXIO3:def 2 :
for D, b₂ being set holds
( b₂ = D ** iff for x being set holds
( x in b₂ 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;

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 'U' B) = {(A 'U' B)} );

existence
ex b₁ being Function of LTLB_WFF,(bool LTLB_WFF) st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = {TFALSUM} & b₁ . (prop n) = {(prop n)} & b₁ . (A => B) = ({(A => B)} \/ (b₁ . A)) \/ (b₁ . B) & b₁ . (A 'U' B) = {(A 'U' B)} )

proof end;

uniqueness
for b₁, b₂ being Function of LTLB_WFF,(bool LTLB_WFF) st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = {TFALSUM} & b₁ . (prop n) = {(prop n)} & b₁ . (A => B) = ({(A => B)} \/ (b₁ . A)) \/ (b₁ . B) & b₁ . (A 'U' B) = {(A 'U' B)} ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₂ . TFALSUM = {TFALSUM} & b₂ . (prop n) = {(prop n)} & b₂ . (A => B) = ({(A => B)} \/ (b₂ . A)) \/ (b₂ . B) & b₂ . (A 'U' B) = {(A 'U' B)} ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines tau1 LTLAXIO3:def 4 :
for b₁ being Function of LTLB_WFF,(bool LTLB_WFF) holds
( b₁ = tau1 iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = {TFALSUM} & b₁ . (prop n) = {(prop n)} & b₁ . (A => B) = ({(A => B)} \/ (b₁ . A)) \/ (b₁ . B) & b₁ . (A 'U' B) = {(A 'U' 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 'U' q in tau1 . ('not' A) holds
p 'U' q in tau1 . A

proof end;

theorem Th10: :: LTLAXIO3:10

for A, B, p, q being Element of LTLB_WFF holds
( not p 'U' q in tau1 . (A '&&' B) or p 'U' q in tau1 . A or p 'U' 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 b₁ being Subset of LTLB_WFF st
for x being set holds
( x in b₁ iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) )

proof end;

uniqueness
for b₁, b₂ being Subset of LTLB_WFF st ( for x being set holds
( x in b₁ iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) ) & ( for x being set holds
( x in b₂ iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines tau LTLAXIO3:def 5 :
for X, b₂ being Subset of LTLB_WFF holds
( b₂ = tau X iff for x being set holds
( x in b₂ 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 :: 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 'U' 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;

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 'U' B) = ((tau1 . (untn (A,B))) \/ (it . A)) \/ (it . B) );

existence
ex b₁ being Function of LTLB_WFF,(bool LTLB_WFF) st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = {TFALSUM} & b₁ . (prop n) = {(prop n)} & b₁ . (A => B) = ({(A => B)} \/ (b₁ . A)) \/ (b₁ . B) & b₁ . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (b₁ . A)) \/ (b₁ . B) )

proof end;

uniqueness
for b₁, b₂ being Function of LTLB_WFF,(bool LTLB_WFF) st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = {TFALSUM} & b₁ . (prop n) = {(prop n)} & b₁ . (A => B) = ({(A => B)} \/ (b₁ . A)) \/ (b₁ . B) & b₁ . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (b₁ . A)) \/ (b₁ . B) ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₂ . TFALSUM = {TFALSUM} & b₂ . (prop n) = {(prop n)} & b₂ . (A => B) = ({(A => B)} \/ (b₂ . A)) \/ (b₂ . B) & b₂ . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (b₂ . A)) \/ (b₂ . B) ) ) holds
b₁ = b₂

proof end;

end;

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

theorem Th24: :: LTLAXIO3:24

for p, q being Element of LTLB_WFF holds p 'U' q in Sub . (p 'U' 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 'U' B) & A 'U' 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;

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 Th27: :: LTLAXIO3:27

[(<*> LTLB_WFF),(<*> LTLB_WFF)] ^ = TVERUM '&&' TVERUM

proof end;

theorem Th28: :: 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 Th29: :: 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 :: LTLAXIO3:def 11
tau (rng P) = rng P;

end;

:: deftheorem 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 b₁ being PNPair st b₁ = [(<*> LTLB_WFF),(<*> LTLB_WFF)] holds
not b₁ is Inconsistent

proof end;

end;

registration

cluster [(<*> LTLB_WFF),(<*> LTLB_WFF)] -> complete for PNPair;

coherence
for b₁ being PNPair st b₁ = [(<*> LTLB_WFF),(<*> LTLB_WFF)] holds
b₁ is complete

proof end;

end;

registration

cluster consistent complete for Element of [:(LTLB_WFF **),(LTLB_WFF **):];

existence
ex b₁ being PNPair st
( b₁ is consistent & b₁ is complete )

proof end;

end;

registration

let P be consistent PNPair;

cluster [(P `1),(P `2)] -> consistent for PNPair;

coherence
for b₁ being PNPair st b₁ = [(P `1),(P `2)] holds
not b₁ is Inconsistent

proof end;

end;

theorem :: LTLAXIO3:30

for P being consistent PNPair holds rng (P `1) misses rng (P `2)

proof end;

theorem Th31: :: 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 PNPair st
( rng (P `1) c= rng (P1 `1) & rng (P `2) c= rng (P1 `2) & tau (rng P) = rng P1 )

proof end;