MODELC_3: Model Checking, Part {III}

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

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 number st r1 <= r2 holds
[\r1/] <= [\r2/]

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm11: for H being LTL-formula st ( H is disjunctive or H is conjunctive or H is Until or H is Release ) holds
{(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H)

proof end;

Lm12: for H being LTL-formula st ( H is disjunctive or H is conjunctive or H is Until or H is Release ) holds
( {(the_left_argument_of H)} is Subset of (Subformulae H) & {(the_right_argument_of H)} is Subset of (Subformulae H) )

proof end;

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

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

proof end;

definition

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

proof end;

end;

definition

end;

:: deftheorem Def1 defines LTLNew1 MODELC_3:def 1 :

:: deftheorem Def2 defines LTLNew2 MODELC_3:def 2 :

:: deftheorem Def3 defines LTLNext MODELC_3:def 3 :

definition

let v be LTL-formula;
attr c₂ is strict ;
struct LTLnode of v -> ;
aggr LTLnode(# LTLold, LTLnew, LTLnext #) -> LTLnode of v;
sel LTLold c₂ -> Subset of (Subformulae v);
sel LTLnew c₂ -> Subset of (Subformulae v);
sel LTLnext c₂ -> Subset of (Subformulae v);

end;

definition

let v be LTL-formula;
let N be LTLnode of v;
let H be LTL-formula;
assume A1: H in the LTLnew of N ;
func SuccNode1 H,N -> strict LTLnode of v means :Def4: :: MODELC_3:def 4
( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N \/ (LTLNext H) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines SuccNode1 MODELC_3:def 4 :

definition

let v be LTL-formula;
let N be LTLnode of v;
let H be LTL-formula;
assume A1: H in the LTLnew of N ;
func SuccNode2 H,N -> strict LTLnode of v means :Def5: :: MODELC_3:def 5
( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = (the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines SuccNode2 MODELC_3:def 5 :

definition

let v be LTL-formula;
let N1, N2 be LTLnode of v;
let H be LTL-formula;
pred N2 is_succ_of N1,H means :Def6: :: 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 Def6 defines is_succ_of MODELC_3:def 6 :

definition

let v be LTL-formula;
let N1, N2 be LTLnode of v;
pred N2 is_succ1_of N1 means :Def7: :: 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 :Def8: :: 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 Def7 defines is_succ1_of MODELC_3:def 7 :

:: deftheorem Def8 defines is_succ2_of MODELC_3:def 8 :

definition

let v be LTL-formula;
let N1, N2 be LTLnode of v;
pred N2 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 :

definition

let v be LTL-formula;
let N be LTLnode of 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 :

definition

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

end;

:: deftheorem Def11 defines elementary MODELC_3:def 11 :

definition

let v be LTL-formula;
let N be LTLnode of 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 :

definition

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

end;

:: deftheorem defines {} MODELC_3:def 13 :

definition

let v be LTL-formula;
func Seed v -> Subset of (Subformulae v) equals :: MODELC_3:def 14
{v};
correctness by Lm9, MODELC_2:27;

end;

:: deftheorem defines Seed MODELC_3:def 14 :

registration

let v be LTL-formula;
cluster strict elementary LTLnode of v;
existence

proof end;

end;

definition

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

end;

:: deftheorem defines FinalNode MODELC_3:def 15 :

definition

let x be set ;
let v be LTL-formula;
func CastNode x,v -> strict LTLnode of v equals :Def16: :: MODELC_3:def 16
x if x is strict LTLnode of v
otherwise LTLnode(# ({} v),({} v),({} v) #);
correctness ;

end;

:: deftheorem Def16 defines CastNode MODELC_3:def 16 :

definition

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

end;

:: deftheorem defines init MODELC_3:def 17 :

definition

let v be LTL-formula;
let N be LTLnode of v;
func 'X' N -> strict LTLnode of v equals :: MODELC_3:def 18
LTLnode(# ({} v),the LTLnext of N,({} v) #);
correctness ;

end;

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

definition

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

end;

:: deftheorem Def19 defines is_Finseq_for MODELC_3:def 19 :

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 of v;
pred N2 is_next_of N1 means :Def20: :: 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 Def20 defines is_next_of MODELC_3:def 20 :

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 by MODELC_2:47;

end;

:: deftheorem defines CastLTL MODELC_3:def 21 :

definition

let v be LTL-formula;
let N be strict LTLnode of 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

proof end;

end;

:: deftheorem defines * MODELC_3:def 22 :

Lm16: for H, v being LTL-formula
for N being strict LTLnode of 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 of 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 of 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 Lm16, Lm17;

Lm18: for H, v being LTL-formula
for N being strict LTLnode of 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 of 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 of 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 of 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 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}

proof end;

Lm22: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

proof end;

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

proof end;

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

proof end;

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;
cluster Subformulae H -> finite ;
correctness

proof end;

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 ;

end;

:: deftheorem Def23 defines Length_fun MODELC_3:def 23 :

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)) ) & ( not L . k in W implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines Partial_seq MODELC_3:def 24 :

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 ;

end;

:: deftheorem defines len MODELC_3:def 25 :

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

proof end;

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 & 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 H, F being LTL-formula
for W, W1 being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & not F in W & W1 = W \/ {F} holds
len L,W1 = (len L,W) + (len F)

proof end;

theorem Th8: :: MODELC_3:8

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

proof end;

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 & L is one-to-one & it = len L,W );
existence

proof end;

uniqueness by Th8;

end;

:: deftheorem Def26 defines len MODELC_3:def 26 :

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

proof end;

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)

proof end;

theorem Th11: :: MODELC_3:11

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

proof end;

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)

proof end;

theorem Th13: :: MODELC_3:13

for H being LTL-formula holds len ({} H) = 0

proof end;

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

proof end;

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 & W c= W1 \ {x} ) )

proof end;

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

proof end;

theorem Th16: :: MODELC_3:16

for H being LTL-formula
for W being Subset of (Subformulae H) st len W < 1 holds
W = {} H

proof end;

theorem Th17: :: MODELC_3:17

for H being LTL-formula
for W being Subset of (Subformulae H) holds len W >= 0

proof end;

theorem Th18: :: MODELC_3:18

for H being LTL-formula
for W, W1, W2 being Subset of (Subformulae H) st W = W1 \/ W2 holds
len W <= (len W1) + (len W2)

proof end;

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

proof end;

func LTLNew2 H,v -> Subset of (Subformulae v) equals :Def28: :: MODELC_3:def 28
LTLNew2 H;
correctness

proof end;

end;

:: deftheorem Def27 defines LTLNew1 MODELC_3:def 27 :

:: deftheorem Def28 defines LTLNew2 MODELC_3:def 28 :

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

proof end;

Lm29: 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 N2, N1 being strict LTLnode of 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 N2, N1 being strict LTLnode of 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 of v;
func len N -> Nat equals :: MODELC_3:def 29
[\(len the LTLnew of N)/];
correctness

proof end;

end;

:: deftheorem defines len MODELC_3:def 29 :

theorem Th21: :: MODELC_3:21

for v being LTL-formula
for N2, N1 being strict LTLnode of 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 of 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 of 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 of v ex n being Nat ex L being FinSequence ex M being strict LTLnode of 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 N2, N1 being strict LTLnode of 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 N2, N1 being strict LTLnode of 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 N2, N1 being strict LTLnode of 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 m, n 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 N2, N1 being strict LTLnode of 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 s2, s1 being strict elementary LTLnode of 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 s2, s1 being strict elementary LTLnode of 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 s2, s1 being strict elementary LTLnode of 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 s2, s1 being strict elementary LTLnode of 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 s1, s0 being strict elementary LTLnode of 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;

Lm30: for F, G, v being LTL-formula
for s1, s0, s2 being strict elementary LTLnode of 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 s1, s0, s2 being strict elementary LTLnode of 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 set holds
( x in it iff ex N being strict LTLnode of v st x = N );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def30 defines LTLNodes MODELC_3:def 30 :

registration

let v be LTL-formula;
cluster LTLNodes v -> non empty finite ;
correctness

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 of v } ;
coherence

proof end;

end;

:: deftheorem defines LTLStates MODELC_3:def 31 :

registration

let v be LTL-formula;
cluster LTLStates v -> non empty finite ;
correctness

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 of 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 of v st s = x )

proof end;

Lm31: 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 :Def32: :: 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 :Def33: :: 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 Def32 defines is_succ_homomorphism MODELC_3:def 32 :

:: deftheorem Def33 defines is_homomorphism MODELC_3:def 33 :

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

proof end;

theorem Th47: :: MODELC_3:47

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode ((f |** i) . x),v is elementary ) holds
w |= * (CastNode ((f |** k) . x),v)

proof end;

theorem Th48: :: MODELC_3:48

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode ((f |** i) . x),v is elementary ) holds
( CastNode ((f |** (k + 1)) . x),v is_succ_of CastNode ((f |** k) . x),v & w |= * (CastNode ((f |** k) . x),v) )

proof end;

theorem Th49: :: MODELC_3:49

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode ((f |** i) . x),v is elementary ) & CastNode ((f |** n) . x),v is elementary )

proof end;

theorem Th50: :: MODELC_3:50

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary holds
for k being Nat st not CastNode ((f |** k) . x),v is elementary & w |= * (CastNode ((f |** k) . x),v) holds
w |= * (CastNode ((f |** (k + 1)) . x),v)

proof end;

theorem Th51: :: MODELC_3:51

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) )

proof end;

theorem Th52: :: MODELC_3:52

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

proof end;

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

proof end;

theorem :: MODELC_3:53

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

proof end;

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

proof end;

theorem Th54: :: MODELC_3:54

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

proof end;

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 of v st not N is elementary holds
( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) )

proof end;

registration

let v be LTL-formula;
cluster union (BOOL (Subformulae v)) -> non empty ;
correctness by Th55;
cluster BOOL (Subformulae v) -> non empty ;
correctness ;

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)

proof end;

definition

let v be LTL-formula;
let U be Choice_Function of BOOL (Subformulae v);
let N be strict LTLnode of 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

proof end;

end;

:: deftheorem Def34 defines chosen_formula MODELC_3:def 34 :

theorem Th58: :: MODELC_3:58

for v being LTL-formula
for N being strict LTLnode of v
for U being Choice_Function of BOOL (Subformulae v) st not N is elementary holds
chosen_formula U,N in the LTLnew of N

proof end;

definition

let w be Element of Inf_seq AtomicFamily ;
let v be LTL-formula;
let U be Choice_Function of BOOL (Subformulae v);
let N be strict LTLnode of v;
func chosen_succ w,v,U,N -> strict LTLnode of 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 ;

end;

:: deftheorem Def35 defines chosen_succ MODELC_3:def 35 :

theorem Th59: :: MODELC_3:59

for v being LTL-formula
for N being strict LTLnode of v
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) st w |= * N & not N is elementary holds
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

proof end;

theorem :: MODELC_3:60

for v being LTL-formula
for N being strict LTLnode of v
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) st not N is elementary & chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) holds
( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,N) )

proof end;

theorem :: MODELC_3:61

for v being LTL-formula
for N being strict LTLnode of v
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) st w |= * N & not N is elementary holds
( the LTLold of N c= the LTLold of (chosen_succ w,v,U,N) & the LTLnext of N c= the LTLnext of (chosen_succ w,v,U,N) )

proof end;

definition

let w be Element of Inf_seq AtomicFamily ;
let v be LTL-formula;
let U be Choice_Function of BOOL (Subformulae v);
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def36 defines choice_succ_func MODELC_3:def 36 :

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

proof end;

begin

definition

let H be LTL-formula;
attr H is neg-inner-most means :Def37: :: 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 Def37 defines neg-inner-most MODELC_3:def 37 :

registration

cluster Relation-like NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V245() V246() V247() V248() V249() V250() neg-inner-most FinSequence of NAT ;
existence

proof end;

end;

definition

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

end;

:: deftheorem Def38 defines Sub_atomic MODELC_3:def 38 :

theorem Th63: :: MODELC_3:63

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

proof end;

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;

begin

definition

let W be non empty set ;
attr c₂ is strict ;
struct BuchiAutomaton of W -> ;
aggr BuchiAutomaton(# carrier, Tran, InitS, FinalS #) -> BuchiAutomaton of W;
sel carrier c₂ -> set ;
sel Tran c₂ -> Relation of [:the carrier of c₂,W:],the carrier of c₂;
sel InitS c₂ -> Element of bool the carrier of c₂;
sel FinalS c₂ -> Subset of (bool the carrier of c₂);

end;

definition

let W be non empty set ;
let B be BuchiAutomaton of W;
let w be Element of Inf_seq W;
pred w 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 & ( 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 Def39 defines is-accepted-by MODELC_3:def 39 :

definition

let v be neg-inner-most LTL-formula;
let N be strict LTLnode of 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

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

proof end;

end;

:: deftheorem defines atomic_LTL MODELC_3:def 40 :

:: deftheorem defines Neg_atomic_LTL MODELC_3:def 41 :

definition

let v be neg-inner-most LTL-formula;
let N be strict LTLnode of 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 ;

end;

:: deftheorem defines Label_ MODELC_3:def 42 :

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 of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;
correctness

proof end;

func InitS_LTL v -> Element of bool (LTLStates v) equals :: MODELC_3:def 44
{(init v)};
correctness

proof end;

end;

:: deftheorem defines Tran_LTL MODELC_3:def 43 :

:: deftheorem defines InitS_LTL MODELC_3:def 44 :

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

proof end;

end;

:: deftheorem defines FinalS_LTL MODELC_3:def 45 :

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 & F is Until & x = FinalS_LTL F,v ) } ;
correctness

proof end;

end;

:: deftheorem defines FinalS_LTL MODELC_3:def 46 :

definition

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

end;

:: deftheorem defines BAutomaton MODELC_3:def 47 :

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 (Subformulae v);
let N be strict LTLnode of 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def48 defines chosen_succ_end_num MODELC_3:def 48 :

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 of v;
assume A1: w |= * ('X' N) ;
func chosen_next w,v,U,N -> strict elementary LTLnode of 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 by A1, Def48;

end;

:: deftheorem Def49 defines chosen_next MODELC_3:def 49 :

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 of v st w |= * ('X' s) holds
( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )

proof end;

definition

let w be Element of Inf_seq AtomicFamily ;
let v be neg-inner-most LTL-formula;
let U be Choice_Function of BOOL (Subformulae v);
func chosen_run w,v,U -> sequence of (LTLStates v) means :Def50: :: MODELC_3:def 50
( it . 0 = init v & ( for n being Nat holds it . (n + 1) = chosen_next (Shift w,n),v,U,(CastNode (it . n),v) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def50 defines chosen_run MODELC_3:def 50 :

Lm34: 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 of 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 (Subformulae v) st w |= v holds
for n being Nat holds
( CastNode ((chosen_run w,v,U) . (n + 1)),v is_next_of CastNode ((chosen_run w,v,U) . n),v & Shift w,n |= * ('X' (CastNode ((chosen_run w,v,U) . n),v)) )

proof end;

theorem Th74: :: MODELC_3:74

for H being LTL-formula
for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for U being Choice_Function of BOOL (Subformulae v) st w |= v holds
for i being Nat st H in the LTLold of (CastNode ((chosen_run w,v,U) . (i + 1)),v) & H is Until & Shift w,i |= the_right_argument_of H holds
the_right_argument_of H in the LTLold of (CastNode ((chosen_run w,v,U) . (i + 1)),v)

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 Th68, Th75;