:: by Mariusz Giero

::

:: Received May 7, 2012

:: Copyright (c) 2012 Association of Mizar Users

begin

set l = LTLB_WFF ;

deffunc H

deffunc H

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

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;

definition

let X be Subset of LTLB_WFF;

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

for p being Element of LTLB_WFF st p in X holds

not p is conditional ;

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

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 ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is one-to-one FinSequence of D )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is one-to-one FinSequence of D ) ) & ( for x being set holds

( x in b_{2} iff x is one-to-one FinSequence of D ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is one-to-one FinSequence of D );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines ** LTLAXIO3:def 2 :

for D, b_{2} being set holds

( b_{2} = D ** iff for x being set holds

( x in b_{2} iff x is one-to-one FinSequence of D ) );

for D, b

( b

( x in b

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

definition

let X be set ;

let f, g be one-to-one FinSequence of X;

assume A1: rng f misses rng g ;

coherence

f ^ g is one-to-one FinSequence of X by Th4, A1;

end;
let f, g be one-to-one FinSequence of X;

assume A1: rng f misses rng g ;

coherence

f ^ g is one-to-one FinSequence of X by Th4, A1;

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

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

ex b_{1} 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_{1} . TFALSUM = {TFALSUM} & b_{1} . (prop n) = {(prop n)} & b_{1} . (A => B) = ({(A => B)} \/ (b_{1} . A)) \/ (b_{1} . B) & b_{1} . (A 'Us' B) = {(A 'Us' B)} )

for b_{1}, b_{2} 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_{1} . TFALSUM = {TFALSUM} & b_{1} . (prop n) = {(prop n)} & b_{1} . (A => B) = ({(A => B)} \/ (b_{1} . A)) \/ (b_{1} . B) & b_{1} . (A 'Us' B) = {(A 'Us' B)} ) ) & ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{2} . TFALSUM = {TFALSUM} & b_{2} . (prop n) = {(prop n)} & b_{2} . (A => B) = ({(A => B)} \/ (b_{2} . A)) \/ (b_{2} . B) & b_{2} . (A 'Us' B) = {(A 'Us' B)} ) ) holds

b_{1} = b_{2}
end;

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

ex b

for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b

proof end;

uniqueness for b

for n being Element of NAT holds

( b

for n being Element of NAT holds

( b

b

proof end;

:: deftheorem Def4 defines tau1 LTLAXIO3:def 4 :

for b_{1} being Function of LTLB_WFF,(bool LTLB_WFF) holds

( b_{1} = tau1 iff for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{1} . TFALSUM = {TFALSUM} & b_{1} . (prop n) = {(prop n)} & b_{1} . (A => B) = ({(A => B)} \/ (b_{1} . A)) \/ (b_{1} . B) & b_{1} . (A 'Us' B) = {(A 'Us' B)} ) );

for b

( b

for n being Element of NAT holds

( b

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

( not p 'Us' q in tau1 . (A '&&' B) or p 'Us' q in tau1 . A or p 'Us' q in tau1 . B )

proof end;

definition

let X be Subset of LTLB_WFF;

ex b_{1} being Subset of LTLB_WFF st

for x being set holds

( x in b_{1} iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) )

for b_{1}, b_{2} being Subset of LTLB_WFF st ( for x being set holds

( x in b_{1} iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ) & ( for x being set holds

( x in b_{2} iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) );

ex b

for x being set holds

( x in b

( A in X & x in tau1 . A ) )

proof end;

uniqueness for b

( x in b

( A in X & x in tau1 . A ) ) ) & ( for x being set holds

( x in b

( A in X & x in tau1 . A ) ) ) holds

b

proof end;

:: deftheorem Def5 defines tau LTLAXIO3:def 5 :

for X, b_{2} being Subset of LTLB_WFF holds

( b_{2} = tau X iff for x being set holds

( x in b_{2} iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) );

for X, b

( b

( x in b

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

registration
end;

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

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 )

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 )

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 )

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

for X being Subset of LTLB_WFF st p in tau X holds

tau1 . p c= tau X

proof end;

begin

definition

ex b_{1} 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_{1} . TFALSUM = {TFALSUM} & b_{1} . (prop n) = {(prop n)} & b_{1} . (A => B) = ({(A => B)} \/ (b_{1} . A)) \/ (b_{1} . B) & b_{1} . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b_{1} . A)) \/ (b_{1} . B) )

for b_{1}, b_{2} 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_{1} . TFALSUM = {TFALSUM} & b_{1} . (prop n) = {(prop n)} & b_{1} . (A => B) = ({(A => B)} \/ (b_{1} . A)) \/ (b_{1} . B) & b_{1} . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b_{1} . A)) \/ (b_{1} . B) ) ) & ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{2} . TFALSUM = {TFALSUM} & b_{2} . (prop n) = {(prop n)} & b_{2} . (A => B) = ({(A => B)} \/ (b_{2} . A)) \/ (b_{2} . B) & b_{2} . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b_{2} . A)) \/ (b_{2} . B) ) ) holds

b_{1} = b_{2}
end;

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

ex b

for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b

proof end;

uniqueness for b

for n being Element of NAT holds

( b

for n being Element of NAT holds

( b

b

proof end;

:: deftheorem Def6 defines Sub LTLAXIO3:def 6 :

for b_{1} being Function of LTLB_WFF,(bool LTLB_WFF) holds

( b_{1} = Sub iff for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( b_{1} . TFALSUM = {TFALSUM} & b_{1} . (prop n) = {(prop n)} & b_{1} . (A => B) = ({(A => B)} \/ (b_{1} . A)) \/ (b_{1} . B) & b_{1} . (A 'Us' B) = ((tau1 . (untn (A,B))) \/ (b_{1} . A)) \/ (b_{1} . B) ) );

for b

( b

for n being Element of NAT holds

( b

registration
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

p in Sub . q

proof end;

definition

let X be Subset of LTLB_WFF;

coherence

{ (Sub . A) where A is Element of LTLB_WFF : A in X } is Subset of (bool LTLB_WFF);

end;
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 { (Sub . A) where A is Element of LTLB_WFF : A in X } ;

coherence

{ (Sub . A) where A is Element of LTLB_WFF : A in X } is Subset of (bool LTLB_WFF);

proof 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 } ;

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;

coherence

( Subt X is finite & Subt X is finite-membered )

end;
coherence

( Subt X is finite & Subt X is finite-membered )

proof end;

begin

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

redefine func P `2 -> one-to-one FinSequence of LTLB_WFF ;

coherence

P `2 is one-to-one FinSequence of LTLB_WFF

end;
:: 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: `2redefine func P `2 -> one-to-one FinSequence of LTLB_WFF ;

coherence

P `2 is one-to-one FinSequence of LTLB_WFF

proof end;

definition
end;

:: deftheorem defines rng LTLAXIO3:def 8 :

for P being PNPair holds rng P = (rng (P `1)) \/ (rng (P `2));

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

end;
:: original: [

redefine func [fp,fm] -> PNPair;

coherence

[fp,fm] is PNPair

proof end;

definition

let P be PNPair;

coherence

((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2))))) is Element of LTLB_WFF ;

;

end;
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 ((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2)))));

coherence

((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2))))) is Element of LTLB_WFF ;

;

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

for P being PNPair holds P ^ = ((con (P `1)) /. (len (con (P `1)))) '&&' ((con (nega (P `2))) /. (len (con (nega (P `2)))));

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

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)

for P being PNPair st A in rng (P `2) holds

{} LTLB_WFF |- (P ^) => ('not' A)

proof end;

:: deftheorem Def10 defines Inconsistent LTLAXIO3:def 10 :

for P being PNPair holds

( P is Inconsistent iff {} LTLB_WFF |- 'not' (P ^) );

for P being PNPair holds

( P is Inconsistent iff {} LTLB_WFF |- 'not' (P ^) );

definition
end;

:: deftheorem Def11 defines complete LTLAXIO3:def 11 :

for P being PNPair holds

( P is complete iff tau (rng P) = rng P );

for P being PNPair holds

( P is complete iff tau (rng P) = rng P );

registration

coherence

for b_{1} being PNPair st b_{1} = [(<*> LTLB_WFF),(<*> LTLB_WFF)] holds

not b_{1} is Inconsistent

end;
for b

not b

proof end;

registration

coherence

for b_{1} being PNPair st b_{1} = [(<*> LTLB_WFF),(<*> LTLB_WFF)] holds

b_{1} is complete

end;
for b

b

proof end;

registration
end;

registration

let P be consistent PNPair;

coherence

for b_{1} being PNPair st b_{1} = [(P `1),(P `2)] holds

not b_{1} is Inconsistent

end;
coherence

for b

not b

proof end;

begin

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 )

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

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 )

( rng (P `1) c= rng (P1 `1) & rng (P `2) c= rng (P1 `2) & tau (rng P) = rng P1 )

proof end;