:: Model Checking, Part {III}
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Copyright (c) 2008-2021 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 ()

by ;

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

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
is Subset of ()

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
( is Subset of () & is Subset of () )

proof end;

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

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

proof end;

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

:: definition of basic operations to build an automaton for LTL.
definition
let H be LTL-formula;
func LTLNew1 H -> Subset of () equals :Def1: :: MODELC_3:def 1
if H is conjunctive
if H is disjunctive
{} if H is next
if H is Until
if H is Release
otherwise {} ;
correctness
coherence
( ( H is conjunctive implies is Subset of () ) & ( H is disjunctive implies is Subset of () ) & ( H is next implies {} is Subset of () ) & ( H is Until implies is Subset of () ) & ( H is Release implies is Subset of () ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of () ) )
;
consistency
for b1 being Subset of () holds
( ( H is conjunctive & H is disjunctive implies ( b1 = iff b1 = ) ) & ( H is conjunctive & H is next implies ( b1 = iff b1 = {} ) ) & ( H is conjunctive & H is Until implies ( b1 = iff b1 = ) ) & ( H is conjunctive & H is Release implies ( b1 = iff b1 = ) ) & ( H is disjunctive & H is next implies ( b1 = iff b1 = {} ) ) & ( H is disjunctive & H is Until implies ( b1 = iff b1 = ) ) & ( H is disjunctive & H is Release implies ( b1 = iff b1 = ) ) & ( H is next & H is Until implies ( b1 = {} iff b1 = ) ) & ( H is next & H is Release implies ( b1 = {} iff b1 = ) ) & ( H is Until & H is Release implies ( b1 = iff b1 = ) ) )
;
by ;
func LTLNew2 H -> Subset of () equals :Def2: :: MODELC_3:def 2
{} if H is conjunctive
if H is disjunctive
{} if H is next
if H is Until
if H is Release
otherwise {} ;
correctness
coherence
( ( H is conjunctive implies {} is Subset of () ) & ( H is disjunctive implies is Subset of () ) & ( H is next implies {} is Subset of () ) & ( H is Until implies is Subset of () ) & ( H is Release implies is Subset of () ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of () ) )
;
consistency
for b1 being Subset of () holds
( ( H is conjunctive & H is disjunctive implies ( b1 = {} iff b1 = ) ) & ( H is conjunctive & H is next implies ( b1 = {} iff b1 = {} ) ) & ( H is conjunctive & H is Until implies ( b1 = {} iff b1 = ) ) & ( H is conjunctive & H is Release implies ( b1 = {} iff b1 = ) ) & ( H is disjunctive & H is next implies ( b1 = iff b1 = {} ) ) & ( H is disjunctive & H is Until implies ( b1 = iff b1 = ) ) & ( H is disjunctive & H is Release implies ( b1 = iff b1 = ) ) & ( H is next & H is Until implies ( b1 = {} iff b1 = ) ) & ( H is next & H is Release implies ( b1 = {} iff b1 = ) ) & ( H is Until & H is Release implies ( b1 = iff b1 = ) ) )
;
by ;
func LTLNext H -> Subset of () equals :Def3: :: MODELC_3:def 3
{} if H is conjunctive
{} if H is disjunctive
if H is next
{H} if H is Until
{H} if H is Release
otherwise {} ;
correctness
coherence
( ( H is conjunctive implies {} is Subset of () ) & ( H is disjunctive implies {} is Subset of () ) & ( H is next implies is Subset of () ) & ( H is Until implies {H} is Subset of () ) & ( H is Release implies {H} is Subset of () ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of () ) )
;
consistency
for b1 being Subset of () holds
( ( H is conjunctive & H is disjunctive implies ( b1 = {} iff b1 = {} ) ) & ( H is conjunctive & H is next implies ( b1 = {} iff b1 = ) ) & ( H is conjunctive & H is Until implies ( b1 = {} iff b1 = {H} ) ) & ( H is conjunctive & H is Release implies ( b1 = {} iff b1 = {H} ) ) & ( H is disjunctive & H is next implies ( b1 = {} iff b1 = ) ) & ( H is disjunctive & H is Until implies ( b1 = {} iff b1 = {H} ) ) & ( H is disjunctive & H is Release implies ( b1 = {} iff b1 = {H} ) ) & ( H is next & H is Until implies ( b1 = iff b1 = {H} ) ) & ( H is next & H is Release implies ( b1 = iff b1 = {H} ) ) & ( H is Until & H is Release implies ( b1 = {H} iff b1 = {H} ) ) )
;
by ;
end;

:: deftheorem Def1 defines LTLNew1 MODELC_3:def 1 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNew1 H = ) & ( H is disjunctive implies LTLNew1 H = ) & ( H is next implies LTLNew1 H = {} ) & ( H is Until implies LTLNew1 H = ) & ( H is Release implies LTLNew1 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 = ) & ( H is next implies LTLNew2 H = {} ) & ( H is Until implies LTLNew2 H = ) & ( H is Release implies LTLNew2 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 = ) & ( 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 c2 is strict ;
struct LTLnode over v -> ;
aggr LTLnode(# LTLold, LTLnew, LTLnext #) -> LTLnode over v;
sel LTLold c2 -> Subset of ();
sel LTLnew c2 -> Subset of ();
sel LTLnext c2 -> Subset of ();
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} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & 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} & the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & the LTLnext of b1 = the LTLnext of N \/ () )
proof end;
uniqueness
for b1, b2 being strict LTLnode over v st the LTLold of b1 = the LTLold of N \/ {H} & the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & the LTLnext of b1 = the LTLnext of N \/ () & the LTLold of b2 = the LTLold of N \/ {H} & the LTLnew of b2 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & the LTLnext of b2 = the LTLnext of N \/ () 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} & the LTLnew of b4 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & the LTLnext of b4 = the LTLnext of N \/ () ) );

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} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & 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} & the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & the LTLnext of b1 = the LTLnext of N )
proof end;
uniqueness
for b1, b2 being strict LTLnode over v st the LTLold of b1 = the LTLold of N \/ {H} & the LTLnew of b1 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & the LTLnext of b1 = the LTLnext of N & the LTLold of b2 = the LTLold of N \/ {H} & the LTLnew of b2 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & 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} & the LTLnew of b4 = ( the LTLnew of N \ {H}) \/ (() \ the LTLold of N) & 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;
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) ) ) );
end;

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

definition
let v be LTL-formula;
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) );
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) );
end;

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

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

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

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

definition
let v be LTL-formula;
let N be LTLnode over v;
attr N is failure means :: MODELC_3:def 10
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 );
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 & F = 'not' H & H in the LTLold of N & F in the LTLold of N ) );

definition
let v be LTL-formula;
let N be LTLnode over v;
attr N 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;
attr N is final means :: MODELC_3:def 12
( N is elementary & 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 & the LTLnext of N = {} ) );

definition
let v be LTL-formula;
func {} v -> Subset of () equals :: MODELC_3:def 13
{} ;
correctness
coherence
{} is Subset of ()
;
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 () equals :: MODELC_3:def 14
{v};
correctness
coherence
{v} is Subset of ()
;
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 & b1 is strict )
proof end;
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 object ;
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 ) & ( 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 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;
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;
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 );
end;

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

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

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

definition
let v be LTL-formula;
let W be Subset of ();
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 () 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
;
proof end;
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 & ( 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
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 atomic or H is negative or H is conjunctive or H is next ) holds
( w |= * N iff w |= * (SuccNode1 (H,N)) ) by ;

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

Lm21: for H being LTL-formula st ( H is negative or H is next ) holds
Subformulae 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 = () \/ {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 () holds not {} in W

proof end;

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

registration
let H be LTL-formula;
correctness
coherence ;
proof end;
end;

definition
let H be LTL-formula;
let W be Subset of ();
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 ) & ( 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 ()
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 ();
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
ex b1 being Real_Sequence st
for k being Nat holds
( ( L . k in W implies b1 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b1 . k = 0 ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for k being Nat holds
( ( L . k in W implies b1 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b1 . k = 0 ) ) ) & ( for k being Nat holds
( ( L . k in W implies b2 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b2 . k = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines Partial_seq MODELC_3:def 24 :
for H being LTL-formula
for W being Subset of ()
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)) ) & ( not L . k in W implies b4 . k = 0 ) ) );

definition
let H be LTL-formula;
let W be Subset of ();
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 ()
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 Th4: :: MODELC_3:4
for L being FinSequence
for H being LTL-formula holds len (L,({} H)) = 0
proof end;

theorem Th5: :: MODELC_3:5
for L being FinSequence
for F, H being LTL-formula
for W being Subset of () 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 () 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 () 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 () 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 ();
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 b1 being Real ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & b1 = len (L,W) )
proof end;
uniqueness
for b1, b2 being Real st ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & b1 = len (L,W) ) & ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & 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 ()
for b3 being Real holds
( b3 = len W iff ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & b3 = len (L,W) ) );

theorem :: MODELC_3:9
for F, H being LTL-formula
for W being Subset of () 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 () 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 () 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 () st W1 = W \/ {F} holds
len W1 <= (len W) + (len F)
proof end;

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

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

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

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

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

theorem Th18: :: MODELC_3:18
for H being LTL-formula
for W, W1, W2 being Subset of () 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 ;
func LTLNew1 (H,v) -> Subset of () equals :Def27: :: MODELC_3:def 27
LTLNew1 H;
correctness
coherence
LTLNew1 H is Subset of ()
;
proof end;
func LTLNew2 (H,v) -> Subset of () equals :Def28: :: MODELC_3:def 28
LTLNew2 H;
correctness
coherence
LTLNew2 H is Subset of ()
;
proof end;
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;

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

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

definition
let v be LTL-formula;
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
ex b1 being non empty set st
for x being object holds
( x in b1 iff ex N being strict LTLnode over v st x = N )
proof end;
uniqueness
for b1, b2 being non empty set st ( for x being object holds
( x in b1 iff ex N being strict LTLnode over v st x = N ) ) & ( for x being object holds
( x in b2 iff ex N being strict LTLnode over v st x = N ) ) holds
b1 = b2
proof end;
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 object 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 ;
proof end;
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
proof end;
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 ;
proof end;
end;

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

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

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

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

theorem :: MODELC_3:46
for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (),() 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 (),() 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 (),() 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 (),() 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 (),() 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 (),() 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 () 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 () 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 () 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 () 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 () 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 Th55: :: MODELC_3:55
for X being set holds union (BOOL X) = X
proof end;

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 () ) by ORDERS_1:2;

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

theorem :: MODELC_3:57
for v being LTL-formula ex f being Choice_Function of (BOOL ()) st f is Function of (BOOL ()),()
proof end;

definition
let v be LTL-formula;
let U be Choice_Function of (BOOL ());
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
;
proof end;
end;

:: deftheorem Def34 defines chosen_formula MODELC_3:def 34 :
for v being LTL-formula
for U being Choice_Function of (BOOL ())
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 ()) 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 ());
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
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 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 ())
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 ()) 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 ()) 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 ()) 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 ());
func choice_succ_func (w,v,U) -> Function of (),() 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 (),() st
for x being set st x in LTLNodes v holds
b1 . x = chosen_succ (w,v,U,(CastNode (x,v)))
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being set st x in LTLNodes v holds
b1 . x = chosen_succ (w,v,U,(CastNode (x,v))) ) & ( for x being set st x in LTLNodes v holds
b2 . x = chosen_succ (w,v,U,(CastNode (x,v))) ) holds
b1 = b2
proof end;
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 ())
for b4 being Function of (),() 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 ()) holds choice_succ_func (w,v,U) is_succ_homomorphism v,w
proof end;

definition
let H be LTL-formula;
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 ;
end;

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

registration
existence
ex b1 being LTL-formula st b1 is neg-inner-most
proof end;
end;

definition
let H be LTL-formula;
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 ) );
end;

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

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;

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

definition
let W be non empty set ;
attr c2 is strict ;
struct BuchiAutomaton over W -> 1-sorted ;
aggr BuchiAutomaton(# 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;
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 ) ) ) );
end;

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

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 & x in the LTLold of N ) } ;
correctness
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
coherence
{ x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } is Subset of LTL_WFF
;
proof end;
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 ) } ;

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

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 & Neg_atomic_LTL N misses x ) } ;
correctness
coherence
{ x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & 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 & Neg_atomic_LTL N misses x ) } ;

definition
let v be neg-inner-most LTL-formula;
func Tran_LTL v -> Relation of ,() equals :: MODELC_3:def 43
{ y where y is Element of [:(),AtomicFamily,():] : 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
coherence
{ y where y is Element of [:(),AtomicFamily,():] : 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 ,()
;
proof end;
func InitS_LTL v -> Element of bool () equals :: MODELC_3:def 44
{(init v)};
correctness
coherence
{(init v)} is Element of bool ()
;
proof end;
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 [:(),AtomicFamily,():] : 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)};

definition
let v be neg-inner-most LTL-formula;
let F be LTL-formula;
func FinalS_LTL (F,v) -> Element of bool () 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 ()
;
proof end;
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 ()) equals :: MODELC_3:def 46
{ x where x is Element of bool () : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) )
}
;
correctness
coherence
{ x where x is Element of bool () : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) )
}
is Subset of (bool ())
;
proof end;
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 () : 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;
func BAutomaton v -> BuchiAutomaton over AtomicFamily equals :: MODELC_3:def 47
BuchiAutomaton(# (),(),(),() #);
correctness
coherence
BuchiAutomaton(# (),(),(),() #) is BuchiAutomaton over AtomicFamily
;
;
end;

:: deftheorem defines BAutomaton MODELC_3:def 47 :
for v being neg-inner-most LTL-formula holds BAutomaton v = BuchiAutomaton(# (),(),(),() #);

::************
:: 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
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 ());
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
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 & 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)) |** b1) . N),v) is elementary & ( for i being Nat st i <= b1 holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) )
proof end;
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 & 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)) |** b1) . N),v) is elementary & ( for i being Nat st i <= b1 holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) & ( for i being Nat st i < b2 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)) |** b2) . N),v) is elementary & ( for i being Nat st i <= b2 holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) holds
b1 = b2
proof end;
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 ())
for N being strict LTLnode over v st not N is elementary & 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 & 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)) |** b5) . N),v) is elementary & ( 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 ());
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 ) & ( '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 ;
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 ())
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 ())
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 ());
func chosen_run (w,v,U) -> sequence of () 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
ex b1 being sequence of () st
( b1 . 0 = init v & ( for n being Nat holds b1 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b1 . n),v))) ) )
proof end;
uniqueness
for b1, b2 being sequence of () st b1 . 0 = init v & ( for n being Nat holds b1 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b1 . n),v))) ) & b2 . 0 = init v & ( for n being Nat holds b2 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b2 . n),v))) ) holds
b1 = b2
proof end;
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 ())
for b4 being sequence of () holds
( b4 = chosen_run (w,v,U) iff ( b4 . 0 = init v & ( for n being Nat holds b4 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b4 . n),v))) ) ) );

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