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 ) )
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 ) ) )
Lm3:
for H being LTL-formula holds
( <*H*> . 1 = H & rng <*H*> = {H} )
Lm4:
for r1, r2 being real number st r1 <= r2 holds
[\r1/] <= [\r2/]
Lm5:
for r1, r2 being real number st r1 <= r2 - 1 holds
[\r1/] <= [\r2/] - 1
Lm6:
for n being Nat holds
( n = 0 or 1 <= n )
Lm7:
for H being LTL-formula st ( H is negative or H is next ) holds
the_argument_of H is_subformula_of H
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 )
Lm9:
for F, H being LTL-formula st F is_subformula_of H holds
{F} is Subset of
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
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
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 & {(the_right_argument_of H)} is Subset of )
Lm13:
for H being LTL-formula holds {H} is Subset of
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
definition
let H be
LTL-formula;
func LTLNew1 H -> Subset of
equals :
Def1:
{(the_left_argument_of H),(the_right_argument_of H)} if H is
conjunctive {(the_left_argument_of H)} if H is
disjunctive {} if H is
next {(the_left_argument_of H)} if H is
Until {(the_right_argument_of H)} if H is
Release otherwise {} ;
correctness
coherence
( ( H is conjunctive implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of ) & ( H is disjunctive implies {(the_left_argument_of H)} is Subset of ) & ( H is next implies {} is Subset of ) & ( H is Until implies {(the_left_argument_of H)} is Subset of ) & ( H is Release implies {(the_right_argument_of 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 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {(the_left_argument_of H)} ) ) & ( H is conjunctive & H is next implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {} ) ) & ( H is conjunctive & H is Until implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {(the_left_argument_of H)} ) ) & ( H is conjunctive & H is Release implies ( b1 = {(the_left_argument_of H),(the_right_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) & ( H is disjunctive & H is next implies ( b1 = {(the_left_argument_of H)} iff b1 = {} ) ) & ( H is disjunctive & H is Until implies ( b1 = {(the_left_argument_of H)} iff b1 = {(the_left_argument_of H)} ) ) & ( H is disjunctive & H is Release implies ( b1 = {(the_left_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) & ( H is next & H is Until implies ( b1 = {} iff b1 = {(the_left_argument_of H)} ) ) & ( H is next & H is Release implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) & ( H is Until & H is Release implies ( b1 = {(the_left_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) );
by Lm11, Lm12, MODELC_2:78, SUBSET_1:4;
func LTLNew2 H -> Subset of
equals :
Def2:
{} if H is
conjunctive {(the_right_argument_of H)} if H is
disjunctive {} if H is
next {(the_right_argument_of H)} if H is
Until {(the_left_argument_of H),(the_right_argument_of H)} if H is
Release otherwise {} ;
correctness
coherence
( ( H is conjunctive implies {} is Subset of ) & ( H is disjunctive implies {(the_right_argument_of H)} is Subset of ) & ( H is next implies {} is Subset of ) & ( H is Until implies {(the_right_argument_of H)} is Subset of ) & ( H is Release implies {(the_left_argument_of H),(the_right_argument_of 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 = {(the_right_argument_of H)} ) ) & ( H is conjunctive & H is next implies ( b1 = {} iff b1 = {} ) ) & ( H is conjunctive & H is Until implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) & ( H is conjunctive & H is Release implies ( b1 = {} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) & ( H is disjunctive & H is next implies ( b1 = {(the_right_argument_of H)} iff b1 = {} ) ) & ( H is disjunctive & H is Until implies ( b1 = {(the_right_argument_of H)} iff b1 = {(the_right_argument_of H)} ) ) & ( H is disjunctive & H is Release implies ( b1 = {(the_right_argument_of H)} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) & ( H is next & H is Until implies ( b1 = {} iff b1 = {(the_right_argument_of H)} ) ) & ( H is next & H is Release implies ( b1 = {} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) & ( H is Until & H is Release implies ( b1 = {(the_right_argument_of H)} iff b1 = {(the_left_argument_of H),(the_right_argument_of H)} ) ) );
by Lm11, Lm12, MODELC_2:78, SUBSET_1:4;
func LTLNext H -> Subset of
equals :
Def3:
{} if H is
conjunctive {} if H is
disjunctive {(the_argument_of H)} if H is
next {H} if H is
Until {H} if H is
Release otherwise {} ;
correctness
coherence
( ( H is conjunctive implies {} is Subset of ) & ( H is disjunctive implies {} is Subset of ) & ( H is next implies {(the_argument_of H)} 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 = {(the_argument_of H)} ) ) & ( 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 = {(the_argument_of H)} ) ) & ( 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 = {(the_argument_of H)} iff b1 = {H} ) ) & ( H is next & H is Release implies ( b1 = {(the_argument_of H)} iff b1 = {H} ) ) & ( H is Until & H is Release implies ( b1 = {H} iff b1 = {H} ) ) );
by Lm13, Lm14, MODELC_2:78, SUBSET_1:4;
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 :
:: deftheorem Def4 defines SuccNode1 MODELC_3:def 4 :
:: deftheorem Def5 defines SuccNode2 MODELC_3:def 5 :
:: deftheorem Def6 defines is_succ_of MODELC_3:def 6 :
:: deftheorem Def7 defines is_succ1_of MODELC_3:def 7 :
:: deftheorem Def8 defines is_succ2_of MODELC_3:def 8 :
:: deftheorem Def9 defines is_succ_of MODELC_3:def 9 :
:: deftheorem defines failure MODELC_3:def 10 :
:: deftheorem Def11 defines elementary MODELC_3:def 11 :
:: deftheorem defines final MODELC_3:def 12 :
:: deftheorem defines {} MODELC_3:def 13 :
:: deftheorem defines Seed MODELC_3:def 14 :
:: deftheorem defines FinalNode MODELC_3:def 15 :
:: deftheorem Def16 defines CastNode MODELC_3:def 16 :
:: deftheorem defines init MODELC_3:def 17 :
:: deftheorem defines 'X' MODELC_3:def 18 :
:: 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) )
:: deftheorem Def20 defines is_next_of MODELC_3:def 20 :
:: deftheorem defines CastLTL MODELC_3:def 21 :
:: 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)
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) )
theorem
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) ) )
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) ) )
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) ) )
theorem
Lm21:
for H being LTL-formula st ( H is negative or H is next ) holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
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}
Lm23:
for H being LTL-formula st H is atomic holds
Subformulae H = {H}
Lm24:
for H being LTL-formula
for W being Subset of holds not {} in W
theorem Th3:
:: deftheorem Def23 defines Length_fun MODELC_3:def 23 :
:: deftheorem Def24 defines Partial_seq MODELC_3:def 24 :
:: 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
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)
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem Def26 defines len MODELC_3:def 26 :
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
Lm27:
for H being LTL-formula
for W, W1 being Subset of holds
( not W c= W1 or W = W1 or ex x being set st
( x in W1 & W c= W1 \ {x} ) )
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
:: 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
Lm29:
for H, v being LTL-formula st H in Subformulae v holds
len (LTLNew2 H,v) <= (len H) - 1
theorem Th19:
theorem Th20:
:: deftheorem defines len MODELC_3:def 29 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
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 )
theorem
:: deftheorem Def30 defines LTLNodes MODELC_3:def 30 :
:: deftheorem defines LTLStates MODELC_3:def 31 :
theorem
theorem Th44:
theorem Th45:
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 ) )
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:
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:
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:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
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) )
theorem
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) ) ) )
theorem Th54:
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) ) ) )
theorem Th55:
theorem Th56:
theorem
:: deftheorem Def34 defines chosen_formula MODELC_3:def 34 :
theorem Th58:
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:
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 of 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 of v ) );
consistency
for b1 being strict LTLnode of v holds verum;
;
end;
:: deftheorem Def35 defines chosen_succ MODELC_3:def 35 :
for
w being
Element of
Inf_seq AtomicFamily for
v being
LTL-formula for
U being
Choice_Function of
BOOL (Subformulae v) for
N being
strict LTLnode of
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:
theorem
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) )
theorem
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:
for
x being
set st
x in LTLNodes v holds
it . x = chosen_succ w,
v,
U,
(CastNode x,v);
existence
ex b1 being Function of LTLNodes v, LTLNodes v st
for x being set st x in LTLNodes v holds
b1 . x = chosen_succ w,v,U,(CastNode x,v)
uniqueness
for b1, b2 being Function of LTLNodes v, LTLNodes v st ( for x being set st x in LTLNodes v holds
b1 . x = chosen_succ w,v,U,(CastNode x,v) ) & ( for x being set st x in LTLNodes v holds
b2 . x = chosen_succ w,v,U,(CastNode x,v) ) holds
b1 = b2
end;
:: deftheorem Def36 defines choice_succ_func MODELC_3:def 36 :
theorem Th62:
begin
:: deftheorem Def37 defines neg-inner-most MODELC_3:def 37 :
:: deftheorem Def38 defines Sub_atomic MODELC_3:def 38 :
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
begin
:: deftheorem Def39 defines is-accepted-by MODELC_3:def 39 :
:: deftheorem defines atomic_LTL MODELC_3:def 40 :
:: deftheorem defines Neg_atomic_LTL MODELC_3:def 41 :
:: deftheorem defines Label_ MODELC_3:def 42 :
definition
let v be
neg-inner-most LTL-formula;
func Tran_LTL v -> Relation of ,
equals
{ 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
coherence
{ 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 ) } is Relation of ,;
func InitS_LTL v -> Element of
bool (LTLStates v) equals
{(init v)};
correctness
coherence
{(init v)} is Element of bool (LTLStates v);
end;
:: deftheorem defines Tran_LTL MODELC_3:def 43 :
:: deftheorem defines InitS_LTL MODELC_3:def 44 :
:: deftheorem defines FinalS_LTL MODELC_3:def 45 :
:: deftheorem defines FinalS_LTL MODELC_3:def 46 :
:: deftheorem defines BAutomaton MODELC_3:def 47 :
theorem Th68:
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:
( ( 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) ) )
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
end;
:: deftheorem Def48 defines chosen_succ_end_num MODELC_3:def 48 :
for
w being
Element of
Inf_seq AtomicFamily for
v being
neg-inner-most LTL-formula for
U being
Choice_Function of
BOOL (Subformulae v) for
N being
strict LTLnode of
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 (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:
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 of v ) & ( 'X' N is elementary implies FinalNode v is strict elementary LTLnode of v ) );
consistency
for b1 being strict elementary LTLnode of v holds verum;
end;
:: deftheorem Def49 defines chosen_next MODELC_3:def 49 :
for
w being
Element of
Inf_seq AtomicFamily for
v being
neg-inner-most LTL-formula for
U being
Choice_Function of
BOOL (Subformulae v) for
N being
strict LTLnode of
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:
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:
(
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 LTLStates v st
( b1 . 0 = init v & ( for n being Nat holds b1 . (n + 1) = chosen_next (Shift w,n),v,U,(CastNode (b1 . n),v) ) )
uniqueness
for b1, b2 being sequence of LTLStates v 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
end;
:: deftheorem Def50 defines chosen_run MODELC_3:def 50 :
Lm34:
for v being neg-inner-most LTL-formula holds 'X' (CastLTL ({} v)) = {}
theorem Th70:
theorem
theorem Th72:
theorem Th73:
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)) )
theorem Th74:
theorem Th75:
theorem