:: by Kazuhisa Ishida and Yasunari Shidama

::

:: Received August 19, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

Lm1: for a, X1, X2, X3 being set holds

( a in (X1 \/ X2) \/ X3 iff ( a in X1 or a in X2 or a in X3 ) )

proof end;

Lm2: for a, X1, X2, X3, X4 being set holds

( a in (X1 \ X2) \/ (X3 \ X4) iff ( ( a in X1 & not a in X2 ) or ( a in X3 & not a in X4 ) ) )

proof end;

Lm3: for H being LTL-formula holds

( <*H*> . 1 = H & rng <*H*> = {H} )

proof end;

Lm4: for r1, r2 being Real st r1 <= r2 holds

[\r1/] <= [\r2/]

proof end;

Lm5: for r1, r2 being Real st r1 <= r2 - 1 holds

[\r1/] <= [\r2/] - 1

proof end;

Lm6: for n being Nat holds

( n = 0 or 1 <= n )

proof end;

Lm7: for H being LTL-formula st ( H is negative or H is next ) holds

the_argument_of H is_subformula_of H

proof end;

Lm8: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

( the_left_argument_of H is_subformula_of H & the_right_argument_of H is_subformula_of H )

proof end;

Lm9: for F, H being LTL-formula st F is_subformula_of H holds

{F} is Subset of (Subformulae H)

by MODELC_2:45, SUBSET_1:41;

Lm10: for F, G, H being LTL-formula st F is_subformula_of H & G is_subformula_of H holds

{F,G} is Subset of (Subformulae H)

proof end;

Lm11: for H being LTL-formula st ( H is disjunctive or H is conjunctive or H is Until or H is Release ) holds

{(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H)

proof end;

Lm12: for H being LTL-formula st ( H is disjunctive or H is conjunctive or H is Until or H is Release ) holds

( {(the_left_argument_of H)} is Subset of (Subformulae H) & {(the_right_argument_of H)} is Subset of (Subformulae H) )

proof end;

Lm13: for H being LTL-formula holds {H} is Subset of (Subformulae H)

by Lm9;

Lm14: for H being LTL-formula st ( H is negative or H is next ) holds

{(the_argument_of H)} is Subset of (Subformulae H)

proof end;

definition

let F be LTL-formula;

:: original: Subformulae

redefine func Subformulae F -> Subset of LTL_WFF;

coherence

Subformulae F is Subset of LTL_WFF

end;
:: original: Subformulae

redefine func Subformulae F -> Subset of LTL_WFF;

coherence

Subformulae F is Subset of LTL_WFF

proof end;

:: definition of basic operations to build an automaton for LTL.

definition

let H be LTL-formula;

coherence

( ( H is conjunctive implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is disjunctive implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) & ( H is next implies {} is Subset of (Subformulae H) ) & ( H is Until implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) & ( H is Release implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );

consistency

for b_{1} being Subset of (Subformulae H) holds

( ( H is conjunctive & H is disjunctive implies ( b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} iff b_{1} = {(the_left_argument_of H)} ) ) & ( H is conjunctive & H is next implies ( b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} iff b_{1} = {} ) ) & ( H is conjunctive & H is Until implies ( b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} iff b_{1} = {(the_left_argument_of H)} ) ) & ( H is conjunctive & H is Release implies ( b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is disjunctive & H is next implies ( b_{1} = {(the_left_argument_of H)} iff b_{1} = {} ) ) & ( H is disjunctive & H is Until implies ( b_{1} = {(the_left_argument_of H)} iff b_{1} = {(the_left_argument_of H)} ) ) & ( H is disjunctive & H is Release implies ( b_{1} = {(the_left_argument_of H)} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is next & H is Until implies ( b_{1} = {} iff b_{1} = {(the_left_argument_of H)} ) ) & ( H is next & H is Release implies ( b_{1} = {} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is Until & H is Release implies ( b_{1} = {(the_left_argument_of H)} iff b_{1} = {(the_right_argument_of H)} ) ) );

by Lm11, Lm12, MODELC_2:78, SUBSET_1:1;

coherence

( ( H is conjunctive implies {} is Subset of (Subformulae H) ) & ( H is disjunctive implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is next implies {} is Subset of (Subformulae H) ) & ( H is Until implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is Release implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );

consistency

for b_{1} being Subset of (Subformulae H) holds

( ( H is conjunctive & H is disjunctive implies ( b_{1} = {} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is conjunctive & H is next implies ( b_{1} = {} iff b_{1} = {} ) ) & ( H is conjunctive & H is Until implies ( b_{1} = {} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is conjunctive & H is Release implies ( b_{1} = {} iff b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} ) ) & ( H is disjunctive & H is next implies ( b_{1} = {(the_right_argument_of H)} iff b_{1} = {} ) ) & ( H is disjunctive & H is Until implies ( b_{1} = {(the_right_argument_of H)} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is disjunctive & H is Release implies ( b_{1} = {(the_right_argument_of H)} iff b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} ) ) & ( H is next & H is Until implies ( b_{1} = {} iff b_{1} = {(the_right_argument_of H)} ) ) & ( H is next & H is Release implies ( b_{1} = {} iff b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} ) ) & ( H is Until & H is Release implies ( b_{1} = {(the_right_argument_of H)} iff b_{1} = {(the_left_argument_of H),(the_right_argument_of H)} ) ) );

by Lm11, Lm12, MODELC_2:78, SUBSET_1:1;

coherence

( ( H is conjunctive implies {} is Subset of (Subformulae H) ) & ( H is disjunctive implies {} is Subset of (Subformulae H) ) & ( H is next implies {(the_argument_of H)} is Subset of (Subformulae H) ) & ( H is Until implies {H} is Subset of (Subformulae H) ) & ( H is Release implies {H} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );

consistency

for b_{1} being Subset of (Subformulae H) holds

( ( H is conjunctive & H is disjunctive implies ( b_{1} = {} iff b_{1} = {} ) ) & ( H is conjunctive & H is next implies ( b_{1} = {} iff b_{1} = {(the_argument_of H)} ) ) & ( H is conjunctive & H is Until implies ( b_{1} = {} iff b_{1} = {H} ) ) & ( H is conjunctive & H is Release implies ( b_{1} = {} iff b_{1} = {H} ) ) & ( H is disjunctive & H is next implies ( b_{1} = {} iff b_{1} = {(the_argument_of H)} ) ) & ( H is disjunctive & H is Until implies ( b_{1} = {} iff b_{1} = {H} ) ) & ( H is disjunctive & H is Release implies ( b_{1} = {} iff b_{1} = {H} ) ) & ( H is next & H is Until implies ( b_{1} = {(the_argument_of H)} iff b_{1} = {H} ) ) & ( H is next & H is Release implies ( b_{1} = {(the_argument_of H)} iff b_{1} = {H} ) ) & ( H is Until & H is Release implies ( b_{1} = {H} iff b_{1} = {H} ) ) );

by Lm13, Lm14, MODELC_2:78, SUBSET_1:1;

end;
func LTLNew1 H -> Subset of (Subformulae H) equals :Def1: :: MODELC_3:def 1

{(the_left_argument_of H),(the_right_argument_of H)} if H is conjunctive

{(the_left_argument_of H)} if H is disjunctive

{} if H is next

{(the_left_argument_of H)} if H is Until

{(the_right_argument_of H)} if H is Release

otherwise {} ;

correctness {(the_left_argument_of H),(the_right_argument_of H)} if H is conjunctive

{(the_left_argument_of H)} if H is disjunctive

{} if H is next

{(the_left_argument_of H)} if H is Until

{(the_right_argument_of H)} if H is Release

otherwise {} ;

coherence

( ( H is conjunctive implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is disjunctive implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) & ( H is next implies {} is Subset of (Subformulae H) ) & ( H is Until implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) & ( H is Release implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );

consistency

for b

( ( H is conjunctive & H is disjunctive implies ( b

by Lm11, Lm12, MODELC_2:78, SUBSET_1:1;

func LTLNew2 H -> Subset of (Subformulae H) equals :Def2: :: MODELC_3:def 2

{} if H is conjunctive

{(the_right_argument_of H)} if H is disjunctive

{} if H is next

{(the_right_argument_of H)} if H is Until

{(the_left_argument_of H),(the_right_argument_of H)} if H is Release

otherwise {} ;

correctness {} if H is conjunctive

{(the_right_argument_of H)} if H is disjunctive

{} if H is next

{(the_right_argument_of H)} if H is Until

{(the_left_argument_of H),(the_right_argument_of H)} if H is Release

otherwise {} ;

coherence

( ( H is conjunctive implies {} is Subset of (Subformulae H) ) & ( H is disjunctive implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is next implies {} is Subset of (Subformulae H) ) & ( H is Until implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is Release implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );

consistency

for b

( ( H is conjunctive & H is disjunctive implies ( b

by Lm11, Lm12, MODELC_2:78, SUBSET_1:1;

func LTLNext H -> Subset of (Subformulae H) equals :Def3: :: MODELC_3:def 3

{} if H is conjunctive

{} if H is disjunctive

{(the_argument_of H)} if H is next

{H} if H is Until

{H} if H is Release

otherwise {} ;

correctness {} if H is conjunctive

{} if H is disjunctive

{(the_argument_of H)} if H is next

{H} if H is Until

{H} if H is Release

otherwise {} ;

coherence

( ( H is conjunctive implies {} is Subset of (Subformulae H) ) & ( H is disjunctive implies {} is Subset of (Subformulae H) ) & ( H is next implies {(the_argument_of H)} is Subset of (Subformulae H) ) & ( H is Until implies {H} is Subset of (Subformulae H) ) & ( H is Release implies {H} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );

consistency

for b

( ( H is conjunctive & H is disjunctive implies ( b

by Lm13, Lm14, MODELC_2:78, SUBSET_1:1;

:: deftheorem Def1 defines LTLNew1 MODELC_3:def 1 :

for H being LTL-formula holds

( ( H is conjunctive implies LTLNew1 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( H is disjunctive implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is next implies LTLNew1 H = {} ) & ( H is Until implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is Release implies LTLNew1 H = {(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew1 H = {} ) );

for H being LTL-formula holds

( ( H is conjunctive implies LTLNew1 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( H is disjunctive implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is next implies LTLNew1 H = {} ) & ( H is Until implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is Release implies LTLNew1 H = {(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew1 H = {} ) );

:: deftheorem Def2 defines LTLNew2 MODELC_3:def 2 :

for H being LTL-formula holds

( ( H is conjunctive implies LTLNew2 H = {} ) & ( H is disjunctive implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is next implies LTLNew2 H = {} ) & ( H is Until implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is Release implies LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew2 H = {} ) );

for H being LTL-formula holds

( ( H is conjunctive implies LTLNew2 H = {} ) & ( H is disjunctive implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is next implies LTLNew2 H = {} ) & ( H is Until implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is Release implies LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew2 H = {} ) );

:: deftheorem Def3 defines LTLNext MODELC_3:def 3 :

for H being LTL-formula holds

( ( H is conjunctive implies LTLNext H = {} ) & ( H is disjunctive implies LTLNext H = {} ) & ( H is next implies LTLNext H = {(the_argument_of H)} ) & ( H is Until implies LTLNext H = {H} ) & ( H is Release implies LTLNext H = {H} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNext H = {} ) );

for H being LTL-formula holds

( ( H is conjunctive implies LTLNext H = {} ) & ( H is disjunctive implies LTLNext H = {} ) & ( H is next implies LTLNext H = {(the_argument_of H)} ) & ( H is Until implies LTLNext H = {H} ) & ( H is Release implies LTLNext H = {H} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNext H = {} ) );

definition

let v be LTL-formula;

attr c_{2} is strict ;

struct LTLnode over v -> ;

aggr LTLnode(# LTLold, LTLnew, LTLnext #) -> LTLnode over v;

sel LTLold c_{2} -> Subset of (Subformulae v);

sel LTLnew c_{2} -> Subset of (Subformulae v);

sel LTLnext c_{2} -> Subset of (Subformulae v);

end;
attr c

struct LTLnode over v -> ;

aggr LTLnode(# LTLold, LTLnew, LTLnext #) -> LTLnode over v;

sel LTLold c

sel LTLnew c

sel LTLnext c

definition

let v be LTL-formula;

let N be LTLnode over v;

let H be LTL-formula;

assume A1: H in the LTLnew of N ;

ex b_{1} being strict LTLnode over v st

( the LTLold of b_{1} = the LTLold of N \/ {H} & the LTLnew of b_{1} = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of b_{1} = the LTLnext of N \/ (LTLNext H) )

for b_{1}, b_{2} being strict LTLnode over v st the LTLold of b_{1} = the LTLold of N \/ {H} & the LTLnew of b_{1} = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of b_{1} = the LTLnext of N \/ (LTLNext H) & the LTLold of b_{2} = the LTLold of N \/ {H} & the LTLnew of b_{2} = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of b_{2} = the LTLnext of N \/ (LTLNext H) holds

b_{1} = b_{2}
;

end;
let N be LTLnode over v;

let H be LTL-formula;

assume A1: H in the LTLnew of N ;

func SuccNode1 (H,N) -> strict LTLnode over v means :Def4: :: MODELC_3:def 4

( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N \/ (LTLNext H) );

existence ( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N \/ (LTLNext H) );

ex b

( the LTLold of b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines SuccNode1 MODELC_3:def 4 :

for v being LTL-formula

for N being LTLnode over v

for H being LTL-formula st H in the LTLnew of N holds

for b_{4} being strict LTLnode over v holds

( b_{4} = SuccNode1 (H,N) iff ( the LTLold of b_{4} = the LTLold of N \/ {H} & the LTLnew of b_{4} = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of b_{4} = the LTLnext of N \/ (LTLNext H) ) );

for v being LTL-formula

for N being LTLnode over v

for H being LTL-formula st H in the LTLnew of N holds

for b

( b

definition

let v be LTL-formula;

let N be LTLnode over v;

let H be LTL-formula;

assume A1: H in the LTLnew of N ;

ex b_{1} being strict LTLnode over v st

( the LTLold of b_{1} = the LTLold of N \/ {H} & the LTLnew of b_{1} = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of b_{1} = the LTLnext of N )

for b_{1}, b_{2} being strict LTLnode over v st the LTLold of b_{1} = the LTLold of N \/ {H} & the LTLnew of b_{1} = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of b_{1} = the LTLnext of N & the LTLold of b_{2} = the LTLold of N \/ {H} & the LTLnew of b_{2} = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of b_{2} = the LTLnext of N holds

b_{1} = b_{2}
;

end;
let N be LTLnode over v;

let H be LTL-formula;

assume A1: H in the LTLnew of N ;

func SuccNode2 (H,N) -> strict LTLnode over v means :Def5: :: MODELC_3:def 5

( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N );

existence ( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N );

ex b

( the LTLold of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines SuccNode2 MODELC_3:def 5 :

for v being LTL-formula

for N being LTLnode over v

for H being LTL-formula st H in the LTLnew of N holds

for b_{4} being strict LTLnode over v holds

( b_{4} = SuccNode2 (H,N) iff ( the LTLold of b_{4} = the LTLold of N \/ {H} & the LTLnew of b_{4} = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of b_{4} = the LTLnext of N ) );

for v being LTL-formula

for N being LTLnode over v

for H being LTL-formula st H in the LTLnew of N holds

for b

( b

definition

let v be LTL-formula;

let N1, N2 be LTLnode over v;

let H be LTL-formula;

end;
let N1, N2 be LTLnode over v;

let H be LTL-formula;

pred N2 is_succ_of N1,H means :: MODELC_3:def 6

( H in the LTLnew of N1 & ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) ) );

( H in the LTLnew of N1 & ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) ) );

:: deftheorem defines is_succ_of MODELC_3:def 6 :

for v being LTL-formula

for N1, N2 being LTLnode over v

for H being LTL-formula holds

( N2 is_succ_of N1,H iff ( H in the LTLnew of N1 & ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) ) ) );

for v being LTL-formula

for N1, N2 being LTLnode over v

for H being LTL-formula holds

( N2 is_succ_of N1,H iff ( H in the LTLnew of N1 & ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) ) ) );

definition

let v be LTL-formula;

let N1, N2 be LTLnode over v;

end;
let N1, N2 be LTLnode over v;

pred N2 is_succ1_of N1 means :: MODELC_3:def 7

ex H being LTL-formula st

( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) );

ex H being LTL-formula st

( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) );

pred N2 is_succ2_of N1 means :: MODELC_3:def 8

ex H being LTL-formula st

( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) );

ex H being LTL-formula st

( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) );

:: deftheorem defines is_succ1_of MODELC_3:def 7 :

for v being LTL-formula

for N1, N2 being LTLnode over v holds

( N2 is_succ1_of N1 iff ex H being LTL-formula st

( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) ) );

for v being LTL-formula

for N1, N2 being LTLnode over v holds

( N2 is_succ1_of N1 iff ex H being LTL-formula st

( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) ) );

:: deftheorem defines is_succ2_of MODELC_3:def 8 :

for v being LTL-formula

for N1, N2 being LTLnode over v holds

( N2 is_succ2_of N1 iff ex H being LTL-formula st

( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) );

for v being LTL-formula

for N1, N2 being LTLnode over v holds

( N2 is_succ2_of N1 iff ex H being LTL-formula st

( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) );

:: deftheorem defines is_succ_of MODELC_3:def 9 :

for v being LTL-formula

for N1, N2 being LTLnode over v holds

( N2 is_succ_of N1 iff ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) );

for v being LTL-formula

for N1, N2 being LTLnode over v holds

( N2 is_succ_of N1 iff ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) );

:: deftheorem defines failure MODELC_3:def 10 :

for v being LTL-formula

for N being LTLnode over v holds

( N is failure iff ex H, F being LTL-formula st

( H is atomic & F = 'not' H & H in the LTLold of N & F in the LTLold of N ) );

for v being LTL-formula

for N being LTLnode over v holds

( N is failure iff ex H, F being LTL-formula st

( H is atomic & F = 'not' H & H in the LTLold of N & F in the LTLold of N ) );

:: deftheorem Def11 defines elementary MODELC_3:def 11 :

for v being LTL-formula

for N being LTLnode over v holds

( N is elementary iff the LTLnew of N = {} );

for v being LTL-formula

for N being LTLnode over v holds

( N is elementary iff the LTLnew of N = {} );

:: deftheorem defines final MODELC_3:def 12 :

for v being LTL-formula

for N being LTLnode over v holds

( N is final iff ( N is elementary & the LTLnext of N = {} ) );

for v being LTL-formula

for N being LTLnode over v holds

( N is final iff ( N is elementary & the LTLnext of N = {} ) );

definition
end;

definition
end;

registration

let v be LTL-formula;

existence

ex b_{1} being LTLnode over v st

( b_{1} is elementary & b_{1} is strict )

end;
existence

ex b

( b

proof end;

definition

let v be LTL-formula;

coherence

LTLnode(# ({} v),({} v),({} v) #) is strict elementary LTLnode over v;

by Def11;

end;
func FinalNode v -> strict elementary LTLnode over v equals :: MODELC_3:def 15

LTLnode(# ({} v),({} v),({} v) #);

correctness LTLnode(# ({} v),({} v),({} v) #);

coherence

LTLnode(# ({} v),({} v),({} v) #) is strict elementary LTLnode over v;

by Def11;

:: deftheorem defines FinalNode MODELC_3:def 15 :

for v being LTL-formula holds FinalNode v = LTLnode(# ({} v),({} v),({} v) #);

for v being LTL-formula holds FinalNode v = LTLnode(# ({} v),({} v),({} v) #);

definition

let x be object ;

let v be LTL-formula;

coherence

( ( x is strict LTLnode over v implies x is strict LTLnode over v ) & ( x is not strict LTLnode over v implies LTLnode(# ({} v),({} v),({} v) #) is strict LTLnode over v ) );

consistency

for b_{1} being strict LTLnode over v holds verum;

;

end;
let v be LTL-formula;

func CastNode (x,v) -> strict LTLnode over v equals :Def16: :: MODELC_3:def 16

x if x is strict LTLnode over v

otherwise LTLnode(# ({} v),({} v),({} v) #);

correctness x if x is strict LTLnode over v

otherwise LTLnode(# ({} v),({} v),({} v) #);

coherence

( ( x is strict LTLnode over v implies x is strict LTLnode over v ) & ( x is not strict LTLnode over v implies LTLnode(# ({} v),({} v),({} v) #) is strict LTLnode over v ) );

consistency

for b

;

:: deftheorem Def16 defines CastNode MODELC_3:def 16 :

for x being object

for v being LTL-formula holds

( ( x is strict LTLnode over v implies CastNode (x,v) = x ) & ( x is not strict LTLnode over v implies CastNode (x,v) = LTLnode(# ({} v),({} v),({} v) #) ) );

for x being object

for v being LTL-formula holds

( ( x is strict LTLnode over v implies CastNode (x,v) = x ) & ( x is not strict LTLnode over v implies CastNode (x,v) = LTLnode(# ({} v),({} v),({} v) #) ) );

definition

let v be LTL-formula;

coherence

LTLnode(# ({} v),({} v),(Seed v) #) is strict elementary LTLnode over v;

by Def11;

end;
func init v -> strict elementary LTLnode over v equals :: MODELC_3:def 17

LTLnode(# ({} v),({} v),(Seed v) #);

correctness LTLnode(# ({} v),({} v),(Seed v) #);

coherence

LTLnode(# ({} v),({} v),(Seed v) #) is strict elementary LTLnode over v;

by Def11;

:: deftheorem defines init MODELC_3:def 17 :

for v being LTL-formula holds init v = LTLnode(# ({} v),({} v),(Seed v) #);

for v being LTL-formula holds init v = LTLnode(# ({} v),({} v),(Seed v) #);

definition

let v be LTL-formula;

let N be LTLnode over v;

coherence

LTLnode(# ({} v), the LTLnext of N,({} v) #) is strict LTLnode over v;

;

end;
let N be LTLnode over v;

func 'X' N -> strict LTLnode over v equals :: MODELC_3:def 18

LTLnode(# ({} v), the LTLnext of N,({} v) #);

correctness LTLnode(# ({} v), the LTLnext of N,({} v) #);

coherence

LTLnode(# ({} v), the LTLnext of N,({} v) #) is strict LTLnode over v;

;

:: deftheorem defines 'X' MODELC_3:def 18 :

for v being LTL-formula

for N being LTLnode over v holds 'X' N = LTLnode(# ({} v), the LTLnext of N,({} v) #);

for v being LTL-formula

for N being LTLnode over v holds 'X' N = LTLnode(# ({} v), the LTLnext of N,({} v) #);

definition

let v be LTL-formula;

let L be FinSequence;

end;
let L be FinSequence;

pred L is_Finseq_for v means :: MODELC_3:def 19

for k being Nat st 1 <= k & k < len L holds

ex N, M being strict LTLnode over v st

( N = L . k & M = L . (k + 1) & M is_succ_of N );

for k being Nat st 1 <= k & k < len L holds

ex N, M being strict LTLnode over v st

( N = L . k & M = L . (k + 1) & M is_succ_of N );

:: deftheorem defines is_Finseq_for MODELC_3:def 19 :

for v being LTL-formula

for L being FinSequence holds

( L is_Finseq_for v iff for k being Nat st 1 <= k & k < len L holds

ex N, M being strict LTLnode over v st

( N = L . k & M = L . (k + 1) & M is_succ_of N ) );

for v being LTL-formula

for L being FinSequence holds

( L is_Finseq_for v iff for k being Nat st 1 <= k & k < len L holds

ex N, M being strict LTLnode over v st

( N = L . k & M = L . (k + 1) & M is_succ_of N ) );

Lm15: for m being Nat

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L holds

ex L1, L2 being FinSequence st

( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) )

proof end;

definition

let v be LTL-formula;

let N1, N2 be strict LTLnode over v;

end;
let N1, N2 be strict LTLnode over v;

pred N2 is_next_of N1 means :: MODELC_3:def 20

( N1 is elementary & N2 is elementary & ex L being FinSequence st

( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' N1 & L . (len L) = N2 ) );

( N1 is elementary & N2 is elementary & ex L being FinSequence st

( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' N1 & L . (len L) = N2 ) );

:: deftheorem defines is_next_of MODELC_3:def 20 :

for v being LTL-formula

for N1, N2 being strict LTLnode over v holds

( N2 is_next_of N1 iff ( N1 is elementary & N2 is elementary & ex L being FinSequence st

( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' N1 & L . (len L) = N2 ) ) );

for v being LTL-formula

for N1, N2 being strict LTLnode over v holds

( N2 is_next_of N1 iff ( N1 is elementary & N2 is elementary & ex L being FinSequence st

( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' N1 & L . (len L) = N2 ) ) );

definition

let v be LTL-formula;

let W be Subset of (Subformulae v);

correctness

coherence

W is Subset of LTL_WFF;

by MODELC_2:47;

end;
let W be Subset of (Subformulae v);

correctness

coherence

W is Subset of LTL_WFF;

by MODELC_2:47;

:: deftheorem defines CastLTL MODELC_3:def 21 :

for v being LTL-formula

for W being Subset of (Subformulae v) holds CastLTL W = W;

for v being LTL-formula

for W being Subset of (Subformulae v) holds CastLTL W = W;

definition

let v be LTL-formula;

let N be strict LTLnode over v;

coherence

( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) is Subset of LTL_WFF;

end;
let N be strict LTLnode over v;

func * N -> Subset of LTL_WFF equals :: MODELC_3:def 22

( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N));

correctness ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N));

coherence

( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) is Subset of LTL_WFF;

proof end;

:: deftheorem defines * MODELC_3:def 22 :

for v being LTL-formula

for N being strict LTLnode over v holds * N = ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N));

for v being LTL-formula

for N being strict LTLnode over v holds * N = ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N));

Lm16: for H, v being LTL-formula

for N being strict LTLnode over v st H in the LTLnew of N & ( H is atomic or H is negative ) holds

* N = * (SuccNode1 (H,N))

proof end;

Lm17: for H, v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & ( H is conjunctive or H is next ) holds

( w |= * N iff w |= * (SuccNode1 (H,N)) )

proof end;

theorem :: MODELC_3:1

Lm18: for H, v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is disjunctive holds

( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )

proof end;

Lm19: for H, v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is Until holds

( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )

proof end;

Lm20: for H, v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is Release holds

( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )

proof end;

theorem :: MODELC_3:2

Lm21: for H being LTL-formula st ( H is negative or H is next ) holds

Subformulae H = (Subformulae (the_argument_of H)) \/ {H}

proof end;

Lm22: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

proof end;

Lm23: for H being LTL-formula st H is atomic holds

Subformulae H = {H}

proof end;

Lm24: for H being LTL-formula

for W being Subset of (Subformulae H) holds not {} in W

proof end;

definition

let H be LTL-formula;

let W be Subset of (Subformulae H);

let L be FinSequence;

let x be set ;

coherence

( ( L . x in W implies len (CastLTL (L . x)) is Nat ) & ( not L . x in W implies 0 is Nat ) );

consistency

for b_{1} being Nat holds verum;

;

end;
let W be Subset of (Subformulae H);

let L be FinSequence;

let x be set ;

func Length_fun (L,W,x) -> Nat equals :Def23: :: MODELC_3:def 23

len (CastLTL (L . x)) if L . x in W

otherwise 0 ;

correctness len (CastLTL (L . x)) if L . x in W

otherwise 0 ;

coherence

( ( L . x in W implies len (CastLTL (L . x)) is Nat ) & ( not L . x in W implies 0 is Nat ) );

consistency

for b

;

:: deftheorem Def23 defines Length_fun MODELC_3:def 23 :

for H being LTL-formula

for W being Subset of (Subformulae H)

for L being FinSequence

for x being set holds

( ( L . x in W implies Length_fun (L,W,x) = len (CastLTL (L . x)) ) & ( not L . x in W implies Length_fun (L,W,x) = 0 ) );

for H being LTL-formula

for W being Subset of (Subformulae H)

for L being FinSequence

for x being set holds

( ( L . x in W implies Length_fun (L,W,x) = len (CastLTL (L . x)) ) & ( not L . x in W implies Length_fun (L,W,x) = 0 ) );

definition

let H be LTL-formula;

let W be Subset of (Subformulae H);

let L be FinSequence;

ex b_{1} being Real_Sequence st

for k being Nat holds

( ( L . k in W implies b_{1} . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Real_Sequence st ( for k being Nat holds

( ( L . k in W implies b_{1} . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( L . k in W implies b_{2} . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
let W be Subset of (Subformulae H);

let L be FinSequence;

func Partial_seq (L,W) -> Real_Sequence means :Def24: :: MODELC_3:def 24

for k being Nat holds

( ( L . k in W implies it . k = len (CastLTL (L . k)) ) & ( not L . k in W implies it . k = 0 ) );

existence for k being Nat holds

( ( L . k in W implies it . k = len (CastLTL (L . k)) ) & ( not L . k in W implies it . k = 0 ) );

ex b

for k being Nat holds

( ( L . k in W implies b

proof end;

uniqueness for b

( ( L . k in W implies b

( ( L . k in W implies b

b

proof end;

:: deftheorem Def24 defines Partial_seq MODELC_3:def 24 :

for H being LTL-formula

for W being Subset of (Subformulae H)

for L being FinSequence

for b_{4} being Real_Sequence holds

( b_{4} = Partial_seq (L,W) iff for k being Nat holds

( ( L . k in W implies b_{4} . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b_{4} . k = 0 ) ) );

for H being LTL-formula

for W being Subset of (Subformulae H)

for L being FinSequence

for b

( b

( ( L . k in W implies b

definition

let H be LTL-formula;

let W be Subset of (Subformulae H);

let L be FinSequence;

correctness

coherence

Sum ((Partial_seq (L,W)),(len L)) is Real;

;

end;
let W be Subset of (Subformulae H);

let L be FinSequence;

correctness

coherence

Sum ((Partial_seq (L,W)),(len L)) is Real;

;

:: deftheorem defines len MODELC_3:def 25 :

for H being LTL-formula

for W being Subset of (Subformulae H)

for L being FinSequence holds len (L,W) = Sum ((Partial_seq (L,W)),(len L));

for H being LTL-formula

for W being Subset of (Subformulae H)

for L being FinSequence holds len (L,W) = Sum ((Partial_seq (L,W)),(len L));

Lm25: for n being Nat

for R1, R2 being Real_Sequence st ( for i being Nat st i <= n holds

R1 . i = R2 . i ) holds

Sum (R1,n) = Sum (R2,n)

proof end;

Lm26: for n, j being Nat

for R1, R2 being Real_Sequence st ( for i being Nat st i <= n & not i = j holds

R1 . i = R2 . i ) & j <= n holds

(Sum (R1,n)) - (R1 . j) = (Sum (R2,n)) - (R2 . j)

proof end;

theorem Th5: :: MODELC_3:5

for L being FinSequence

for F, H being LTL-formula

for W being Subset of (Subformulae H) st not F in W holds

len (L,(W \ {F})) = len (L,W)

for F, H being LTL-formula

for W being Subset of (Subformulae H) st not F in W holds

len (L,(W \ {F})) = len (L,W)

proof end;

theorem Th6: :: MODELC_3:6

for L being FinSequence

for F, H being LTL-formula

for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds

len (L,(W \ {F})) = (len (L,W)) - (len F)

for F, H being LTL-formula

for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds

len (L,(W \ {F})) = (len (L,W)) - (len F)

proof end;

theorem Th7: :: MODELC_3:7

for L being FinSequence

for F, H being LTL-formula

for W, W1 being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & not F in W & W1 = W \/ {F} holds

len (L,W1) = (len (L,W)) + (len F)

for F, H being LTL-formula

for W, W1 being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & not F in W & W1 = W \/ {F} holds

len (L,W1) = (len (L,W)) + (len F)

proof end;

theorem Th8: :: MODELC_3:8

for L1, L2 being FinSequence

for H being LTL-formula

for W being Subset of (Subformulae H) st rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one holds

len (L1,W) = len (L2,W)

for H being LTL-formula

for W being Subset of (Subformulae H) st rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one holds

len (L1,W) = len (L2,W)

proof end;

definition

let H be LTL-formula;

let W be Subset of (Subformulae H);

ex b_{1} being Real ex L being FinSequence st

( rng L = Subformulae H & L is one-to-one & b_{1} = len (L,W) )

for b_{1}, b_{2} being Real st ex L being FinSequence st

( rng L = Subformulae H & L is one-to-one & b_{1} = len (L,W) ) & ex L being FinSequence st

( rng L = Subformulae H & L is one-to-one & b_{2} = len (L,W) ) holds

b_{1} = b_{2}
by Th8;

end;
let W be Subset of (Subformulae H);

func len W -> Real means :Def26: :: MODELC_3:def 26

ex L being FinSequence st

( rng L = Subformulae H & L is one-to-one & it = len (L,W) );

existence ex L being FinSequence st

( rng L = Subformulae H & L is one-to-one & it = len (L,W) );

ex b

( rng L = Subformulae H & L is one-to-one & b

proof end;

uniqueness for b

( rng L = Subformulae H & L is one-to-one & b

( rng L = Subformulae H & L is one-to-one & b

b

:: deftheorem Def26 defines len MODELC_3:def 26 :

for H being LTL-formula

for W being Subset of (Subformulae H)

for b_{3} being Real holds

( b_{3} = len W iff ex L being FinSequence st

( rng L = Subformulae H & L is one-to-one & b_{3} = len (L,W) ) );

for H being LTL-formula

for W being Subset of (Subformulae H)

for b

( b

( rng L = Subformulae H & L is one-to-one & b

theorem :: MODELC_3:9

for F, H being LTL-formula

for W being Subset of (Subformulae H) st not F in W holds

len (W \ {F}) = len W

for W being Subset of (Subformulae H) st not F in W holds

len (W \ {F}) = len W

proof end;

theorem Th10: :: MODELC_3:10

for F, H being LTL-formula

for W being Subset of (Subformulae H) st F in W holds

len (W \ {F}) = (len W) - (len F)

for W being Subset of (Subformulae H) st F in W holds

len (W \ {F}) = (len W) - (len F)

proof end;

theorem Th11: :: MODELC_3:11

for F, H being LTL-formula

for W, W1 being Subset of (Subformulae H) st not F in W & W1 = W \/ {F} holds

len W1 = (len W) + (len F)

for W, W1 being Subset of (Subformulae H) st not F in W & W1 = W \/ {F} holds

len W1 = (len W) + (len F)

proof end;

theorem Th12: :: MODELC_3:12

for F, H being LTL-formula

for W, W1 being Subset of (Subformulae H) st W1 = W \/ {F} holds

len W1 <= (len W) + (len F)

for W, W1 being Subset of (Subformulae H) st W1 = W \/ {F} holds

len W1 <= (len W) + (len F)

proof end;

theorem Th18: :: MODELC_3:18

for H being LTL-formula

for W, W1, W2 being Subset of (Subformulae H) st W = W1 \/ W2 holds

len W <= (len W1) + (len W2)

for W, W1, W2 being Subset of (Subformulae H) st W = W1 \/ W2 holds

len W <= (len W1) + (len W2)

proof end;

definition

let v, H be LTL-formula;

assume A1: H in Subformulae v ;

correctness

coherence

LTLNew1 H is Subset of (Subformulae v);

coherence

LTLNew2 H is Subset of (Subformulae v);

end;
assume A1: H in Subformulae v ;

correctness

coherence

LTLNew1 H is Subset of (Subformulae v);

proof end;

correctness coherence

LTLNew2 H is Subset of (Subformulae v);

proof end;

:: deftheorem Def27 defines LTLNew1 MODELC_3:def 27 :

for v, H being LTL-formula st H in Subformulae v holds

LTLNew1 (H,v) = LTLNew1 H;

for v, H being LTL-formula st H in Subformulae v holds

LTLNew1 (H,v) = LTLNew1 H;

:: deftheorem Def28 defines LTLNew2 MODELC_3:def 28 :

for v, H being LTL-formula st H in Subformulae v holds

LTLNew2 (H,v) = LTLNew2 H;

for v, H being LTL-formula st H in Subformulae v holds

LTLNew2 (H,v) = LTLNew2 H;

Lm27: for H, v being LTL-formula st H in Subformulae v holds

len (LTLNew1 (H,v)) <= (len H) - 1

proof end;

Lm28: for H, v being LTL-formula st H in Subformulae v holds

len (LTLNew2 (H,v)) <= (len H) - 1

proof end;

theorem Th19: :: MODELC_3:19

for v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ1_of N1 holds

len the LTLnew of N2 <= (len the LTLnew of N1) - 1

for N1, N2 being strict LTLnode over v st N2 is_succ1_of N1 holds

len the LTLnew of N2 <= (len the LTLnew of N1) - 1

proof end;

theorem Th20: :: MODELC_3:20

for v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ2_of N1 holds

len the LTLnew of N2 <= (len the LTLnew of N1) - 1

for N1, N2 being strict LTLnode over v st N2 is_succ2_of N1 holds

len the LTLnew of N2 <= (len the LTLnew of N1) - 1

proof end;

definition

let v be LTL-formula;

let N be strict LTLnode over v;

correctness

coherence

[\(len the LTLnew of N)/] is Nat;

end;
let N be strict LTLnode over v;

correctness

coherence

[\(len the LTLnew of N)/] is Nat;

proof end;

:: deftheorem defines len MODELC_3:def 29 :

for v being LTL-formula

for N being strict LTLnode over v holds len N = [\(len the LTLnew of N)/];

for v being LTL-formula

for N being strict LTLnode over v holds len N = [\(len the LTLnew of N)/];

theorem Th21: :: MODELC_3:21

for v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds

len N2 <= (len N1) - 1

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds

len N2 <= (len N1) - 1

proof end;

theorem Th22: :: MODELC_3:22

for v being LTL-formula

for N being strict LTLnode over v st len N <= 0 holds

the LTLnew of N = {} v

for N being strict LTLnode over v st len N <= 0 holds

the LTLnew of N = {} v

proof end;

theorem Th23: :: MODELC_3:23

for v being LTL-formula

for N being strict LTLnode over v st len N > 0 holds

the LTLnew of N <> {} v

for N being strict LTLnode over v st len N > 0 holds

the LTLnew of N <> {} v

proof end;

theorem :: MODELC_3:24

for v being LTL-formula

for N being strict LTLnode over v ex n being Nat ex L being FinSequence ex M being strict LTLnode over v st

( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )

for N being strict LTLnode over v ex n being Nat ex L being FinSequence ex M being strict LTLnode over v st

( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )

proof end;

theorem Th25: :: MODELC_3:25

for v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds

( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds

( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )

proof end;

theorem Th26: :: MODELC_3:26

for m being Nat

for L, L1 being FinSequence

for v being LTL-formula st L is_Finseq_for v & m <= len L & L1 = L | (Seg m) holds

L1 is_Finseq_for v

for L, L1 being FinSequence

for v being LTL-formula st L is_Finseq_for v & m <= len L & L1 = L | (Seg m) holds

L1 is_Finseq_for v

proof end;

theorem Th27: :: MODELC_3:27

for n being Nat

for L being FinSequence

for F, v being LTL-formula st L is_Finseq_for v & not F in the LTLold of (CastNode ((L . 1),v)) & 1 < n & n <= len L & F in the LTLold of (CastNode ((L . n),v)) holds

ex m being Nat st

( 1 <= m & m < n & not F in the LTLold of (CastNode ((L . m),v)) & F in the LTLold of (CastNode ((L . (m + 1)),v)) )

for L being FinSequence

for F, v being LTL-formula st L is_Finseq_for v & not F in the LTLold of (CastNode ((L . 1),v)) & 1 < n & n <= len L & F in the LTLold of (CastNode ((L . n),v)) holds

ex m being Nat st

( 1 <= m & m < n & not F in the LTLold of (CastNode ((L . m),v)) & F in the LTLold of (CastNode ((L . (m + 1)),v)) )

proof end;

theorem Th28: :: MODELC_3:28

for F, v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 & not F in the LTLold of N1 & F in the LTLold of N2 holds

N2 is_succ_of N1,F

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 & not F in the LTLold of N1 & F in the LTLold of N2 holds

N2 is_succ_of N1,F

proof end;

theorem Th29: :: MODELC_3:29

for n being Nat

for L being FinSequence

for F, v being LTL-formula st L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) holds

ex m being Nat st

( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )

for L being FinSequence

for F, v being LTL-formula st L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) holds

ex m being Nat st

( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )

proof end;

theorem Th30: :: MODELC_3:30

for F, v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 & F in the LTLnew of N1 & not F in the LTLnew of N2 holds

N2 is_succ_of N1,F

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 & F in the LTLnew of N1 & not F in the LTLnew of N2 holds

N2 is_succ_of N1,F

proof end;

theorem Th31: :: MODELC_3:31

for n, m being Nat

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= n & n <= len L holds

( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) )

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= n & n <= len L holds

( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) )

proof end;

theorem Th32: :: MODELC_3:32

for F, v being LTL-formula

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1,F holds

F in the LTLold of N2

for N1, N2 being strict LTLnode over v st N2 is_succ_of N1,F holds

F in the LTLold of N2

proof end;

theorem Th33: :: MODELC_3:33

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds

the LTLnew of (CastNode ((L . 1),v)) c= the LTLold of (CastNode ((L . (len L)),v))

for v being LTL-formula st L is_Finseq_for v & 1 <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds

the LTLnew of (CastNode ((L . 1),v)) c= the LTLold of (CastNode ((L . (len L)),v))

proof end;

theorem Th34: :: MODELC_3:34

for m being Nat

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds

the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v))

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds

the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v))

proof end;

theorem Th35: :: MODELC_3:35

for k being Nat

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds

CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds

CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)

proof end;

theorem Th36: :: MODELC_3:36

for k being Nat

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= k & k <= len L holds

len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

for L being FinSequence

for v being LTL-formula st L is_Finseq_for v & 1 <= k & k <= len L holds

len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

proof end;

theorem Th37: :: MODELC_3:37

for v being LTL-formula

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 holds

the LTLnext of s1 c= the LTLold of s2

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 holds

the LTLnext of s1 c= the LTLold of s2

proof end;

theorem Th38: :: MODELC_3:38

for F, v being LTL-formula

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & F in the LTLold of s2 holds

ex L being FinSequence ex m being Nat st

( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 & 1 <= m & m < len L & CastNode ((L . (m + 1)),v) is_succ_of CastNode ((L . m),v),F )

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & F in the LTLold of s2 holds

ex L being FinSequence ex m being Nat st

( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 & 1 <= m & m < len L & CastNode ((L . (m + 1)),v) is_succ_of CastNode ((L . m),v),F )

proof end;

theorem Th39: :: MODELC_3:39

for H, v being LTL-formula

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & H is Release & H in the LTLold of s2 & not the_left_argument_of H in the LTLold of s2 holds

( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 )

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & H is Release & H in the LTLold of s2 & not the_left_argument_of H in the LTLold of s2 holds

( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 )

proof end;

theorem Th40: :: MODELC_3:40

for H, v being LTL-formula

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & H is Release & H in the LTLnext of s1 holds

( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 )

for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & H is Release & H in the LTLnext of s1 holds

( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 )

proof end;

theorem Th41: :: MODELC_3:41

for H, v being LTL-formula

for s0, s1 being strict elementary LTLnode over v st s1 is_next_of s0 & H in the LTLold of s1 holds

( ( H is conjunctive implies ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) ) & ( ( not H is disjunctive & not H is Until ) or the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) & ( H is next implies the_argument_of H in the LTLnext of s1 ) & ( H is Release implies the_right_argument_of H in the LTLold of s1 ) )

for s0, s1 being strict elementary LTLnode over v st s1 is_next_of s0 & H in the LTLold of s1 holds

( ( H is conjunctive implies ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) ) & ( ( not H is disjunctive & not H is Until ) or the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) & ( H is next implies the_argument_of H in the LTLnext of s1 ) & ( H is Release implies the_right_argument_of H in the LTLold of s1 ) )

proof end;

Lm29: for F, G, v being LTL-formula

for s0, s1, s2 being strict elementary LTLnode over v st s1 is_next_of s0 & s2 is_next_of s1 & F 'U' G in the LTLold of s1 & not G in the LTLold of s1 holds

( F in the LTLold of s1 & F 'U' G in the LTLold of s2 )

proof end;

theorem :: MODELC_3:42

for H, v being LTL-formula

for s0, s1, s2 being strict elementary LTLnode over v st s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 & H is Until & not the_right_argument_of H in the LTLold of s1 holds

( the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2 )

for s0, s1, s2 being strict elementary LTLnode over v st s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 & H is Until & not the_right_argument_of H in the LTLold of s1 holds

( the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2 )

proof end;

definition

let v be LTL-formula;

ex b_{1} being non empty set st

for x being object holds

( x in b_{1} iff ex N being strict LTLnode over v st x = N )

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

( x in b_{1} iff ex N being strict LTLnode over v st x = N ) ) & ( for x being object holds

( x in b_{2} iff ex N being strict LTLnode over v st x = N ) ) holds

b_{1} = b_{2}

end;
func LTLNodes v -> non empty set means :Def30: :: MODELC_3:def 30

for x being object holds

( x in it iff ex N being strict LTLnode over v st x = N );

existence for x being object holds

( x in it iff ex N being strict LTLnode over v st x = N );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def30 defines LTLNodes MODELC_3:def 30 :

for v being LTL-formula

for b_{2} being non empty set holds

( b_{2} = LTLNodes v iff for x being object holds

( x in b_{2} iff ex N being strict LTLnode over v st x = N ) );

for v being LTL-formula

for b

( b

( x in b

definition

let v be LTL-formula;

{ x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } is non empty set

end;
func LTLStates v -> non empty set equals :: MODELC_3:def 31

{ x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;

coherence { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;

{ x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } is non empty set

proof end;

:: deftheorem defines LTLStates MODELC_3:def 31 :

for v being LTL-formula holds LTLStates v = { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;

for v being LTL-formula holds LTLStates v = { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;

theorem Th44: :: MODELC_3:44

for v being LTL-formula

for s being strict elementary LTLnode over v holds s is Element of LTLStates v

for s being strict elementary LTLnode over v holds s is Element of LTLStates v

proof end;

theorem Th45: :: MODELC_3:45

for x being set

for v being LTL-formula holds

( x is Element of LTLStates v iff ex s being strict elementary LTLnode over v st s = x )

for v being LTL-formula holds

( x is Element of LTLStates v iff ex s being strict elementary LTLnode over v st s = x )

proof end;

Lm30: for n being Nat

for X being set st X <> {} & X c= Seg n holds

ex k being Nat st

( 1 <= k & k <= n & k in X & ( for i being Nat st 1 <= i & i < k holds

not i in X ) )

proof end;

definition

let v be LTL-formula;

let w be Element of Inf_seq AtomicFamily;

let f be Function;

end;
let w be Element of Inf_seq AtomicFamily;

let f be Function;

pred f is_succ_homomorphism v,w means :: MODELC_3:def 32

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

( CastNode ((f . x),v) is_succ_of CastNode (x,v) & w |= * (CastNode ((f . x),v)) );

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

( CastNode ((f . x),v) is_succ_of CastNode (x,v) & w |= * (CastNode ((f . x),v)) );

pred f is_homomorphism v,w means :: MODELC_3:def 33

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

w |= * (CastNode ((f . x),v));

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

w |= * (CastNode ((f . x),v));

:: deftheorem defines is_succ_homomorphism MODELC_3:def 32 :

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function holds

( f is_succ_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

( CastNode ((f . x),v) is_succ_of CastNode (x,v) & w |= * (CastNode ((f . x),v)) ) );

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function holds

( f is_succ_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

( CastNode ((f . x),v) is_succ_of CastNode (x,v) & w |= * (CastNode ((f . x),v)) ) );

:: deftheorem defines is_homomorphism MODELC_3:def 33 :

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function holds

( f is_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

w |= * (CastNode ((f . x),v)) );

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function holds

( f is_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

w |= * (CastNode ((f . x),v)) );

theorem :: MODELC_3:46

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

f is_homomorphism v,w ;

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

f is_homomorphism v,w ;

theorem Th47: :: MODELC_3:47

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

for k being Nat st ( for i being Nat st i <= k holds

not CastNode (((f |** i) . x),v) is elementary ) holds

w |= * (CastNode (((f |** k) . x),v))

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

for k being Nat st ( for i being Nat st i <= k holds

not CastNode (((f |** i) . x),v) is elementary ) holds

w |= * (CastNode (((f |** k) . x),v))

proof end;

theorem Th48: :: MODELC_3:48

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

for k being Nat st ( for i being Nat st i <= k holds

not CastNode (((f |** i) . x),v) is elementary ) holds

( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

for k being Nat st ( for i being Nat st i <= k holds

not CastNode (((f |** i) . x),v) is elementary ) holds

( CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) & w |= * (CastNode (((f |** k) . x),v)) )

proof end;

theorem Th49: :: MODELC_3:49

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

ex n being Nat st

( ( for i being Nat st i < n holds

not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

ex n being Nat st

( ( for i being Nat st i < n holds

not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )

proof end;

theorem Th50: :: MODELC_3:50

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary holds

for k being Nat st not CastNode (((f |** k) . x),v) is elementary & w |= * (CastNode (((f |** k) . x),v)) holds

w |= * (CastNode (((f |** (k + 1)) . x),v))

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary holds

for k being Nat st not CastNode (((f |** k) . x),v) is elementary & w |= * (CastNode (((f |** k) . x),v)) holds

w |= * (CastNode (((f |** (k + 1)) . x),v))

proof end;

theorem Th51: :: MODELC_3:51

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

ex n being Nat st

( ( for i being Nat st i < n holds

( not CastNode (((f |** i) . x),v) is elementary & CastNode (((f |** (i + 1)) . x),v) is_succ_of CastNode (((f |** i) . x),v) ) ) & CastNode (((f |** n) . x),v) is elementary & ( for i being Nat st i <= n holds

w |= * (CastNode (((f |** i) . x),v)) ) )

for w being Element of Inf_seq AtomicFamily

for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds

for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds

ex n being Nat st

( ( for i being Nat st i < n holds

( not CastNode (((f |** i) . x),v) is elementary & CastNode (((f |** (i + 1)) . x),v) is_succ_of CastNode (((f |** i) . x),v) ) ) & CastNode (((f |** n) . x),v) is elementary & ( for i being Nat st i <= n holds

w |= * (CastNode (((f |** i) . x),v)) ) )

proof end;

theorem Th52: :: MODELC_3:52

for n being Nat

for v being LTL-formula

for q being sequence of (LTLStates v) ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v)

for v being LTL-formula

for q being sequence of (LTLStates v) ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v)

proof end;

Lm31: for n being Nat

for F, G, v being LTL-formula

for q being sequence of (LTLStates v) st F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ( for i being Nat st 1 <= i & i < n holds

not G in the LTLold of (CastNode ((q . i),v)) ) holds

for i being Nat st 1 <= i & i < n holds

( F in the LTLold of (CastNode ((q . i),v)) & F 'U' G in the LTLold of (CastNode ((q . i),v)) )

proof end;

theorem :: MODELC_3:53

for n being Nat

for H, v being LTL-formula

for q being sequence of (LTLStates v) st H is Until & H in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ( for i being Nat st 1 <= i & i < n holds

not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) holds

for i being Nat st 1 <= i & i < n holds

( the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & H in the LTLold of (CastNode ((q . i),v)) )

for H, v being LTL-formula

for q being sequence of (LTLStates v) st H is Until & H in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ( for i being Nat st 1 <= i & i < n holds

not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) holds

for i being Nat st 1 <= i & i < n holds

( the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & H in the LTLold of (CastNode ((q . i),v)) )

proof end;

Lm32: for F, G, v being LTL-formula

for q being sequence of (LTLStates v) st F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ex i being Nat st

( i >= 1 & not ( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) & not G in the LTLold of (CastNode ((q . i),v)) ) ) holds

ex j being Nat st

( j >= 1 & G in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds

( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) ) ) )

proof end;

theorem Th54: :: MODELC_3:54

for H, v being LTL-formula

for q being sequence of (LTLStates v) st H is Until & H in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ex i being Nat st

( i >= 1 & not ( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) holds

ex j being Nat st

( j >= 1 & the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds

( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) )

for q being sequence of (LTLStates v) st H is Until & H in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ex i being Nat st

( i >= 1 & not ( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) holds

ex j being Nat st

( j >= 1 & the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds

( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) )

proof end;

::some properties for choice function

theorem Th56: :: MODELC_3:56

for v being LTL-formula

for N being strict LTLnode over v st not N is elementary holds

( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) ) by ORDERS_1:2;

for N being strict LTLnode over v st not N is elementary holds

( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) ) by ORDERS_1:2;

registration

let v be LTL-formula;

correctness

coherence

not union (BOOL (Subformulae v)) is empty ;

by Th55;

correctness

coherence

not BOOL (Subformulae v) is empty ;

;

end;
correctness

coherence

not union (BOOL (Subformulae v)) is empty ;

by Th55;

correctness

coherence

not BOOL (Subformulae v) is empty ;

;

theorem :: MODELC_3:57

for v being LTL-formula ex f being Choice_Function of (BOOL (Subformulae v)) st f is Function of (BOOL (Subformulae v)),(Subformulae v)

proof end;

definition

let v be LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

assume A1: not N is elementary ;

correctness

coherence

U . the LTLnew of N is LTL-formula;

end;
let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

assume A1: not N is elementary ;

correctness

coherence

U . the LTLnew of N is LTL-formula;

proof end;

:: deftheorem Def34 defines chosen_formula MODELC_3:def 34 :

for v being LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v st not N is elementary holds

chosen_formula (U,N) = U . the LTLnew of N;

for v being LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v st not N is elementary holds

chosen_formula (U,N) = U . the LTLnew of N;

theorem Th58: :: MODELC_3:58

for v being LTL-formula

for N being strict LTLnode over v

for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary holds

chosen_formula (U,N) in the LTLnew of N

for N being strict LTLnode over v

for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary holds

chosen_formula (U,N) in the LTLnew of N

proof end;

definition

let w be Element of Inf_seq AtomicFamily;

let v be LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

coherence

( ( ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies SuccNode1 ((chosen_formula (U,N)),N) is strict LTLnode over v ) & ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) or SuccNode2 ((chosen_formula (U,N)),N) is strict LTLnode over v ) );

consistency

for b_{1} being strict LTLnode over v holds verum;

;

end;
let v be LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

func chosen_succ (w,v,U,N) -> strict LTLnode over v equals :Def35: :: MODELC_3:def 35

SuccNode1 ((chosen_formula (U,N)),N) if ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) )

otherwise SuccNode2 ((chosen_formula (U,N)),N);

correctness SuccNode1 ((chosen_formula (U,N)),N) if ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) )

otherwise SuccNode2 ((chosen_formula (U,N)),N);

coherence

( ( ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies SuccNode1 ((chosen_formula (U,N)),N) is strict LTLnode over v ) & ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) or SuccNode2 ((chosen_formula (U,N)),N) is strict LTLnode over v ) );

consistency

for b

;

:: deftheorem Def35 defines chosen_succ MODELC_3:def 35 :

for w being Element of Inf_seq AtomicFamily

for v being LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v holds

( ( ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies chosen_succ (w,v,U,N) = SuccNode1 ((chosen_formula (U,N)),N) ) & ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) or chosen_succ (w,v,U,N) = SuccNode2 ((chosen_formula (U,N)),N) ) );

for w being Element of Inf_seq AtomicFamily

for v being LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v holds

( ( ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies chosen_succ (w,v,U,N) = SuccNode1 ((chosen_formula (U,N)),N) ) & ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) or chosen_succ (w,v,U,N) = SuccNode2 ((chosen_formula (U,N)),N) ) );

theorem Th59: :: MODELC_3:59

for v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds

( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds

( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )

proof end;

theorem :: MODELC_3:60

for v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary & chosen_formula (U,N) is Until & w |= the_right_argument_of (chosen_formula (U,N)) holds

( ( the_right_argument_of (chosen_formula (U,N)) in the LTLnew of (chosen_succ (w,v,U,N)) or the_right_argument_of (chosen_formula (U,N)) in the LTLold of N ) & chosen_formula (U,N) in the LTLold of (chosen_succ (w,v,U,N)) )

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary & chosen_formula (U,N) is Until & w |= the_right_argument_of (chosen_formula (U,N)) holds

( ( the_right_argument_of (chosen_formula (U,N)) in the LTLnew of (chosen_succ (w,v,U,N)) or the_right_argument_of (chosen_formula (U,N)) in the LTLold of N ) & chosen_formula (U,N) in the LTLold of (chosen_succ (w,v,U,N)) )

proof end;

theorem :: MODELC_3:61

for v being LTL-formula

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds

( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )

for N being strict LTLnode over v

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds

( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )

proof end;

definition

let w be Element of Inf_seq AtomicFamily;

let v be LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

ex b_{1} being Function of (LTLNodes v),(LTLNodes v) st

for x being set st x in LTLNodes v holds

b_{1} . x = chosen_succ (w,v,U,(CastNode (x,v)))

for b_{1}, b_{2} being Function of (LTLNodes v),(LTLNodes v) st ( for x being set st x in LTLNodes v holds

b_{1} . x = chosen_succ (w,v,U,(CastNode (x,v))) ) & ( for x being set st x in LTLNodes v holds

b_{2} . x = chosen_succ (w,v,U,(CastNode (x,v))) ) holds

b_{1} = b_{2}

end;
let v be LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

func choice_succ_func (w,v,U) -> Function of (LTLNodes v),(LTLNodes v) means :Def36: :: MODELC_3:def 36

for x being set st x in LTLNodes v holds

it . x = chosen_succ (w,v,U,(CastNode (x,v)));

existence for x being set st x in LTLNodes v holds

it . x = chosen_succ (w,v,U,(CastNode (x,v)));

ex b

for x being set st x in LTLNodes v holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def36 defines choice_succ_func MODELC_3:def 36 :

for w being Element of Inf_seq AtomicFamily

for v being LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for b_{4} being Function of (LTLNodes v),(LTLNodes v) holds

( b_{4} = choice_succ_func (w,v,U) iff for x being set st x in LTLNodes v holds

b_{4} . x = chosen_succ (w,v,U,(CastNode (x,v))) );

for w being Element of Inf_seq AtomicFamily

for v being LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for b

( b

b

theorem Th62: :: MODELC_3:62

for v being LTL-formula

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) holds choice_succ_func (w,v,U) is_succ_homomorphism v,w

for w being Element of Inf_seq AtomicFamily

for U being Choice_Function of (BOOL (Subformulae v)) holds choice_succ_func (w,v,U) is_succ_homomorphism v,w

proof end;

definition

let H be LTL-formula;

end;
attr H is neg-inner-most means :: MODELC_3:def 37

for G being LTL-formula st G is_subformula_of H & G is negative holds

the_argument_of G is atomic ;

for G being LTL-formula st G is_subformula_of H & G is negative holds

the_argument_of G is atomic ;

:: deftheorem defines neg-inner-most MODELC_3:def 37 :

for H being LTL-formula holds

( H is neg-inner-most iff for G being LTL-formula st G is_subformula_of H & G is negative holds

the_argument_of G is atomic );

for H being LTL-formula holds

( H is neg-inner-most iff for G being LTL-formula st G is_subformula_of H & G is negative holds

the_argument_of G is atomic );

registration

ex b_{1} being LTL-formula st b_{1} is neg-inner-most
end;

cluster Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V265() V266() V267() V268() neg-inner-most for LTL-formula;

existence ex b

proof end;

definition

let H be LTL-formula;

end;
attr H is Sub_atomic means :: MODELC_3:def 38

( H is atomic or ex G being LTL-formula st

( G is atomic & H = 'not' G ) );

( H is atomic or ex G being LTL-formula st

( G is atomic & H = 'not' G ) );

:: deftheorem defines Sub_atomic MODELC_3:def 38 :

for H being LTL-formula holds

( H is Sub_atomic iff ( H is atomic or ex G being LTL-formula st

( G is atomic & H = 'not' G ) ) );

for H being LTL-formula holds

( H is Sub_atomic iff ( H is atomic or ex G being LTL-formula st

( G is atomic & H = 'not' G ) ) );

theorem Th63: :: MODELC_3:63

for F, H being LTL-formula st H is neg-inner-most & F is_subformula_of H holds

F is neg-inner-most by MODELC_2:35;

F is neg-inner-most by MODELC_2:35;

theorem Th64: :: MODELC_3:64

for H being LTL-formula holds

( H is Sub_atomic iff ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) )

( H is Sub_atomic iff ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) )

proof end;

theorem Th65: :: MODELC_3:65

for H being LTL-formula holds

( not H is neg-inner-most or H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

( not H is neg-inner-most or H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

proof end;

theorem :: MODELC_3:66

for H being LTL-formula st H is next & H is neg-inner-most holds

the_argument_of H is neg-inner-most

the_argument_of H is neg-inner-most

proof end;

theorem :: MODELC_3:67

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & H is neg-inner-most holds

( the_left_argument_of H is neg-inner-most & the_right_argument_of H is neg-inner-most )

( the_left_argument_of H is neg-inner-most & the_right_argument_of H is neg-inner-most )

proof end;

definition

let W be non empty set ;

attr c_{2} is strict ;

struct BuchiAutomaton over W -> 1-sorted ;

aggr BuchiAutomaton(# carrier, Tran, InitS, FinalS #) -> BuchiAutomaton over W;

sel Tran c_{2} -> Relation of [: the carrier of c_{2},W:], the carrier of c_{2};

sel InitS c_{2} -> Element of bool the carrier of c_{2};

sel FinalS c_{2} -> Subset of (bool the carrier of c_{2});

end;
attr c

struct BuchiAutomaton over W -> 1-sorted ;

aggr BuchiAutomaton(# carrier, Tran, InitS, FinalS #) -> BuchiAutomaton over W;

sel Tran c

sel InitS c

sel FinalS c

definition

let W be non empty set ;

let B be BuchiAutomaton over W;

let w be Element of Inf_seq W;

end;
let B be BuchiAutomaton over W;

let w be Element of Inf_seq W;

pred w is-accepted-by B means :: MODELC_3:def 39

ex run being sequence of the carrier of B st

( run . 0 in the InitS of B & ( for i being Nat holds

( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B & ( for FSet being set st FSet in the FinalS of B holds

{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) );

ex run being sequence of the carrier of B st

( run . 0 in the InitS of B & ( for i being Nat holds

( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B & ( for FSet being set st FSet in the FinalS of B holds

{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) );

:: deftheorem defines is-accepted-by MODELC_3:def 39 :

for W being non empty set

for B being BuchiAutomaton over W

for w being Element of Inf_seq W holds

( w is-accepted-by B iff ex run being sequence of the carrier of B st

( run . 0 in the InitS of B & ( for i being Nat holds

( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B & ( for FSet being set st FSet in the FinalS of B holds

{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) ) );

for W being non empty set

for B being BuchiAutomaton over W

for w being Element of Inf_seq W holds

( w is-accepted-by B iff ex run being sequence of the carrier of B st

( run . 0 in the InitS of B & ( for i being Nat holds

( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B & ( for FSet being set st FSet in the FinalS of B holds

{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) ) );

definition

let v be neg-inner-most LTL-formula;

let N be strict LTLnode over v;

coherence

{ x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } is Subset of LTL_WFF;

coherence

{ x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } is Subset of LTL_WFF;

end;
let N be strict LTLnode over v;

func atomic_LTL N -> Subset of LTL_WFF equals :: MODELC_3:def 40

{ x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;

correctness { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;

coherence

{ x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } is Subset of LTL_WFF;

proof end;

func Neg_atomic_LTL N -> Subset of LTL_WFF equals :: MODELC_3:def 41

{ x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } ;

correctness { x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } ;

coherence

{ x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } is Subset of LTL_WFF;

proof end;

:: deftheorem defines atomic_LTL MODELC_3:def 40 :

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v holds atomic_LTL N = { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v holds atomic_LTL N = { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;

:: deftheorem defines Neg_atomic_LTL MODELC_3:def 41 :

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v holds Neg_atomic_LTL N = { x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } ;

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v holds Neg_atomic_LTL N = { x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } ;

definition

let v be neg-inner-most LTL-formula;

let N be strict LTLnode over v;

coherence

{ x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } is set ;

;

end;
let N be strict LTLnode over v;

func Label_ N -> set equals :: MODELC_3:def 42

{ x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } ;

correctness { x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } ;

coherence

{ x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } is set ;

;

:: deftheorem defines Label_ MODELC_3:def 42 :

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v holds Label_ N = { x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } ;

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v holds Label_ N = { x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } ;

definition

let v be neg-inner-most LTL-formula;

coherence

{ y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st

( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } is Relation of [:(LTLStates v),AtomicFamily:],(LTLStates v);

coherence

{(init v)} is Element of bool (LTLStates v);

end;
func Tran_LTL v -> Relation of [:(LTLStates v),AtomicFamily:],(LTLStates v) equals :: MODELC_3:def 43

{ y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st

( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;

correctness { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st

( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;

coherence

{ y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st

( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } is Relation of [:(LTLStates v),AtomicFamily:],(LTLStates v);

proof end;

correctness coherence

{(init v)} is Element of bool (LTLStates v);

proof end;

:: deftheorem defines Tran_LTL MODELC_3:def 43 :

for v being neg-inner-most LTL-formula holds Tran_LTL v = { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st

( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;

for v being neg-inner-most LTL-formula holds Tran_LTL v = { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st

( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;

:: deftheorem defines InitS_LTL MODELC_3:def 44 :

for v being neg-inner-most LTL-formula holds InitS_LTL v = {(init v)};

for v being neg-inner-most LTL-formula holds InitS_LTL v = {(init v)};

definition

let v be neg-inner-most LTL-formula;

let F be LTL-formula;

coherence

{ x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } is Element of bool (LTLStates v);

end;
let F be LTL-formula;

func FinalS_LTL (F,v) -> Element of bool (LTLStates v) equals :: MODELC_3:def 45

{ x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } ;

correctness { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } ;

coherence

{ x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } is Element of bool (LTLStates v);

proof end;

:: deftheorem defines FinalS_LTL MODELC_3:def 45 :

for v being neg-inner-most LTL-formula

for F being LTL-formula holds FinalS_LTL (F,v) = { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } ;

for v being neg-inner-most LTL-formula

for F being LTL-formula holds FinalS_LTL (F,v) = { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } ;

definition

let v be neg-inner-most LTL-formula;

coherence

{ x where x is Element of bool (LTLStates v) : ex F being LTL-formula st

( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } is Subset of (bool (LTLStates v));

end;
func FinalS_LTL v -> Subset of (bool (LTLStates v)) equals :: MODELC_3:def 46

{ x where x is Element of bool (LTLStates v) : ex F being LTL-formula st

( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;

correctness { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st

( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;

coherence

{ x where x is Element of bool (LTLStates v) : ex F being LTL-formula st

( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } is Subset of (bool (LTLStates v));

proof end;

:: deftheorem defines FinalS_LTL MODELC_3:def 46 :

for v being neg-inner-most LTL-formula holds FinalS_LTL v = { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st

( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;

for v being neg-inner-most LTL-formula holds FinalS_LTL v = { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st

( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;

definition

let v be neg-inner-most LTL-formula;

coherence

BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #) is BuchiAutomaton over AtomicFamily ;

;

end;
func BAutomaton v -> BuchiAutomaton over AtomicFamily equals :: MODELC_3:def 47

BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);

correctness BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);

coherence

BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #) is BuchiAutomaton over AtomicFamily ;

;

:: deftheorem defines BAutomaton MODELC_3:def 47 :

for v being neg-inner-most LTL-formula holds BAutomaton v = BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);

for v being neg-inner-most LTL-formula holds BAutomaton v = BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);

::************

:: verification of the main theorem

::************

:: verification of the main theorem

::************

theorem Th68: :: MODELC_3:68

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula st w is-accepted-by BAutomaton v holds

w |= v

for v being neg-inner-most LTL-formula st w is-accepted-by BAutomaton v holds

w |= v

proof end;

definition

let w be Element of Inf_seq AtomicFamily;

let v be neg-inner-most LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

assume that

A1: not N is elementary and

A2: w |= * N ;

ex b_{1} being Nat st

( ( for i being Nat st i < b_{1} holds

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b_{1}) . N),v) is elementary & ( for i being Nat st i <= b_{1} holds

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) )

for b_{1}, b_{2} being Nat st ( for i being Nat st i < b_{1} holds

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b_{1}) . N),v) is elementary & ( for i being Nat st i <= b_{1} holds

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) & ( for i being Nat st i < b_{2} holds

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b_{2}) . N),v) is elementary & ( for i being Nat st i <= b_{2} holds

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) holds

b_{1} = b_{2}

end;
let v be neg-inner-most LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

assume that

A1: not N is elementary and

A2: w |= * N ;

func chosen_succ_end_num (w,v,U,N) -> Nat means :Def48: :: MODELC_3:def 48

( ( for i being Nat st i < it holds

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** it) . N),v) is elementary & ( for i being Nat st i <= it holds

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) );

existence ( ( for i being Nat st i < it holds

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** it) . N),v) is elementary & ( for i being Nat st i <= it holds

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) );

ex b

( ( for i being Nat st i < b

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) )

proof end;

uniqueness for b

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) & ( for i being Nat st i < b

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) holds

b

proof end;

:: deftheorem Def48 defines chosen_succ_end_num MODELC_3:def 48 :

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v st not N is elementary & w |= * N holds

for b_{5} being Nat holds

( b_{5} = chosen_succ_end_num (w,v,U,N) iff ( ( for i being Nat st i < b_{5} holds

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b_{5}) . N),v) is elementary & ( for i being Nat st i <= b_{5} holds

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) ) );

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v st not N is elementary & w |= * N holds

for b

( b

( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b

w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) ) );

definition

let w be Element of Inf_seq AtomicFamily;

let v be neg-inner-most LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

assume A1: w |= * ('X' N) ;

coherence

( ( not 'X' N is elementary implies CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) is strict elementary LTLnode over v ) & ( 'X' N is elementary implies FinalNode v is strict elementary LTLnode over v ) );

consistency

for b_{1} being strict elementary LTLnode over v holds verum;

by A1, Def48;

end;
let v be neg-inner-most LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

let N be strict LTLnode over v;

assume A1: w |= * ('X' N) ;

func chosen_next (w,v,U,N) -> strict elementary LTLnode over v equals :Def49: :: MODELC_3:def 49

CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) if not 'X' N is elementary

otherwise FinalNode v;

correctness CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) if not 'X' N is elementary

otherwise FinalNode v;

coherence

( ( not 'X' N is elementary implies CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) is strict elementary LTLnode over v ) & ( 'X' N is elementary implies FinalNode v is strict elementary LTLnode over v ) );

consistency

for b

by A1, Def48;

:: deftheorem Def49 defines chosen_next MODELC_3:def 49 :

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v st w |= * ('X' N) holds

( ( not 'X' N is elementary implies chosen_next (w,v,U,N) = CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) ) & ( 'X' N is elementary implies chosen_next (w,v,U,N) = FinalNode v ) );

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for N being strict LTLnode over v st w |= * ('X' N) holds

( ( not 'X' N is elementary implies chosen_next (w,v,U,N) = CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) ) & ( 'X' N is elementary implies chosen_next (w,v,U,N) = FinalNode v ) );

theorem Th69: :: MODELC_3:69

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for s being strict elementary LTLnode over v st w |= * ('X' s) holds

( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for s being strict elementary LTLnode over v st w |= * ('X' s) holds

( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )

proof end;

definition

let w be Element of Inf_seq AtomicFamily;

let v be neg-inner-most LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

ex b_{1} being sequence of (LTLStates v) st

( b_{1} . 0 = init v & ( for n being Nat holds b_{1} . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b_{1} . n),v))) ) )

for b_{1}, b_{2} being sequence of (LTLStates v) st b_{1} . 0 = init v & ( for n being Nat holds b_{1} . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b_{1} . n),v))) ) & b_{2} . 0 = init v & ( for n being Nat holds b_{2} . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b_{2} . n),v))) ) holds

b_{1} = b_{2}

end;
let v be neg-inner-most LTL-formula;

let U be Choice_Function of (BOOL (Subformulae v));

func chosen_run (w,v,U) -> sequence of (LTLStates v) means :Def50: :: MODELC_3:def 50

( it . 0 = init v & ( for n being Nat holds it . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((it . n),v))) ) );

existence ( it . 0 = init v & ( for n being Nat holds it . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((it . n),v))) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def50 defines chosen_run MODELC_3:def 50 :

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for b_{4} being sequence of (LTLStates v) holds

( b_{4} = chosen_run (w,v,U) iff ( b_{4} . 0 = init v & ( for n being Nat holds b_{4} . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b_{4} . n),v))) ) ) );

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v))

for b

( b

Lm33: for v being neg-inner-most LTL-formula holds 'X' (CastLTL ({} v)) = {}

proof end;

theorem Th70: :: MODELC_3:70

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v st w |= * N holds

Shift (w,1) |= * ('X' N)

for v being neg-inner-most LTL-formula

for N being strict LTLnode over v st w |= * N holds

Shift (w,1) |= * ('X' N)

proof end;

theorem :: MODELC_3:71

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula st w |= 'X' v holds

w |= * (init v)

for v being neg-inner-most LTL-formula st w |= 'X' v holds

w |= * (init v)

proof end;

theorem Th72: :: MODELC_3:72

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula holds

( w |= v iff w |= * ('X' (init v)) )

for v being neg-inner-most LTL-formula holds

( w |= v iff w |= * ('X' (init v)) )

proof end;

theorem Th73: :: MODELC_3:73

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v)) st w |= v holds

for n being Nat holds

( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) )

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v)) st w |= v holds

for n being Nat holds

( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) )

proof end;

theorem Th74: :: MODELC_3:74

for H being LTL-formula

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v)) st w |= v holds

for i being Nat st H in the LTLold of (CastNode (((chosen_run (w,v,U)) . (i + 1)),v)) & H is Until & Shift (w,i) |= the_right_argument_of H holds

the_right_argument_of H in the LTLold of (CastNode (((chosen_run (w,v,U)) . (i + 1)),v))

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula

for U being Choice_Function of (BOOL (Subformulae v)) st w |= v holds

for i being Nat st H in the LTLold of (CastNode (((chosen_run (w,v,U)) . (i + 1)),v)) & H is Until & Shift (w,i) |= the_right_argument_of H holds

the_right_argument_of H in the LTLold of (CastNode (((chosen_run (w,v,U)) . (i + 1)),v))

proof end;

theorem Th75: :: MODELC_3:75

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula st w |= v holds

w is-accepted-by BAutomaton v

for v being neg-inner-most LTL-formula st w |= v holds

w is-accepted-by BAutomaton v

proof end;

theorem :: MODELC_3:76

for w being Element of Inf_seq AtomicFamily

for v being neg-inner-most LTL-formula holds

( w is-accepted-by BAutomaton v iff w |= v ) by Th68, Th75;

for v being neg-inner-most LTL-formula holds

( w is-accepted-by BAutomaton v iff w |= v ) by Th68, Th75;