:: Model Checking, Part {III}
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received August 19, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

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

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

Lm3:  for H being LTL-formula holds
( <*H*> . 1 = H &amp; rng <*H*> = {H} )
proofend;

Lm4:  for r1, r2 being real number st r1 <= r2 holds
[\r1/] <= [\r2/]
proofend;

Lm5:  for r1, r2 being real number st r1 <= r2 - 1 holds
[\r1/] <= [\r2/] - 1
proofend;

Lm6:  for n being Nat holds
( n = 0 or 1 <= n )
proofend;

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

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 &amp; the_right_argument_of H is_subformula_of H )
proofend;

Lm9:  for F, H being LTL-formula st F is_subformula_of H holds
{F} is Subset of (Subformulae H)
proofend;

Lm10:  for F, H, G being LTL-formula st F is_subformula_of H &amp; G is_subformula_of H holds
{F,G} is Subset of (Subformulae H)
proofend;

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

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) &amp; {(the_right_argument_of H)} is Subset of (Subformulae H) )
proofend;

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

definition
let F be LTL-formula;
:: original:Subformulae
redefine func Subformulae F ->  Subset of LTL_WFF;
coherence
 Subformulae F is Subset of LTL_WFF
proofend;
end;

:: definition of basic operations to build an automaton for LTL.
definition
let H be LTL-formula;
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
coherence
( ( H is conjunctive implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) &amp; ( H is disjunctive implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) &amp; ( H is next implies {} is Subset of (Subformulae H) ) &amp; ( H is Until implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) &amp; ( H is Release implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) &amp; ( not H is conjunctive &amp; not H is disjunctive &amp; not H is next &amp; not H is Until &amp; not H is Release implies {} is Subset of (Subformulae H) ) );
consistency
for b1 being Subset of (Subformulae H) holds
( ( H is conjunctive &amp; H is disjunctive implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {(the_left_argument_of H)} ) ) &amp; ( H is conjunctive &amp; H is next implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {} ) ) &amp; ( H is conjunctive &amp; H is Until implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {(the_left_argument_of H)} ) ) &amp; ( H is conjunctive &amp; H is Release implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is disjunctive &amp; H is next implies ( b1 = {(the_left_argument_of H)} iff b1 = {} ) ) &amp; ( H is disjunctive &amp; H is Until implies ( b1 = {(the_left_argument_of H)} iff b1 = {(the_left_argument_of H)} ) ) &amp; ( H is disjunctive &amp; H is Release implies ( b1 = {(the_left_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is next &amp; H is Until implies ( b1 = {} iff b1 = {(the_left_argument_of H)} ) ) &amp; ( H is next &amp; H is Release implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is Until &amp; H is Release implies ( b1 = {(the_left_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) );
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
coherence
( ( H is conjunctive implies {} is Subset of (Subformulae H) ) &amp; ( H is disjunctive implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) &amp; ( H is next implies {} is Subset of (Subformulae H) ) &amp; ( H is Until implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) &amp; ( H is Release implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) &amp; ( not H is conjunctive &amp; not H is disjunctive &amp; not H is next &amp; not H is Until &amp; not H is Release implies {} is Subset of (Subformulae H) ) );
consistency
for b1 being Subset of (Subformulae H) holds
( ( H is conjunctive &amp; H is disjunctive implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is conjunctive &amp; H is next implies ( b1 = {} iff b1 = {} ) ) &amp; ( H is conjunctive &amp; H is Until implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is conjunctive &amp; H is Release implies ( b1 = {} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) &amp; ( H is disjunctive &amp; H is next implies ( b1 = {(the_right_argument_of H)} iff b1 = {} ) ) &amp; ( H is disjunctive &amp; H is Until implies ( b1 = {(the_right_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is disjunctive &amp; H is Release implies ( b1 = {(the_right_argument_of H)} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) &amp; ( H is next &amp; H is Until implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) &amp; ( H is next &amp; H is Release implies ( b1 = {} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) &amp; ( H is Until &amp; H is Release implies ( b1 = {(the_right_argument_of H)} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) );
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
coherence
( ( H is conjunctive implies {} is Subset of (Subformulae H) ) &amp; ( H is disjunctive implies {} is Subset of (Subformulae H) ) &amp; ( H is next implies {(the_argument_of H)} is Subset of (Subformulae H) ) &amp; ( H is Until implies {H} is Subset of (Subformulae H) ) &amp; ( H is Release implies {H} is Subset of (Subformulae H) ) &amp; ( not H is conjunctive &amp; not H is disjunctive &amp; not H is next &amp; not H is Until &amp; not H is Release implies {} is Subset of (Subformulae H) ) );
consistency
for b1 being Subset of (Subformulae H) holds
( ( H is conjunctive &amp; H is disjunctive implies ( b1 = {} iff b1 = {} ) ) &amp; ( H is conjunctive &amp; H is next implies ( b1 = {} iff b1 = {(the_argument_of H)} ) ) &amp; ( H is conjunctive &amp; H is Until implies ( b1 = {} iff b1 = {H} ) ) &amp; ( H is conjunctive &amp; H is Release implies ( b1 = {} iff b1 = {H} ) ) &amp; ( H is disjunctive &amp; H is next implies ( b1 = {} iff b1 = {(the_argument_of H)} ) ) &amp; ( H is disjunctive &amp; H is Until implies ( b1 = {} iff b1 = {H} ) ) &amp; ( H is disjunctive &amp; H is Release implies ( b1 = {} iff b1 = {H} ) ) &amp; ( H is next &amp; H is Until implies ( b1 = {(the_argument_of H)} iff b1 = {H} ) ) &amp; ( H is next &amp; H is Release implies ( b1 = {(the_argument_of H)} iff b1 = {H} ) ) &amp; ( H is Until &amp; H is Release implies ( b1 = {H} iff b1 = {H} ) ) );
by Lm13, Lm14, MODELC_2:78, SUBSET_1:1;
end;

:: 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)} ) &amp; ( H is disjunctive implies LTLNew1 H = {(the_left_argument_of H)} ) &amp; ( H is next implies LTLNew1 H = {} ) &amp; ( H is Until implies LTLNew1 H = {(the_left_argument_of H)} ) &amp; ( H is Release implies LTLNew1 H = {(the_right_argument_of H)} ) &amp; ( not H is conjunctive &amp; not H is disjunctive &amp; not H is next &amp; not H is Until &amp; 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 = {} ) &amp; ( H is disjunctive implies LTLNew2 H = {(the_right_argument_of H)} ) &amp; ( H is next implies LTLNew2 H = {} ) &amp; ( H is Until implies LTLNew2 H = {(the_right_argument_of H)} ) &amp; ( H is Release implies LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} ) &amp; ( not H is conjunctive &amp; not H is disjunctive &amp; not H is next &amp; not H is Until &amp; 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 = {} ) &amp; ( H is disjunctive implies LTLNext H = {} ) &amp; ( H is next implies LTLNext H = {(the_argument_of H)} ) &amp; ( H is Until implies LTLNext H = {H} ) &amp; ( H is Release implies LTLNext H = {H} ) &amp; ( not H is conjunctive &amp; not H is disjunctive &amp; not H is next &amp; not H is Until &amp; not H is Release implies LTLNext H = {} ) );

definition
let v be LTL-formula;
attrc2 is strict ;
struct LTLnode over v -> ;
aggrLTLnode(# LTLold, LTLnew, LTLnext #) ->  LTLnode over v;
sel LTLold c2 ->  Subset of (Subformulae v);
sel LTLnew c2 ->  Subset of (Subformulae v);
sel LTLnext c2 ->  Subset of (Subformulae v);
end;

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 ;
func SuccNode1 (H,N) ->  strict LTLnode over v means :Def4: :: MODELC_3:def 4
( the LTLold of it = the LTLold of N \/ {H} &amp; the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) &amp; the LTLnext of it = the LTLnext of N \/ (LTLNext H) );
existence
 ex b1 being strict LTLnode over v st
( the LTLold of b1 = the LTLold of N \/ {H} &amp; the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) &amp; the LTLnext of b1 = the LTLnext of N \/ (LTLNext H) )
proofend;
uniqueness
 for b1, b2 being strict LTLnode over v st the LTLold of b1 = the LTLold of N \/ {H} &amp; the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) &amp; the LTLnext of b1 = the LTLnext of N \/ (LTLNext H) &amp; the LTLold of b2 = the LTLold of N \/ {H} &amp; the LTLnew of b2 = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) &amp; the LTLnext of b2 = the LTLnext of N \/ (LTLNext H) holds
b1 = b2 ;
end;

:: 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 b4 being strict LTLnode over v holds
( b4 = SuccNode1 (H,N) iff ( the LTLold of b4 = the LTLold of N \/ {H} &amp; the LTLnew of b4 = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) &amp; the LTLnext of b4 = the LTLnext of N \/ (LTLNext H) ) );

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 ;
func SuccNode2 (H,N) ->  strict LTLnode over v means :Def5: :: MODELC_3:def 5
( the LTLold of it = the LTLold of N \/ {H} &amp; the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) &amp; the LTLnext of it = the LTLnext of N );
existence
 ex b1 being strict LTLnode over v st
( the LTLold of b1 = the LTLold of N \/ {H} &amp; the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) &amp; the LTLnext of b1 = the LTLnext of N )
proofend;
uniqueness
 for b1, b2 being strict LTLnode over v st the LTLold of b1 = the LTLold of N \/ {H} &amp; the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) &amp; the LTLnext of b1 = the LTLnext of N &amp; the LTLold of b2 = the LTLold of N \/ {H} &amp; the LTLnew of b2 = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) &amp; the LTLnext of b2 = the LTLnext of N holds
b1 = b2 ;
end;

:: 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 b4 being strict LTLnode over v holds
( b4 = SuccNode2 (H,N) iff ( the LTLold of b4 = the LTLold of N \/ {H} &amp; the LTLnew of b4 = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) &amp; the LTLnext of b4 = the LTLnext of N ) );

definition
let v be LTL-formula;
let N1, N2 be LTLnode over v;
let H be LTL-formula;
predN2 is_succ_of N1,H means :Def6: :: MODELC_3:def 6
( H in the LTLnew of N1 &amp; ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) &amp; N2 = SuccNode2 (H,N1) ) ) );
end;

:: deftheorem Def6 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 &amp; ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) &amp; N2 = SuccNode2 (H,N1) ) ) ) );

definition
let v be LTL-formula;
let N1, N2 be LTLnode over v;
predN2 is_succ1_of N1 means :Def7: :: MODELC_3:def 7
 ex H being LTL-formula st
( H in the LTLnew of N1 &amp; N2 = SuccNode1 (H,N1) );
predN2 is_succ2_of N1 means :Def8: :: MODELC_3:def 8
 ex H being LTL-formula st
( H in the LTLnew of N1 &amp; ( H is disjunctive or H is Until or H is Release ) &amp; N2 = SuccNode2 (H,N1) );
end;

:: deftheorem Def7 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 &amp; N2 = SuccNode1 (H,N1) ) );

:: deftheorem Def8 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 &amp; ( H is disjunctive or H is Until or H is Release ) &amp; N2 = SuccNode2 (H,N1) ) );

definition
let v be LTL-formula;
let N1, N2 be LTLnode over v;
predN2 is_succ_of N1 means :Def9: :: MODELC_3:def 9
( N2 is_succ1_of N1 or N2 is_succ2_of N1 );
end;

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

definition
let v be LTL-formula;
let N be LTLnode over v;
attrN is failure  means :: MODELC_3:def 10
 ex H, F being LTL-formula st
( H is atomic &amp; F = 'not' H &amp; H in the LTLold of N &amp; F in the LTLold of N );
end;

:: 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 &amp; F = 'not' H &amp; H in the LTLold of N &amp; F in the LTLold of N ) );

definition
let v be LTL-formula;
let N be LTLnode over v;
attrN is elementary  means :Def11: :: MODELC_3:def 11
 the LTLnew of N = {} ;
end;

:: 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 = {} );

definition
let v be LTL-formula;
let N be LTLnode over v;
attrN is final  means :: MODELC_3:def 12
( N is elementary &amp; the LTLnext of N = {} );
end;

:: 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 &amp; the LTLnext of N = {} ) );

definition
let v be LTL-formula;
func {} v ->  Subset of (Subformulae v) equals :: MODELC_3:def 13
 {} ;
correctness
coherence
{} is Subset of (Subformulae v);
by SUBSET_1:1;
end;

:: deftheorem  defines {} MODELC_3:def_13_:_
 for v being LTL-formula holds {} v = {} ;

definition
let v be LTL-formula;
func Seed v ->  Subset of (Subformulae v) equals :: MODELC_3:def 14
{v};
correctness
coherence
{v} is Subset of (Subformulae v);
by Lm9;
end;

:: deftheorem  defines Seed MODELC_3:def_14_:_
 for v being LTL-formula holds Seed v = {v};

registration
let v be LTL-formula;
cluster strict elementary for LTLnode over v;
existence
 ex b1 being LTLnode over v st
( b1 is elementary &amp; b1 is strict )
proofend;
end;

definition
let v be LTL-formula;
func FinalNode v ->  strict elementary LTLnode over v equals :: MODELC_3:def 15
 LTLnode(# ({} v),({} v),({} v) #);
correctness
coherence
LTLnode(# ({} v),({} v),({} v) #) is strict elementary LTLnode over v;
by Def11;
end;

:: deftheorem  defines FinalNode MODELC_3:def_15_:_
 for v being LTL-formula holds FinalNode v = LTLnode(# ({} v),({} v),({} v) #);

definition
let x be set ;
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
coherence
( ( x is strict LTLnode over v implies x is strict LTLnode over v ) &amp; ( x is not strict LTLnode over v implies LTLnode(# ({} v),({} v),({} v) #) is strict LTLnode over v ) );
consistency
for b1 being strict LTLnode over v holds verum;
;
end;

:: deftheorem Def16 defines CastNode MODELC_3:def_16_:_
 for x being set
for v being LTL-formula holds
( ( x is strict LTLnode over v implies CastNode (x,v) = x ) &amp; ( x is not strict LTLnode over v implies CastNode (x,v) = LTLnode(# ({} v),({} v),({} v) #) ) );

definition
let v be LTL-formula;
func init v ->  strict elementary LTLnode over v equals :: MODELC_3:def 17
 LTLnode(# ({} v),({} v),(Seed v) #);
correctness
coherence
LTLnode(# ({} v),({} v),(Seed v) #) is strict elementary LTLnode over v;
by Def11;
end;

:: deftheorem  defines init MODELC_3:def_17_:_
 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;
func 'X' N ->  strict LTLnode over v equals :: MODELC_3:def 18
 LTLnode(# ({} v), the LTLnext of N,({} v) #);
correctness
coherence
LTLnode(# ({} v), the LTLnext of N,({} v) #) is strict LTLnode over v;
;
end;

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

definition
let v be LTL-formula;
let L be FinSequence;
predL is_Finseq_for v means :Def19: :: MODELC_3:def 19
 for k being Nat st 1 <= k &amp; k < len L holds
ex N, M being strict LTLnode over v st
( N = L . k &amp; M = L . (k + 1) &amp; M is_succ_of N );
end;

:: deftheorem Def19 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 &amp; k < len L holds
ex N, M being strict LTLnode over v st
( N = L . k &amp; M = L . (k + 1) &amp; 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 &amp; 1 <= m &amp; m <= len L holds
ex L1, L2 being FinSequence st
( L2 is_Finseq_for v &amp; L = L1 ^ L2 &amp; L2 . 1 = L . m &amp; 1 <= len L2 &amp; len L2 = (len L) - (m - 1) &amp; L2 . (len L2) = L . (len L) )
proofend;

definition
let v be LTL-formula;
let N1, N2 be strict LTLnode over v;
predN2 is_next_of N1 means :Def20: :: MODELC_3:def 20
( N1 is elementary &amp; N2 is elementary &amp; ex L being FinSequence st
( 1 <= len L &amp; L is_Finseq_for v &amp; L . 1 = 'X' N1 &amp; L . (len L) = N2 ) );
end;

:: deftheorem Def20 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 &amp; N2 is elementary &amp; ex L being FinSequence st
( 1 <= len L &amp; L is_Finseq_for v &amp; L . 1 = 'X' N1 &amp; L . (len L) = N2 ) ) );

definition
let v be LTL-formula;
let W be Subset of (Subformulae v);
func CastLTL W ->  Subset of LTL_WFF equals :: MODELC_3:def 21
W;
correctness
coherence
W is Subset of LTL_WFF;
by MODELC_2:47;
end;

:: deftheorem  defines CastLTL MODELC_3:def_21_:_
 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;
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
coherence
( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) is Subset of LTL_WFF;
proofend;
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));

Lm16:  for H, v being LTL-formula
for N being strict LTLnode over v st H in the LTLnew of N &amp; ( H is atomic or H is negative ) holds
* N = * (SuccNode1 (H,N))
proofend;

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 &amp; ( H is conjunctive or H is next ) holds
( w |= * N iff w |= * (SuccNode1 (H,N)) )
proofend;

theorem :: MODELC_3:1
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 &amp; ( H is atomic or H is negative or H is conjunctive or H is next ) holds
( w |= * N iff w |= * (SuccNode1 (H,N)) ) by Lm16, Lm17;

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 &amp; H is disjunctive holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
proofend;

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 &amp; H is Until holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
proofend;

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 &amp; H is Release holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
proofend;

theorem :: MODELC_3:2
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 &amp; ( H is disjunctive or H is Until or H is Release ) holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ) by Lm18, Lm19, Lm20;

Lm21:  for H being LTL-formula st ( H is negative or H is next ) holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
proofend;

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

Lm23:  for H being LTL-formula st H is atomic holds
Subformulae H = {H}
proofend;

Lm24:  for H being LTL-formula
for W being Subset of (Subformulae H) holds not {} in W
proofend;

theorem Th3: :: MODELC_3:3
for H being LTL-formula ex L being FinSequence st Subformulae H = rng L
proofend;

registration
let H be LTL-formula;
cluster Subformulae H ->  finite ;
correctness
coherence
Subformulae H is finite ;
proofend;
end;

definition
let H be LTL-formula;
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
coherence
( ( L . x in W implies len (CastLTL (L . x)) is Nat ) &amp; ( not L . x in W implies 0 is Nat ) );
consistency
for b1 being Nat holds verum;
;
end;

:: 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)) ) &amp; ( 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;
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)) ) &amp; ( not L . k in W implies it . k = 0 ) );
existence
 ex b1 being Real_Sequence st
for k being Nat holds
( ( L . k in W implies b1 . k = len (CastLTL (L . k)) ) &amp; ( not L . k in W implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for k being Nat holds
( ( L . k in W implies b1 . k = len (CastLTL (L . k)) ) &amp; ( not L . k in W implies b1 . k = 0 ) ) ) &amp; ( for k being Nat holds
( ( L . k in W implies b2 . k = len (CastLTL (L . k)) ) &amp; ( not L . k in W implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
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 b4 being Real_Sequence holds
( b4 = Partial_seq (L,W) iff for k being Nat holds
( ( L . k in W implies b4 . k = len (CastLTL (L . k)) ) &amp; ( not L . k in W implies b4 . k = 0 ) ) );

definition
let H be LTL-formula;
let W be Subset of (Subformulae H);
let L be FinSequence;
func len (L,W) ->  Real equals :: MODELC_3:def 25
 Sum ((Partial_seq (L,W)),(len L));
correctness
coherence
Sum ((Partial_seq (L,W)),(len L)) is Real;
;
end;

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

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

Lm26:  for n, j being Nat
for R1, R2 being Real_Sequence st ( for i being Nat st i <= n &amp; not i = j holds
R1 . i = R2 . i ) &amp; j <= n holds
(Sum (R1,n)) - (R1 . j) = (Sum (R2,n)) - (R2 . j)
proofend;

theorem Th4: :: MODELC_3:4
for L being FinSequence
for H being LTL-formula holds len (L,({} H)) = 0
proofend;

theorem Th5: :: MODELC_3:5
for L being FinSequence
for H, F being LTL-formula
for W being Subset of (Subformulae H) st not F in W holds
len (L,(W \ {F})) = len (L,W)
proofend;

theorem Th6: :: MODELC_3:6
for L being FinSequence
for H, F being LTL-formula
for W being Subset of (Subformulae H) st rng L = Subformulae H &amp; L is one-to-one &amp; F in W holds
len (L,(W \ {F})) = (len (L,W)) - (len F)
proofend;

theorem Th7: :: MODELC_3:7
for L being FinSequence
for H, F being LTL-formula
for W, W1 being Subset of (Subformulae H) st rng L = Subformulae H &amp; L is one-to-one &amp; not F in W &amp; W1 = W \/ {F} holds
len (L,W1) = (len (L,W)) + (len F)
proofend;

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 &amp; L1 is one-to-one &amp; rng L2 = Subformulae H &amp; L2 is one-to-one holds
len (L1,W) = len (L2,W)
proofend;

definition
let H be LTL-formula;
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 &amp; L is one-to-one &amp; it = len (L,W) );
existence
 ex b1 being Real ex L being FinSequence st
( rng L = Subformulae H &amp; L is one-to-one &amp; b1 = len (L,W) )
proofend;
uniqueness
 for b1, b2 being Real st ex L being FinSequence st
( rng L = Subformulae H &amp; L is one-to-one &amp; b1 = len (L,W) ) &amp; ex L being FinSequence st
( rng L = Subformulae H &amp; L is one-to-one &amp; b2 = len (L,W) ) holds
b1 = b2 by Th8;
end;

:: deftheorem Def26 defines len MODELC_3:def_26_:_
 for H being LTL-formula
for W being Subset of (Subformulae H)
for b3 being Real holds
( b3 = len W iff ex L being FinSequence st
( rng L = Subformulae H &amp; L is one-to-one &amp; b3 = len (L,W) ) );

theorem :: MODELC_3:9
for H, F being LTL-formula
for W being Subset of (Subformulae H) st not F in W holds
len (W \ {F}) = len W
proofend;

theorem Th10: :: MODELC_3:10
for H, F being LTL-formula
for W being Subset of (Subformulae H) st F in W holds
len (W \ {F}) = (len W) - (len F)
proofend;

theorem Th11: :: MODELC_3:11
for H, F being LTL-formula
for W, W1 being Subset of (Subformulae H) st not F in W &amp; W1 = W \/ {F} holds
len W1 = (len W) + (len F)
proofend;

theorem Th12: :: MODELC_3:12
for H, F being LTL-formula
for W1, W being Subset of (Subformulae H) st W1 = W \/ {F} holds
len W1 <= (len W) + (len F)
proofend;

theorem Th13: :: MODELC_3:13
for H being LTL-formula holds len ({} H) = 0
proofend;

theorem Th14: :: MODELC_3:14
for H, F being LTL-formula
for W being Subset of (Subformulae H) st W = {F} holds
len W = len F
proofend;

Lm27:  for H being LTL-formula
for W, W1 being Subset of (Subformulae H) holds
( not W c= W1 or W = W1 or ex x being set st
( x in W1 &amp; W c= W1 \ {x} ) )
proofend;

theorem Th15: :: MODELC_3:15
for H being LTL-formula
for W, W1 being Subset of (Subformulae H) st W c= W1 holds
len W <= len W1
proofend;

theorem Th16: :: MODELC_3:16
for H being LTL-formula
for W being Subset of (Subformulae H) st len W < 1 holds
W = {} H
proofend;

theorem Th17: :: MODELC_3:17
for H being LTL-formula
for W being Subset of (Subformulae H) holds len W >= 0
proofend;

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

definition
let v, H be LTL-formula;
assume A1: H in Subformulae v ;
func LTLNew1 (H,v) ->  Subset of (Subformulae v) equals :Def27: :: MODELC_3:def 27
 LTLNew1 H;
correctness
coherence
LTLNew1 H is Subset of (Subformulae v);
proofend;
func LTLNew2 (H,v) ->  Subset of (Subformulae v) equals :Def28: :: MODELC_3:def 28
 LTLNew2 H;
correctness
coherence
LTLNew2 H is Subset of (Subformulae v);
proofend;
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;

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

Lm28:  for H, v being LTL-formula st H in Subformulae v holds
len (LTLNew1 (H,v)) <= (len H) - 1
proofend;

Lm29:  for H, v being LTL-formula st H in Subformulae v holds
len (LTLNew2 (H,v)) <= (len H) - 1
proofend;

theorem Th19: :: MODELC_3:19
for v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ1_of N1 holds
len the LTLnew of N2 <= (len the LTLnew of N1) - 1
proofend;

theorem Th20: :: MODELC_3:20
for v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ2_of N1 holds
len the LTLnew of N2 <= (len the LTLnew of N1) - 1
proofend;

definition
let v be LTL-formula;
let N be strict LTLnode over v;
func len N ->  Nat equals :: MODELC_3:def 29
[\(len the LTLnew of N)/];
correctness
coherence
[\(len the LTLnew of N)/] is Nat;
proofend;
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)/];

theorem Th21: :: MODELC_3:21
for v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ_of N1 holds
len N2 <= (len N1) - 1
proofend;

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

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

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 &amp; len L = n &amp; L . 1 = N &amp; L . n = M &amp; the LTLnew of M = {} v &amp; L is_Finseq_for v )
proofend;

theorem Th25: :: MODELC_3:25
for v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ_of N1 holds
( the LTLold of N1 c= the LTLold of N2 &amp; the LTLnext of N1 c= the LTLnext of N2 )
proofend;

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 &amp; m <= len L &amp; L1 = L | (Seg m) holds
L1 is_Finseq_for v
proofend;

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 &amp; not F in the LTLold of (CastNode ((L . 1),v)) &amp; 1 < n &amp; n <= len L &amp; F in the LTLold of (CastNode ((L . n),v)) holds
ex m being Nat st
( 1 <= m &amp; m < n &amp; not F in the LTLold of (CastNode ((L . m),v)) &amp; F in the LTLold of (CastNode ((L . (m + 1)),v)) )
proofend;

theorem Th28: :: MODELC_3:28
for F, v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ_of N1 &amp; not F in the LTLold of N1 &amp; F in the LTLold of N2 holds
N2 is_succ_of N1,F
proofend;

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 &amp; F in the LTLnew of (CastNode ((L . 1),v)) &amp; 1 < n &amp; n <= len L &amp; not F in the LTLnew of (CastNode ((L . n),v)) holds
ex m being Nat st
( 1 <= m &amp; m < n &amp; F in the LTLnew of (CastNode ((L . m),v)) &amp; not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
proofend;

theorem Th30: :: MODELC_3:30
for F, v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ_of N1 &amp; F in the LTLnew of N1 &amp; not F in the LTLnew of N2 holds
N2 is_succ_of N1,F
proofend;

theorem Th31: :: MODELC_3:31
for m, n being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v &amp; 1 <= m &amp; m <= n &amp; n <= len L holds
( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) &amp; the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) )
proofend;

theorem Th32: :: MODELC_3:32
for F, v being LTL-formula
for N2, N1 being strict LTLnode over v st N2 is_succ_of N1,F holds
F in the LTLold of N2
proofend;

theorem Th33: :: MODELC_3:33
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v &amp; 1 <= len L &amp; 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))
proofend;

theorem Th34: :: MODELC_3:34
for m being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v &amp; 1 <= m &amp; m <= len L &amp; 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))
proofend;

theorem Th35: :: MODELC_3:35
for k being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v &amp; 1 <= k &amp; k < len L holds
CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)
proofend;

theorem Th36: :: MODELC_3:36
for k being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v &amp; 1 <= k &amp; k <= len L holds
len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1
proofend;

theorem Th37: :: MODELC_3:37
for v being LTL-formula
for s2, s1 being strict elementary LTLnode over v st s2 is_next_of s1 holds
the LTLnext of s1 c= the LTLold of s2
proofend;

theorem Th38: :: MODELC_3:38
for F, v being LTL-formula
for s2, s1 being strict elementary LTLnode over v st s2 is_next_of s1 &amp; F in the LTLold of s2 holds
ex L being FinSequence ex m being Nat st
( 1 <= len L &amp; L is_Finseq_for v &amp; L . 1 = 'X' s1 &amp; L . (len L) = s2 &amp; 1 <= m &amp; m < len L &amp; CastNode ((L . (m + 1)),v) is_succ_of CastNode ((L . m),v),F )
proofend;

theorem Th39: :: MODELC_3:39
for H, v being LTL-formula
for s2, s1 being strict elementary LTLnode over v st s2 is_next_of s1 &amp; H is Release &amp; H in the LTLold of s2 &amp; not the_left_argument_of H in the LTLold of s2 holds
( the_right_argument_of H in the LTLold of s2 &amp; H in the LTLnext of s2 )
proofend;

theorem Th40: :: MODELC_3:40
for H, v being LTL-formula
for s2, s1 being strict elementary LTLnode over v st s2 is_next_of s1 &amp; H is Release &amp; H in the LTLnext of s1 holds
( the_right_argument_of H in the LTLold of s2 &amp; H in the LTLold of s2 )
proofend;

theorem Th41: :: MODELC_3:41
for H, v being LTL-formula
for s1, s0 being strict elementary LTLnode over v st s1 is_next_of s0 &amp; H in the LTLold of s1 holds
( ( H is conjunctive implies ( the_left_argument_of H in the LTLold of s1 &amp; the_right_argument_of H in the LTLold of s1 ) ) &amp; ( ( not H is disjunctive &amp; 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 ) &amp; ( H is next implies the_argument_of H in the LTLnext of s1 ) &amp; ( H is Release implies the_right_argument_of H in the LTLold of s1 ) )
proofend;

Lm30:  for F, G, v being LTL-formula
for s1, s0, s2 being strict elementary LTLnode over v st s1 is_next_of s0 &amp; s2 is_next_of s1 &amp; F 'U' G in the LTLold of s1 &amp; not G in the LTLold of s1 holds
( F in the LTLold of s1 &amp; F 'U' G in the LTLold of s2 )
proofend;

theorem :: MODELC_3:42
for H, v being LTL-formula
for s1, s0, s2 being strict elementary LTLnode over v st s1 is_next_of s0 &amp; s2 is_next_of s1 &amp; H in the LTLold of s1 &amp; H is Until &amp; not the_right_argument_of H in the LTLold of s1 holds
( the_left_argument_of H in the LTLold of s1 &amp; H in the LTLold of s2 )
proofend;

definition
let v be LTL-formula;
func LTLNodes v ->  non empty set  means :Def30: :: MODELC_3:def 30
 for x being set holds
( x in it iff ex N being strict LTLnode over v st x = N );
existence
 ex b1 being non empty set st
for x being set holds
( x in b1 iff ex N being strict LTLnode over v st x = N )
proofend;
uniqueness
 for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff ex N being strict LTLnode over v st x = N ) ) &amp; ( for x being set holds
( x in b2 iff ex N being strict LTLnode over v st x = N ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def30 defines LTLNodes MODELC_3:def_30_:_
 for v being LTL-formula
for b2 being non empty set holds
( b2 = LTLNodes v iff for x being set holds
( x in b2 iff ex N being strict LTLnode over v st x = N ) );

registration
let v be LTL-formula;
cluster LTLNodes v ->  non empty finite ;
correctness
coherence
LTLNodes v is finite ;
proofend;
end;

definition
let v be LTL-formula;
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  }  is non empty set
proofend;
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  }  ;

registration
let v be LTL-formula;
cluster LTLStates v ->  non empty finite ;
correctness
coherence
LTLStates v is finite ;
proofend;
end;

theorem :: MODELC_3:43
for v being LTL-formula holds init v is Element of LTLStates v
proofend;

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

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

Lm31:  for n being Nat
for X being set st X <> {} &amp; X c= Seg n holds
ex k being Nat st
( 1 <= k &amp; k <= n &amp; k in X &amp; ( for i being Nat st 1 <= i &amp; i < k holds
not i in X ) )
proofend;

definition
let v be LTL-formula;
let w be Element of Inf_seq AtomicFamily;
let f be Function;
predf is_succ_homomorphism v,w means :Def32: :: MODELC_3:def 32
 for x being set st x in LTLNodes v &amp; not CastNode (x,v) is elementary &amp; w |= * (CastNode (x,v)) holds
( CastNode ((f . x),v) is_succ_of CastNode (x,v) &amp; w |= * (CastNode ((f . x),v)) );
predf is_homomorphism v,w means :Def33: :: MODELC_3:def 33
 for x being set st x in LTLNodes v &amp; not CastNode (x,v) is elementary &amp; w |= * (CastNode (x,v)) holds
w |= * (CastNode ((f . x),v));
end;

:: deftheorem Def32 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 &amp; not CastNode (x,v) is elementary &amp; w |= * (CastNode (x,v)) holds
( CastNode ((f . x),v) is_succ_of CastNode (x,v) &amp; w |= * (CastNode ((f . x),v)) ) );

:: deftheorem Def33 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 &amp; not CastNode (x,v) is elementary &amp; w |= * (CastNode (x,v)) holds
w |= * (CastNode ((f . x),v)) );

theorem Th46: :: 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
proofend;

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 &amp; not CastNode (x,v) is elementary &amp; 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))
proofend;

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 &amp; not CastNode (x,v) is elementary &amp; 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) &amp; w |= * (CastNode (((f |** k) . x),v)) )
proofend;

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 &amp; not CastNode (x,v) is elementary &amp; 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 ) &amp; CastNode (((f |** n) . x),v) is elementary )
proofend;

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 &amp; not CastNode (x,v) is elementary holds
for k being Nat st not CastNode (((f |** k) . x),v) is elementary &amp; w |= * (CastNode (((f |** k) . x),v)) holds
w |= * (CastNode (((f |** (k + 1)) . x),v))
proofend;

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 &amp; not CastNode (x,v) is elementary &amp; 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 &amp; CastNode (((f |** (i + 1)) . x),v) is_succ_of CastNode (((f |** i) . x),v) ) ) &amp; CastNode (((f |** n) . x),v) is elementary &amp; ( for i being Nat st i <= n holds
w |= * (CastNode (((f |** i) . x),v)) ) )
proofend;

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

Lm32:  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)) &amp; ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) &amp; ( for i being Nat st 1 <= i &amp; i < n holds
not G in the LTLold of (CastNode ((q . i),v)) ) holds
for i being Nat st 1 <= i &amp; i < n holds
( F in the LTLold of (CastNode ((q . i),v)) &amp; F 'U' G in the LTLold of (CastNode ((q . i),v)) )
proofend;

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 &amp; H in the LTLold of (CastNode ((q . 1),v)) &amp; ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) &amp; ( for i being Nat st 1 <= i &amp; 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 &amp; i < n holds
( the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) &amp; H in the LTLold of (CastNode ((q . i),v)) )
proofend;

Lm33:  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)) &amp; ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) &amp; ex i being Nat st
( i >= 1 &amp; not ( F 'U' G in the LTLold of (CastNode ((q . i),v)) &amp; F in the LTLold of (CastNode ((q . i),v)) &amp; not G in the LTLold of (CastNode ((q . i),v)) ) ) holds
ex j being Nat st
( j >= 1 &amp; G in the LTLold of (CastNode ((q . j),v)) &amp; ( for i being Nat st 1 <= i &amp; i < j holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) &amp; F in the LTLold of (CastNode ((q . i),v)) ) ) )
proofend;

theorem Th54: :: MODELC_3:54
for H, v being LTL-formula
for q being sequence of (LTLStates v) st H is Until &amp; H in the LTLold of (CastNode ((q . 1),v)) &amp; ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) &amp; ex i being Nat st
( i >= 1 &amp; not ( H in the LTLold of (CastNode ((q . i),v)) &amp; the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) &amp; not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) holds
ex j being Nat st
( j >= 1 &amp; the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) &amp; ( for i being Nat st 1 <= i &amp; i < j holds
( H in the LTLold of (CastNode ((q . i),v)) &amp; the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) )
proofend;

::some properties for choice function
theorem Th55: :: MODELC_3:55
for X being set holds union (BOOL X) = X
proofend;

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 <> {} &amp; the LTLnew of N in BOOL (Subformulae v) )
proofend;

registration
let v be LTL-formula;
cluster union (BOOL (Subformulae v)) ->  non empty ;
correctness
coherence
not union (BOOL (Subformulae v)) is empty ;
by Th55;
cluster BOOL (Subformulae v) ->  non empty ;
correctness
coherence
not BOOL (Subformulae v) is empty ;
;
end;

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

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 ;
func chosen_formula (U,N) ->  LTL-formula equals :Def34: :: MODELC_3:def 34
U . the LTLnew of N;
correctness
coherence
U . the LTLnew of N is LTL-formula;
proofend;
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;

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

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;
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 &amp; w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until &amp; w |/= the_right_argument_of (chosen_formula (U,N)) ) )
otherwise  SuccNode2 ((chosen_formula (U,N)),N);
correctness
coherence
( ( ( ( not chosen_formula (U,N) is Until &amp; w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until &amp; w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies SuccNode1 ((chosen_formula (U,N)),N) is strict LTLnode over v ) &amp; ( ( not chosen_formula (U,N) is Until &amp; w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until &amp; w |/= the_right_argument_of (chosen_formula (U,N)) ) or SuccNode2 ((chosen_formula (U,N)),N) is strict LTLnode over v ) );
consistency
for b1 being strict LTLnode over v holds verum;
;
end;

:: 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 &amp; w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until &amp; w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies chosen_succ (w,v,U,N) = SuccNode1 ((chosen_formula (U,N)),N) ) &amp; ( ( not chosen_formula (U,N) is Until &amp; w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until &amp; 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 &amp; not N is elementary holds
( w |= * (chosen_succ (w,v,U,N)) &amp; chosen_succ (w,v,U,N) is_succ_of N )
proofend;

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 &amp; chosen_formula (U,N) is Until &amp; 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 ) &amp; chosen_formula (U,N) in the LTLold of (chosen_succ (w,v,U,N)) )
proofend;

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 &amp; not N is elementary holds
( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) &amp; the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )
proofend;

definition
let w be Element of Inf_seq AtomicFamily;
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
 ex b1 being Function of (LTLNodes v),(LTLNodes v) st
for x being set st x in LTLNodes v holds
b1 . x = chosen_succ (w,v,U,(CastNode (x,v)))
proofend;
uniqueness
 for b1, b2 being Function of (LTLNodes v),(LTLNodes v) st ( for x being set st x in LTLNodes v holds
b1 . x = chosen_succ (w,v,U,(CastNode (x,v))) ) &amp; ( for x being set st x in LTLNodes v holds
b2 . x = chosen_succ (w,v,U,(CastNode (x,v))) ) holds
b1 = b2
proofend;
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 b4 being Function of (LTLNodes v),(LTLNodes v) holds
( b4 = choice_succ_func (w,v,U) iff for x being set st x in LTLNodes v holds
b4 . x = chosen_succ (w,v,U,(CastNode (x,v))) );

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

begin

definition
let H be LTL-formula;
attrH is neg-inner-most  means :Def37: :: MODELC_3:def 37
 for G being LTL-formula st G is_subformula_of H &amp; G is negative holds
the_argument_of G is atomic ;
end;

:: deftheorem Def37 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 &amp; G is negative holds
the_argument_of G is atomic );

registration
cluster Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() neg-inner-most for FinSequence of NAT ;
existence
 ex b1 being LTL-formula st b1 is neg-inner-most
proofend;
end;

definition
let H be LTL-formula;
attrH is Sub_atomic  means :Def38: :: MODELC_3:def 38
( H is atomic or ex G being LTL-formula st
( G is atomic &amp; H = 'not' G ) );
end;

:: deftheorem Def38 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 &amp; H = 'not' G ) ) );

theorem Th63: :: MODELC_3:63
for H, F being LTL-formula st H is neg-inner-most &amp; F is_subformula_of H holds
F is neg-inner-most
proofend;

theorem Th64: :: MODELC_3:64
for H being LTL-formula holds
( H is Sub_atomic iff ( H is atomic or ( H is negative &amp; the_argument_of H is atomic ) ) )
proofend;

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

theorem :: MODELC_3:66
for H being LTL-formula st H is next &amp; H is neg-inner-most holds
the_argument_of H is neg-inner-most
proofend;

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 ) &amp; H is neg-inner-most holds
( the_left_argument_of H is neg-inner-most &amp; the_right_argument_of H is neg-inner-most )
proofend;

begin

definition
let W be non empty set ;
attrc2 is strict ;
struct BuchiAutomaton over W ->  1-sorted ;
aggrBuchiAutomaton(# carrier, Tran, InitS, FinalS #) ->  BuchiAutomaton over W;
sel Tran c2 ->  Relation of [: the carrier of c2,W:], the carrier of c2;
sel InitS c2 ->  Element of bool the carrier of c2;
sel FinalS c2 ->  Subset of (bool the carrier of c2);
end;

definition
let W be non empty set ;
let B be BuchiAutomaton over W;
let w be Element of Inf_seq W;
predw is-accepted-by B means :Def39: :: MODELC_3:def 39
 ex run being sequence of the carrier of B st
( run . 0 in the InitS of B &amp; ( for i being Nat holds
( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B &amp; ( 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 ) ) ) );
end;

:: deftheorem Def39 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 &amp; ( for i being Nat holds
( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B &amp; ( 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;
func atomic_LTL N ->  Subset of LTL_WFF equals :: MODELC_3:def 40
 {  x where x is LTL-formula : ( x is atomic &amp; x in the LTLold of N )  }  ;
correctness
coherence
{  x where x is LTL-formula : ( x is atomic &amp; x in the LTLold of N )  }  is Subset of LTL_WFF;
proofend;
func Neg_atomic_LTL N ->  Subset of LTL_WFF equals :: MODELC_3:def 41
 {  x where x is LTL-formula : ( x is atomic &amp; 'not' x in the LTLold of N )  }  ;
correctness
coherence
{  x where x is LTL-formula : ( x is atomic &amp; 'not' x in the LTLold of N )  }  is Subset of LTL_WFF;
proofend;
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 &amp; 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 &amp; 'not' x in the LTLold of N )  }  ;

definition
let v be neg-inner-most LTL-formula;
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 &amp; Neg_atomic_LTL N misses x )  }  ;
correctness
coherence
{  x where x is Subset of atomic_LTL : ( atomic_LTL N c= x &amp; Neg_atomic_LTL N misses x )  }  is set ;
;
end;

:: 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 &amp; Neg_atomic_LTL N misses x )  }  ;

definition
let v be neg-inner-most LTL-formula;
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] &amp; s1 is_next_of s &amp; x in Label_ s1 )  }  ;
correctness
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] &amp; s1 is_next_of s &amp; x in Label_ s1 )  }  is Relation of [:(LTLStates v),AtomicFamily:],(LTLStates v);
proofend;
func InitS_LTL v ->  Element of bool (LTLStates v) equals :: MODELC_3:def 44
{(init v)};
correctness
coherence
{(init v)} is Element of bool (LTLStates v);
proofend;
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] &amp; s1 is_next_of s &amp; 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)};

definition
let v be neg-inner-most LTL-formula;
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
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);
proofend;
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)) )  }  ;

definition
let v be neg-inner-most LTL-formula;
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 &amp; F is Until &amp; x = FinalS_LTL (F,v) )  }  ;
correctness
coherence
{  x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v &amp; F is Until &amp; x = FinalS_LTL (F,v) )  }  is Subset of (bool (LTLStates v));
proofend;
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 &amp; F is Until &amp; x = FinalS_LTL (F,v) )  }  ;

definition
let v be neg-inner-most LTL-formula;
func BAutomaton v ->  BuchiAutomaton over AtomicFamily  equals :: MODELC_3:def 47
 BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);
correctness
coherence
BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #) is BuchiAutomaton over AtomicFamily ;
;
end;

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

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

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 ;
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 &amp; CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) &amp; CastNode ((((choice_succ_func (w,v,U)) |** it) . N),v) is elementary &amp; ( for i being Nat st i <= it holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) );
existence
 ex b1 being Nat st
( ( for i being Nat st i < b1 holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary &amp; CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) &amp; CastNode ((((choice_succ_func (w,v,U)) |** b1) . N),v) is elementary &amp; ( for i being Nat st i <= b1 holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) )
proofend;
uniqueness
 for b1, b2 being Nat st ( for i being Nat st i < b1 holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary &amp; CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) &amp; CastNode ((((choice_succ_func (w,v,U)) |** b1) . N),v) is elementary &amp; ( for i being Nat st i <= b1 holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) &amp; ( for i being Nat st i < b2 holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary &amp; CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) &amp; CastNode ((((choice_succ_func (w,v,U)) |** b2) . N),v) is elementary &amp; ( for i being Nat st i <= b2 holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) holds
b1 = b2
proofend;
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 &amp; w |= * N holds
for b5 being Nat holds
( b5 = chosen_succ_end_num (w,v,U,N) iff ( ( for i being Nat st i < b5 holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary &amp; CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) &amp; CastNode ((((choice_succ_func (w,v,U)) |** b5) . N),v) is elementary &amp; ( for i being Nat st i <= b5 holds
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) ;
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
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 ) &amp; ( 'X' N is elementary implies FinalNode v is strict elementary LTLnode over v ) );
consistency
for b1 being strict elementary LTLnode over v holds verum;
by A1, Def48;
end;

:: 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) ) &amp; ( '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 &amp; w |= * (chosen_next (w,v,U,s)) )
proofend;

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);
func chosen_run (w,v,U) ->  sequence of (LTLStates v) means :Def50: :: MODELC_3:def 50
( it . 0 = init v &amp; ( for n being Nat holds it . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((it . n),v))) ) );
existence
 ex b1 being sequence of (LTLStates v) st
( b1 . 0 = init v &amp; ( for n being Nat holds b1 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b1 . n),v))) ) )
proofend;
uniqueness
 for b1, b2 being sequence of (LTLStates v) st b1 . 0 = init v &amp; ( for n being Nat holds b1 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b1 . n),v))) ) &amp; b2 . 0 = init v &amp; ( for n being Nat holds b2 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b2 . n),v))) ) holds
b1 = b2
proofend;
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 b4 being sequence of (LTLStates v) holds
( b4 = chosen_run (w,v,U) iff ( b4 . 0 = init v &amp; ( for n being Nat holds b4 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b4 . n),v))) ) ) );

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

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

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

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

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) &amp; Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) )
proofend;

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)) &amp; H is Until &amp; 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))
proofend;

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

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;