MODELC_3: Model Checking, Part {III}

:: Model Checking, Part {III}
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received August 19, 2008
:: 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 (Subformulae H)
by MODELC_2:45, SUBSET_1:41;

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

proof end;

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

proof end;

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

proof end;

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

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

proof end;

definition

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

proof end;

end;

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

definition

let H be LTL-formula;

func LTLNew1 H -> Subset of (Subformulae H) equals :Def1: :: MODELC_3:def 1
{(the_left_argument_of H),(the_right_argument_of H)} if H is conjunctive
{(the_left_argument_of H)} if H is disjunctive
{} if H is next
{(the_left_argument_of H)} if H is Until
{(the_right_argument_of H)} if H is Release
otherwise {} ;

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

func LTLNew2 H -> Subset of (Subformulae H) equals :Def2: :: MODELC_3:def 2
{} if H is conjunctive
{(the_right_argument_of H)} if H is disjunctive
{} if H is next
{(the_right_argument_of H)} if H is Until
{(the_left_argument_of H),(the_right_argument_of H)} if H is Release
otherwise {} ;

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

func LTLNext H -> Subset of (Subformulae H) equals :Def3: :: MODELC_3:def 3
{} if H is conjunctive
{} if H is disjunctive
{(the_argument_of H)} if H is next
{H} if H is Until
{H} if H is Release
otherwise {} ;

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

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 over v -> ;
aggr LTLnode(# LTLold, LTLnew, LTLnext #) -> LTLnode over 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 over v;
let H be LTL-formula;
assume A1: H in the LTLnew of N ;

func SuccNode1 (H,N) -> strict LTLnode over v means :Def4: :: MODELC_3:def 4
( the LTLold of it = the LTLold of N \/ {H} & the LTLnew of it = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of it = the LTLnext of N \/ (LTLNext H) );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines SuccNode1 MODELC_3:def 4 :

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}) \/ ((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 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 :

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 :

:: deftheorem defines is_succ2_of MODELC_3:def 8 :

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 :

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 :

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 :

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 :

definition

let v be LTL-formula;

func {} v -> Subset of (Subformulae v) equals :: MODELC_3:def 13
{} ;

correctness by SUBSET_1:1;

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;

end;

:: deftheorem defines Seed MODELC_3:def 14 :

registration

let v be LTL-formula;

cluster strict elementary for LTLnode over v;

existence

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 by Def11;

end;

:: deftheorem defines FinalNode MODELC_3:def 15 :

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 ;

end;

:: deftheorem Def16 defines CastNode MODELC_3:def 16 :

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 by Def11;

end;

:: deftheorem defines init MODELC_3:def 17 :

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 ;

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

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 :

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

proof end;

end;

:: deftheorem defines * MODELC_3:def 22 :

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 Lm16, Lm17;

Lm18: for H, v being LTL-formula
for N being strict LTLnode over v
for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & 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 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 F, H being LTL-formula
for W being Subset of (Subformulae H) st not F in W holds
len (L,(W \ {F})) = len (L,W)

proof end;

theorem Th6: :: MODELC_3:6

for L being FinSequence
for F, H being LTL-formula
for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds
len (L,(W \ {F})) = (len (L,W)) - (len F)

proof end;

theorem Th7: :: MODELC_3:7

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

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

proof end;

theorem Th12: :: MODELC_3:12

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

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 (Subformulae H) 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 (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 :

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

proof end;

end;

:: deftheorem defines len MODELC_3:def 29 :

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

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

:: deftheorem defines is_homomorphism MODELC_3:def 33 :

theorem :: MODELC_3:46

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
f is_homomorphism v,w ;

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 over v st s = CastNode ((q . n),v)

proof end;

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

proof end;

theorem :: MODELC_3:53

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

proof end;

Lm32: for F, G, v being LTL-formula
for q being sequence of (LTLStates v) st F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ex i being Nat st
( i >= 1 & not ( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) & not G in the LTLold of (CastNode ((q . i),v)) ) ) holds
ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) ) ) )

proof end;

theorem Th54: :: MODELC_3:54

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

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

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

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 over v
for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary holds
chosen_formula (U,N) in the LTLnew of N

proof end;

definition

let w be Element of Inf_seq AtomicFamily;
let v be LTL-formula;
let U be Choice_Function of (BOOL (Subformulae v));
let N be strict LTLnode over v;

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 ;

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 over v
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds
( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )

proof end;

theorem :: MODELC_3:60

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

proof end;

theorem :: MODELC_3:61

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

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;

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 :

registration

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

existence

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 :

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 c₂ is strict ;
struct BuchiAutomaton over W -> 1-sorted ;
aggr BuchiAutomaton(# carrier, Tran, InitS, FinalS #) -> BuchiAutomaton over W;
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 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 :

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

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

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

::************
:: 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 (Subformulae v));
let N be strict LTLnode over v;
assume that
A1: not N is elementary and
A2: w |= * N ;

func chosen_succ_end_num (w,v,U,N) -> Nat means :Def48: :: MODELC_3:def 48
( ( for i being Nat st i < it holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** it) . N),v) is elementary & ( for i being Nat st i <= it holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) );

existence

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

proof end;

definition

let w be Element of Inf_seq AtomicFamily;
let v be neg-inner-most LTL-formula;
let U be Choice_Function of (BOOL (Subformulae v));

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 :

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