:: by Mariusz Giero

::

:: Received May 7, 2012

:: Copyright (c) 2012-2021 Association of Mizar Users

set l = LTLB_WFF ;

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

deffunc H

deffunc H

definition

let X be finite set ;

:: original: Enumeration

redefine mode Enumeration of X -> one-to-one FinSequence of X;

coherence

for b_{1} being Enumeration of X holds b_{1} is one-to-one FinSequence of X

end;
:: original: Enumeration

redefine mode Enumeration of X -> one-to-one FinSequence of X;

coherence

for b

proof end;

definition

let E be set ;

let F be finite Subset of E;

:: original: Enumeration

redefine mode Enumeration of F -> one-to-one FinSequence of E;

coherence

for b_{1} being Enumeration of F holds b_{1} is one-to-one FinSequence of E

end;
let F be finite Subset of E;

:: original: Enumeration

redefine mode Enumeration of F -> one-to-one FinSequence of E;

coherence

for b

proof end;

registration

let D be set ;

existence

ex b_{1} being FinSequenceSet of D st

( not b_{1} is empty & b_{1} is finite )

end;
existence

ex b

( not b

proof end;

theorem Th1: :: LTLAXIO4:1

for X being set

for G being non empty finite FinSequenceSet of X ex A being FinSequence st

( A in G & ( for B being FinSequence st B in G holds

len B <= len A ) )

for G being non empty finite FinSequenceSet of X ex A being FinSequence st

( A in G & ( for B being FinSequence st B in G holds

len B <= len A ) )

proof end;

definition

let T be DecoratedTree;

let n be Element of NAT ;

let t be Node of T;

:: original: |

redefine func t | n -> Node of T;

correctness

coherence

t | n is Node of T;

end;
let n be Element of NAT ;

let t be Node of T;

:: original: |

redefine func t | n -> Node of T;

correctness

coherence

t | n is Node of T;

proof end;

definition

let A be Element of LTLB_WFF ;

assume A1: A is s-until ;

ex b_{1}, p being Element of LTLB_WFF st p 'U' b_{1} = A

for b_{1}, b_{2} being Element of LTLB_WFF st ex p being Element of LTLB_WFF st p 'U' b_{1} = A & ex p being Element of LTLB_WFF st p 'U' b_{2} = A holds

b_{1} = b_{2}
by HILBERT2:19;

end;
assume A1: A is s-until ;

func rarg A -> Element of LTLB_WFF means :Def1: :: LTLAXIO4:def 1

ex p being Element of LTLB_WFF st p 'U' it = A;

existence ex p being Element of LTLB_WFF st p 'U' it = A;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines rarg LTLAXIO4:def 1 :

for A being Element of LTLB_WFF st A is s-until holds

for b_{2} being Element of LTLB_WFF holds

( b_{2} = rarg A iff ex p being Element of LTLB_WFF st p 'U' b_{2} = A );

for A being Element of LTLB_WFF st A is s-until holds

for b

( b

:: deftheorem defines satisfiable LTLAXIO4:def 2 :

for A being Element of LTLB_WFF holds

( A is satisfiable iff ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1 );

for A being Element of LTLB_WFF holds

( A is satisfiable iff ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1 );

theorem Th5: :: LTLAXIO4:5

for p, q being Element of LTLB_WFF

for M being LTLModel

for i being Element of NAT holds

( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st

( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds

(SAT M) . [k,p] = 1 ) ) )

for M being LTLModel

for i being Element of NAT holds

( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st

( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds

(SAT M) . [k,p] = 1 ) ) )

proof end;

theorem Th6: :: LTLAXIO4:6

for M being LTLModel

for n being Element of NAT

for f being FinSequence of LTLB_WFF holds

( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds

(SAT M) . [n,(f /. i)] = 1 )

for n being Element of NAT

for f being FinSequence of LTLB_WFF holds

( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds

(SAT M) . [n,(f /. i)] = 1 )

proof end;

theorem Th8: :: LTLAXIO4:8

for A, B being Element of LTLB_WFF

for P being complete PNPair st untn (A,B) in rng P holds

( A in rng P & B in rng P & A 'U' B in rng P )

for P being complete PNPair st untn (A,B) in rng P holds

( A in rng P & B in rng P & A 'U' B in rng P )

proof end;

definition

let F be Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

{ (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } is Subset of LTLB_WFF

end;
func F ^ -> Subset of LTLB_WFF equals :: LTLAXIO4:def 3

{ (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;

coherence { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;

{ (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } is Subset of LTLB_WFF

proof end;

:: deftheorem defines ^ LTLAXIO4:def 3 :

for F being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds F ^ = { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;

for F being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds F ^ = { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;

registration
end;

registration
end;

definition

let F be finite Subset of LTLB_WFF;

{ Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

end;
func comp F -> non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 4

{ Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

coherence { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

{ Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

:: deftheorem defines comp LTLAXIO4:def 4 :

for F being finite Subset of LTLB_WFF holds comp F = { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

for F being finite Subset of LTLB_WFF holds comp F = { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

registration

let F be finite Subset of LTLB_WFF;

coherence

for b_{1} being Element of comp F holds b_{1} is complete

end;
coherence

for b

proof end;

:: deftheorem defines is_completion_of LTLAXIO4:def 5 :

for P, Q being PNPair holds

( Q is_completion_of P iff ( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q ) );

for P, Q being PNPair holds

( Q is_completion_of P iff ( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q ) );

definition

let P be PNPair;

{ Q where Q is consistent PNPair : Q is_completion_of P } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

end;
func comp P -> finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 6

{ Q where Q is consistent PNPair : Q is_completion_of P } ;

coherence { Q where Q is consistent PNPair : Q is_completion_of P } ;

{ Q where Q is consistent PNPair : Q is_completion_of P } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

:: deftheorem defines comp LTLAXIO4:def 6 :

for P being PNPair holds comp P = { Q where Q is consistent PNPair : Q is_completion_of P } ;

for P being PNPair holds comp P = { Q where Q is consistent PNPair : Q is_completion_of P } ;

registration

let P be consistent PNPair;

coherence

for b_{1} being Element of comp P holds b_{1} is consistent

end;
coherence

for b

proof end;

definition

let X be Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } is Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

end;
func comp X -> Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 7

union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;

coherence union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;

union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } is Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

:: deftheorem defines comp LTLAXIO4:def 7 :

for X being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds comp X = union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;

for X being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds comp X = union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;

registration
end;

theorem Th14: :: LTLAXIO4:14

for Q being PNPair

for X being non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):] st Q in X holds

comp Q c= comp X

for X being non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):] st Q in X holds

comp Q c= comp X

proof end;

theorem Th15: :: LTLAXIO4:15

for F being non empty finite Subset of LTLB_WFF ex p being Element of LTLB_WFF st

( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )

( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )

proof end;

theorem Th16: :: LTLAXIO4:16

for F being finite Subset of LTLB_WFF

for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds

{} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f))))

for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds

{} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f))))

proof end;

theorem Th17: :: LTLAXIO4:17

for P being consistent PNPair

for f being FinSequence of LTLB_WFF st rng f = (comp P) ^ holds

{} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f)))))

for f being FinSequence of LTLB_WFF st rng f = (comp P) ^ holds

{} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f)))))

proof end;

definition

let X be Subset of LTLB_WFF;

{ (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } is Subset of LTLB_WFF

end;
func untn X -> Subset of LTLB_WFF equals :: LTLAXIO4:def 8

{ (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

coherence { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

{ (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } is Subset of LTLB_WFF

proof end;

:: deftheorem defines untn LTLAXIO4:def 8 :

for X being Subset of LTLB_WFF holds untn X = { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

for X being Subset of LTLB_WFF holds untn X = { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

definition

let P be PNPair;

{ Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

end;
func untn P -> non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 9

{ Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

coherence { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

{ Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

:: deftheorem defines untn LTLAXIO4:def 9 :

for P being PNPair holds untn P = { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

for P being PNPair holds untn P = { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

registration

let P be consistent PNPair;

coherence

for b_{1} being Element of untn P holds b_{1} is consistent

end;
coherence

for b

proof end;

definition

let P be PNPair;

{ Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

end;
func compn P -> finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 10

{ Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;

coherence { Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;

{ Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

:: deftheorem defines compn LTLAXIO4:def 10 :

for P being PNPair holds compn P = { Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;

for P being PNPair holds compn P = { Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;

registration

let P be consistent PNPair;

coherence

for b_{1} being Element of compn P holds b_{1} is consistent

end;
coherence

for b

proof end;

registration

let P be consistent PNPair;

coherence

for b_{1} being Element of compn P holds b_{1} is complete
by Th20;

end;
coherence

for b

theorem Th21: :: LTLAXIO4:21

for A, B being Element of LTLB_WFF

for P, Q being PNPair st A 'U' B in rng (P `2) & Q in compn P holds

untn (A,B) in rng (Q `2)

for P, Q being PNPair st A 'U' B in rng (P `2) & Q in compn P holds

untn (A,B) in rng (Q `2)

proof end;

theorem Th22: :: LTLAXIO4:22

for A, B being Element of LTLB_WFF

for P, Q being PNPair st A 'U' B in rng (P `1) & Q in compn P holds

untn (A,B) in rng (Q `1)

for P, Q being PNPair st A 'U' B in rng (P `1) & Q in compn P holds

untn (A,B) in rng (Q `1)

proof end;

theorem Th23: :: LTLAXIO4:23

for P, Q, R being PNPair st R in compn Q & rng Q c= union (Subt (rng P)) holds

rng R c= union (Subt (rng P))

rng R c= union (Subt (rng P))

proof end;

theorem Th24: :: LTLAXIO4:24

for A, B being Element of LTLB_WFF

for P being consistent complete PNPair

for Q being Element of compn P st A 'U' B in rng (P `2) holds

( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) )

for P being consistent complete PNPair

for Q being Element of compn P st A 'U' B in rng (P `2) holds

( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) )

proof end;

theorem Th25: :: LTLAXIO4:25

for A, B being Element of LTLB_WFF

for P being consistent complete PNPair

for Q being Element of compn P holds

( not A 'U' B in rng (P `1) or B in rng (Q `1) or ( A in rng (Q `1) & A 'U' B in rng (Q `1) ) )

for P being consistent complete PNPair

for Q being Element of compn P holds

( not A 'U' B in rng (P `1) or B in rng (Q `1) or ( A in rng (Q `1) & A 'U' B in rng (Q `1) ) )

proof end;

definition

let P be PNPair;

existence

ex b_{1} being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] st

( b_{1} . {} = P & ( for t being Element of dom b_{1}

for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b_{1} . t holds

succ (b_{1},t) = the Enumeration of compn w ) );

end;
mode pnptree of P -> finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] means :Def11: :: LTLAXIO4:def 11

( it . {} = P & ( for t being Element of dom it

for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = it . t holds

succ (it,t) = the Enumeration of compn w ) );

correctness ( it . {} = P & ( for t being Element of dom it

for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = it . t holds

succ (it,t) = the Enumeration of compn w ) );

existence

ex b

( b

for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b

succ (b

proof end;

:: deftheorem Def11 defines pnptree LTLAXIO4:def 11 :

for P being PNPair

for b_{2} being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] holds

( b_{2} is pnptree of P iff ( b_{2} . {} = P & ( for t being Element of dom b_{2}

for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b_{2} . t holds

succ (b_{2},t) = the Enumeration of compn w ) ) );

for P being PNPair

for b

( b

for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b

succ (b

definition

let P be PNPair;

let T be pnptree of P;

let t be Node of T;

:: original: |

redefine func T | t -> pnptree of T . t;

correctness

coherence

T | t is pnptree of T . t;

end;
let T be pnptree of P;

let t be Node of T;

:: original: |

redefine func T | t -> pnptree of T . t;

correctness

coherence

T | t is pnptree of T . t;

proof end;

theorem Th26: :: LTLAXIO4:26

for P being PNPair

for T being pnptree of P

for t being Node of T

for n being Nat st t ^ <*n*> in dom T holds

T . (t ^ <*n*>) in compn (T . t)

for T being pnptree of P

for t being Node of T

for n being Nat st t ^ <*n*> in dom T holds

T . (t ^ <*n*>) in compn (T . t)

proof end;

registration

let P be PNPair;

let T be pnptree of P;

coherence

( not rng T is empty & rng T is finite )

end;
let T be pnptree of P;

coherence

( not rng T is empty & rng T is finite )

proof end;

registration

let P be consistent PNPair;

let T be pnptree of P;

coherence

for b_{1} being Element of rng T holds b_{1} is consistent

end;
let T be pnptree of P;

coherence

for b

proof end;

registration

let P be consistent complete PNPair;

let T be pnptree of P;

coherence

for b_{1} being Element of rng T holds b_{1} is complete

end;
let T be pnptree of P;

coherence

for b

proof end;

registration

let P be consistent complete PNPair;

let T be pnptree of P;

let t be Node of T;

coherence

for b_{1} being PNPair st b_{1} = T . t holds

( not b_{1} is Inconsistent & b_{1} is complete )

end;
let T be pnptree of P;

let t be Node of T;

coherence

for b

( not b

proof end;

registration

let P be consistent PNPair;

let T be pnptree of P;

let t be Element of dom T;

coherence

not succ t is empty

end;
let T be pnptree of P;

let t be Element of dom T;

coherence

not succ t is empty

proof end;

definition

let P be PNPair;

let T be pnptree of P;

coherence

{ (T . t) where t is Node of T : t <> {} } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

end;
let T be pnptree of P;

func rngr T -> finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 12

{ (T . t) where t is Node of T : t <> {} } ;

correctness { (T . t) where t is Node of T : t <> {} } ;

coherence

{ (T . t) where t is Node of T : t <> {} } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

proof end;

:: deftheorem defines rngr LTLAXIO4:def 12 :

for P being PNPair

for T being pnptree of P holds rngr T = { (T . t) where t is Node of T : t <> {} } ;

for P being PNPair

for T being pnptree of P holds rngr T = { (T . t) where t is Node of T : t <> {} } ;

registration
end;

theorem Th28: :: LTLAXIO4:28

for P, Q, R being PNPair

for T being pnptree of P st R in rng T & Q in untn R holds

comp Q c= rngr T

for T being pnptree of P st R in rng T & Q in untn R holds

comp Q c= rngr T

proof end;

theorem Th29: :: LTLAXIO4:29

for P being consistent complete PNPair

for T being pnptree of P

for f being FinSequence of LTLB_WFF st rng f = (rngr T) ^ holds

{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f))))))

for T being pnptree of P

for f being FinSequence of LTLB_WFF st rng f = (rngr T) ^ holds

{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f))))))

proof end;

definition

let P be consistent PNPair;

let T be pnptree of P;

ex b_{1} being sequence of (dom T) st

( b_{1} . 0 = {} & ( for k being Nat holds b_{1} . (k + 1) in succ (b_{1} . k) ) )

end;
let T be pnptree of P;

mode path of T -> sequence of (dom T) means :Def13: :: LTLAXIO4:def 13

( it . 0 = {} & ( for k being Nat holds it . (k + 1) in succ (it . k) ) );

existence ( it . 0 = {} & ( for k being Nat holds it . (k + 1) in succ (it . k) ) );

ex b

( b

proof end;

:: deftheorem Def13 defines path LTLAXIO4:def 13 :

for P being consistent PNPair

for T being pnptree of P

for b_{3} being sequence of (dom T) holds

( b_{3} is path of T iff ( b_{3} . 0 = {} & ( for k being Nat holds b_{3} . (k + 1) in succ (b_{3} . k) ) ) );

for P being consistent PNPair

for T being pnptree of P

for b

( b

definition

let P be consistent complete PNPair;

let T be pnptree of P;

let t be path of T;

let i be Nat;

:: original: .

redefine func t . i -> Node of T;

coherence

t . i is Node of T

end;
let T be pnptree of P;

let t be path of T;

let i be Nat;

:: original: .

redefine func t . i -> Node of T;

coherence

t . i is Node of T

proof end;

theorem Th30: :: LTLAXIO4:30

for A, B being Element of LTLB_WFF

for i being Nat

for P being consistent complete PNPair

for T being pnptree of P

for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds

for j being Element of NAT holds

( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st

( i < k & k < j & A in rng ((T . (t . k)) `2) ) )

for i being Nat

for P being consistent complete PNPair

for T being pnptree of P

for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds

for j being Element of NAT holds

( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st

( i < k & k < j & A in rng ((T . (t . k)) `2) ) )

proof end;

theorem Th31: :: LTLAXIO4:31

for A, B being Element of LTLB_WFF

for P being consistent complete PNPair

for T being pnptree of P st A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) holds

for Q being Element of rngr T holds

( B in rng (Q `2) & A 'U' B in rng (Q `1) )

for P being consistent complete PNPair

for T being pnptree of P st A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) holds

for Q being Element of rngr T holds

( B in rng (Q `2) & A 'U' B in rng (Q `1) )

proof end;

theorem Th32: :: LTLAXIO4:32

for A, B being Element of LTLB_WFF

for P being consistent complete PNPair

for T being pnptree of P st A 'U' B in rng (P `1) holds

ex R being Element of rngr T st B in rng (R `1)

for P being consistent complete PNPair

for T being pnptree of P st A 'U' B in rng (P `1) holds

ex R being Element of rngr T st B in rng (R `1)

proof end;

:: deftheorem Def14 defines complete LTLAXIO4:def 14 :

for P being consistent PNPair

for T being pnptree of P

for t being path of T holds

( t is complete iff for A, B being Element of LTLB_WFF

for i being Nat st A 'U' B in rng ((T . (t . i)) `1) holds

ex j being Element of NAT st

( j > i & B in rng ((T . (t . j)) `1) & ( for k being Element of NAT st i < k & k < j holds

A in rng ((T . (t . k)) `1) ) ) );

for P being consistent PNPair

for T being pnptree of P

for t being path of T holds

( t is complete iff for A, B being Element of LTLB_WFF

for i being Nat st A 'U' B in rng ((T . (t . i)) `1) holds

ex j being Element of NAT st

( j > i & B in rng ((T . (t . j)) `1) & ( for k being Element of NAT st i < k & k < j holds

A in rng ((T . (t . k)) `1) ) ) );

registration

let P be consistent complete PNPair;

let T be pnptree of P;

ex b_{1} being path of T st b_{1} is complete

end;
let T be pnptree of P;

cluster Relation-like omega -defined dom T -valued Function-like V36( omega , dom T) complete for path of T;

existence ex b

proof end;

registration
end;

:: Completeness theorem for Propositional Linear Temporal Logic