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 (Subformulae H)
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)
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)
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) )
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)
definition
let H be
LTL-formula;
func LTLNew1 H -> Subset of
(Subformulae H) 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 (Subformulae H) ) & ( H is disjunctive implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) & ( H is next implies {} is Subset of (Subformulae H) ) & ( H is Until implies {(the_left_argument_of H)} is Subset of (Subformulae H) ) & ( H is Release implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );
consistency
for b1 being Subset of (Subformulae H) 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
(Subformulae H) 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 (Subformulae H) ) & ( H is disjunctive implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is next implies {} is Subset of (Subformulae H) ) & ( H is Until implies {(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( H is Release implies {(the_left_argument_of H),(the_right_argument_of H)} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );
consistency
for b1 being Subset of (Subformulae H) 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
(Subformulae H) 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 (Subformulae H) ) & ( H is disjunctive implies {} is Subset of (Subformulae H) ) & ( H is next implies {(the_argument_of H)} is Subset of (Subformulae H) ) & ( H is Until implies {H} is Subset of (Subformulae H) ) & ( H is Release implies {H} is Subset of (Subformulae H) ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies {} is Subset of (Subformulae H) ) );
consistency
for b1 being Subset of (Subformulae H) 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 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNew1 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( H is disjunctive implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is next implies LTLNew1 H = {} ) & ( H is Until implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is Release implies LTLNew1 H = {(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew1 H = {} ) );
:: deftheorem Def2 defines LTLNew2 MODELC_3:def 2 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNew2 H = {} ) & ( H is disjunctive implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is next implies LTLNew2 H = {} ) & ( H is Until implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is Release implies LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew2 H = {} ) );
:: deftheorem Def3 defines LTLNext MODELC_3:def 3 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNext H = {} ) & ( H is disjunctive implies LTLNext H = {} ) & ( H is next implies LTLNext H = {(the_argument_of H)} ) & ( H is Until implies LTLNext H = {H} ) & ( H is Release implies LTLNext H = {H} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNext H = {} ) );
:: deftheorem Def4 defines SuccNode1 MODELC_3:def 4 :
for v being LTL-formula
for N being LTLnode of v
for H being LTL-formula st H in the LTLnew of N holds
for b4 being strict LTLnode of v holds
( b4 = SuccNode1 (H,N) iff ( the LTLold of b4 = the LTLold of N \/ {H} & the LTLnew of b4 = ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of b4 = the LTLnext of N \/ (LTLNext H) ) );
:: deftheorem Def5 defines SuccNode2 MODELC_3:def 5 :
for v being LTL-formula
for N being LTLnode of v
for H being LTL-formula st H in the LTLnew of N holds
for b4 being strict LTLnode of v holds
( b4 = SuccNode2 (H,N) iff ( the LTLold of b4 = the LTLold of N \/ {H} & the LTLnew of b4 = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of b4 = the LTLnext of N ) );
:: deftheorem Def6 defines is_succ_of MODELC_3:def 6 :
for v being LTL-formula
for N1, N2 being LTLnode of v
for H being LTL-formula holds
( N2 is_succ_of N1,H iff ( H in the LTLnew of N1 & ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) ) ) );
:: deftheorem Def7 defines is_succ1_of MODELC_3:def 7 :
for v being LTL-formula
for N1, N2 being LTLnode of v holds
( N2 is_succ1_of N1 iff ex H being LTL-formula st
( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) ) );
:: deftheorem Def8 defines is_succ2_of MODELC_3:def 8 :
for v being LTL-formula
for N1, N2 being LTLnode of v holds
( N2 is_succ2_of N1 iff ex H being LTL-formula st
( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) );
:: deftheorem Def9 defines is_succ_of MODELC_3:def 9 :
for v being LTL-formula
for N1, N2 being LTLnode of v holds
( N2 is_succ_of N1 iff ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) );
:: deftheorem defines failure MODELC_3:def 10 :
for v being LTL-formula
for N being LTLnode of v holds
( N is failure iff ex H, F being LTL-formula st
( H is atomic & F = 'not' H & H in the LTLold of N & F in the LTLold of N ) );
:: deftheorem Def11 defines elementary MODELC_3:def 11 :
for v being LTL-formula
for N being LTLnode of v holds
( N is elementary iff the LTLnew of N = {} );
:: deftheorem defines final MODELC_3:def 12 :
for v being LTL-formula
for N being LTLnode of v holds
( N is final iff ( N is elementary & the LTLnext of N = {} ) );
:: deftheorem defines {} MODELC_3:def 13 :
for v being LTL-formula holds {} v = {} ;
:: deftheorem defines Seed MODELC_3:def 14 :
for v being LTL-formula holds Seed v = {v};
:: deftheorem defines FinalNode MODELC_3:def 15 :
for v being LTL-formula holds FinalNode v = LTLnode(# ({} v),({} v),({} v) #);
:: deftheorem Def16 defines CastNode MODELC_3:def 16 :
for x being set
for v being LTL-formula holds
( ( x is strict LTLnode of v implies CastNode (x,v) = x ) & ( x is not strict LTLnode of v implies CastNode (x,v) = LTLnode(# ({} v),({} v),({} v) #) ) );
:: deftheorem defines init MODELC_3:def 17 :
for v being LTL-formula holds init v = LTLnode(# ({} v),({} v),(Seed v) #);
:: deftheorem defines 'X' MODELC_3:def 18 :
for v being LTL-formula
for N being LTLnode of v holds 'X' N = LTLnode(# ({} v), the LTLnext of N,({} v) #);
:: deftheorem Def19 defines is_Finseq_for MODELC_3:def 19 :
for v being LTL-formula
for L being FinSequence holds
( L is_Finseq_for v iff for k being Nat st 1 <= k & 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 ) );
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 :
for v being LTL-formula
for N1, N2 being strict LTLnode of v holds
( N2 is_next_of N1 iff ( N1 is elementary & N2 is elementary & ex L being FinSequence st
( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' N1 & L . (len L) = N2 ) ) );
:: deftheorem defines CastLTL MODELC_3:def 21 :
for v being LTL-formula
for W being Subset of (Subformulae v) holds CastLTL W = W;
:: deftheorem defines * MODELC_3:def 22 :
for v being LTL-formula
for N being strict LTLnode of v holds * N = ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N));
Lm16:
for H, v being LTL-formula
for N being strict LTLnode 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 (Subformulae H) holds not {} in W
theorem Th3:
:: deftheorem Def23 defines Length_fun MODELC_3:def 23 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for L being FinSequence
for x being set holds
( ( L . x in W implies Length_fun (L,W,x) = len (CastLTL (L . x)) ) & ( not L . x in W implies Length_fun (L,W,x) = 0 ) );
:: deftheorem Def24 defines Partial_seq MODELC_3:def 24 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for L being FinSequence
for b4 being Real_Sequence holds
( b4 = Partial_seq (L,W) iff for k being Nat holds
( ( L . k in W implies b4 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b4 . k = 0 ) ) );
:: deftheorem defines len MODELC_3:def 25 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for L being FinSequence holds len (L,W) = Sum ((Partial_seq (L,W)),(len L));
Lm25:
for n being Nat
for R1, R2 being Real_Sequence st ( for i being Nat st i <= n holds
R1 . i = R2 . i ) holds
Sum (R1,n) = Sum (R2,n)
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 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for b3 being Real holds
( b3 = len W iff ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & b3 = len (L,W) ) );
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
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} ) )
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
:: deftheorem Def27 defines LTLNew1 MODELC_3:def 27 :
for v, H being LTL-formula st H in Subformulae v holds
LTLNew1 (H,v) = LTLNew1 H;
:: deftheorem Def28 defines LTLNew2 MODELC_3:def 28 :
for v, H being LTL-formula st H in Subformulae v holds
LTLNew2 (H,v) = LTLNew2 H;
Lm28:
for H, v being LTL-formula st H in Subformulae v holds
len (LTLNew1 (H,v)) <= (len H) - 1
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 :
for v being LTL-formula
for N being strict LTLnode of v holds len N = [\(len the LTLnew of N)/];
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 :
for v being LTL-formula
for b2 being non empty set holds
( b2 = LTLNodes v iff for x being set holds
( x in b2 iff ex N being strict LTLnode of v st x = N ) );
:: deftheorem defines LTLStates MODELC_3:def 31 :
for v being LTL-formula holds LTLStates v = { x where x is Element of LTLNodes v : x is strict elementary LTLnode of v } ;
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 :
for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function holds
( f is_succ_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
( CastNode ((f . x),v) is_succ_of CastNode (x,v) & w |= * (CastNode ((f . x),v)) ) );
:: deftheorem Def33 defines is_homomorphism MODELC_3:def 33 :
for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function holds
( f is_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
w |= * (CastNode ((f . x),v)) );
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 :
for v being LTL-formula
for U being Choice_Function of BOOL (Subformulae v)
for N being strict LTLnode of v st not N is elementary holds
chosen_formula (U,N) = U . the LTLnew of N;
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 :
for w being Element of Inf_seq AtomicFamily
for v being LTL-formula
for U being Choice_Function of BOOL (Subformulae v)
for b4 being Function of (LTLNodes v),(LTLNodes v) holds
( b4 = choice_succ_func (w,v,U) iff for x being set st x in LTLNodes v holds
b4 . x = chosen_succ (w,v,U,(CastNode (x,v))) );
theorem Th62:
begin
:: deftheorem Def37 defines neg-inner-most MODELC_3:def 37 :
for H being LTL-formula holds
( H is neg-inner-most iff for G being LTL-formula st G is_subformula_of H & G is negative holds
the_argument_of G is atomic );
:: deftheorem Def38 defines Sub_atomic MODELC_3:def 38 :
for H being LTL-formula holds
( H is Sub_atomic iff ( H is atomic or ex G being LTL-formula st
( G is atomic & H = 'not' G ) ) );
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
begin
:: deftheorem Def39 defines is-accepted-by MODELC_3:def 39 :
for W being non empty set
for B being BuchiAutomaton of W
for w being Element of Inf_seq W holds
( w is-accepted-by B iff ex run being sequence of the carrier of B st
( run . 0 in the InitS of B & ( for i being Nat holds
( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B & ( for FSet being set st FSet in the FinalS of B holds
{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) ) );
:: deftheorem defines atomic_LTL MODELC_3:def 40 :
for v being neg-inner-most LTL-formula
for N being strict LTLnode of v holds atomic_LTL N = { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;
:: deftheorem defines Neg_atomic_LTL MODELC_3:def 41 :
for v being neg-inner-most LTL-formula
for N being strict LTLnode of v holds Neg_atomic_LTL N = { x where x is LTL-formula : ( x is atomic & 'not' x in the LTLold of N ) } ;
:: deftheorem defines Label_ MODELC_3:def 42 :
for v being neg-inner-most LTL-formula
for N being strict LTLnode of v holds Label_ N = { x where x is Subset of atomic_LTL : ( atomic_LTL N c= x & Neg_atomic_LTL N misses x ) } ;
definition
let v be
neg-inner-most LTL-formula;
func Tran_LTL v -> Relation of
[:(LTLStates v),AtomicFamily:],
(LTLStates v) 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 [:(LTLStates v),AtomicFamily:],(LTLStates v);
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 :
for v being neg-inner-most LTL-formula holds Tran_LTL v = { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;
:: deftheorem defines InitS_LTL MODELC_3:def 44 :
for v being neg-inner-most LTL-formula holds InitS_LTL v = {(init v)};
:: deftheorem defines FinalS_LTL MODELC_3:def 45 :
for v being neg-inner-most LTL-formula
for F being LTL-formula holds FinalS_LTL (F,v) = { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } ;
:: deftheorem defines FinalS_LTL MODELC_3:def 46 :
for v being neg-inner-most LTL-formula holds FinalS_LTL v = { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;
:: deftheorem defines BAutomaton MODELC_3:def 47 :
for v being neg-inner-most LTL-formula holds BAutomaton v = BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);
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;
by A1, Def48;
end;
:: deftheorem Def49 defines chosen_next MODELC_3:def 49 :
for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for U being Choice_Function of BOOL (Subformulae v)
for N being strict LTLnode 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 :
for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for U being Choice_Function of BOOL (Subformulae v)
for b4 being sequence of (LTLStates v) holds
( b4 = chosen_run (w,v,U) iff ( b4 . 0 = init v & ( for n being Nat holds b4 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b4 . n),v))) ) ) );
Lm34:
for v being neg-inner-most LTL-formula holds 'X' (CastLTL ({} v)) = {}
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