:: Model Checking, Part {III}
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received August 19, 2008
:: Copyright (c) 2008 Association of Mizar Users
LemSUM01:
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 ) )
LemSUM02:
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 ) ) )
LemFinSeq01:
for H being LTL-formula holds
( <*H*> . 1 = H & rng <*H*> = {H} )
LemReal01:
for r1, r2 being real number st r1 <= r2 holds
[\r1/] <= [\r2/]
LemReal02:
for r1, r2 being real number st r1 <= r2 - 1 holds
[\r1/] <= [\r2/] - 1
Lem1006:
for n being Nat holds
( n = 0 or 1 <= n )
Lem101:
for H being LTL-formula st ( H is negative or H is next ) holds
the_argument_of H is_subformula_of H
Lem102:
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 )
Lem104:
for F, H being LTL-formula st F is_subformula_of H holds
{F} is Subset of (Subformulae H)
Lem106:
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)
Lem107:
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)
Lem108:
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) )
Lem109:
for H being LTL-formula holds {H} is Subset of (Subformulae H)
by Lem104, MODELC_2:27;
Lem110:
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 :
Def203:
:: 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
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 Lem107, Lem108, MODELC_2:78, SUBSET_1:4;
func LTLNew2 H -> Subset of
(Subformulae H) equals :
Def204:
:: 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
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 Lem107, Lem108, MODELC_2:78, SUBSET_1:4;
func LTLNext H -> Subset of
(Subformulae H) equals :
Def205:
:: 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
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 Lem109, Lem110, MODELC_2:78, SUBSET_1:4;
end;
:: deftheorem Def203 defines LTLNew1 MODELC_3:def 1 :
:: deftheorem Def204 defines LTLNew2 MODELC_3:def 2 :
:: deftheorem Def205 defines LTLNext MODELC_3:def 3 :
:: deftheorem Def206 defines SuccNode1 MODELC_3:def 4 :
:: deftheorem Def207 defines SuccNode2 MODELC_3:def 5 :
:: deftheorem DefSucc01 defines is_succ_of MODELC_3:def 6 :
:: deftheorem Def208 defines is_succ1_of MODELC_3:def 7 :
:: deftheorem Def209 defines is_succ2_of MODELC_3:def 8 :
:: deftheorem Def210 defines is_succ_of MODELC_3:def 9 :
:: deftheorem defines failure MODELC_3:def 10 :
:: deftheorem Defelementary 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 defCastNode01 defines CastNode MODELC_3:def 16 :
:: deftheorem defines init MODELC_3:def 17 :
:: deftheorem defines 'X' MODELC_3:def 18 :
:: deftheorem DefFinseq defines is_Finseq_for MODELC_3:def 19 :
lemFinseq01:
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 Def215 defines is_next_of MODELC_3:def 20 :
:: deftheorem defines CastLTL MODELC_3:def 21 :
:: deftheorem defines * MODELC_3:def 22 :
LemSUM04:
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)
LemSUM06:
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 :: MODELC_3:1
Lem203:
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) ) )
Lem204:
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) ) )
Lem205:
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 :: MODELC_3:2
LemSubformulae01:
for H being LTL-formula st ( H is negative or H is next ) holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
LemSubformulae02:
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}
LemSubformulae03:
for H being LTL-formula st H is atomic holds
Subformulae H = {H}
LemSubformulae04:
for H being LTL-formula
for W being Subset of (Subformulae H) holds not {} in W
theorem Th207: :: MODELC_3:3
:: deftheorem DefPartialfun defines Length_fun MODELC_3:def 23 :
:: deftheorem DefPartialseq defines Partial_seq MODELC_3:def 24 :
:: deftheorem defines len MODELC_3:def 25 :
lemlen02:
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
lemlen03:
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 Thlen00: :: MODELC_3:4
theorem Thlen01: :: MODELC_3:5
theorem Thlen02: :: MODELC_3:6
theorem Thlen03: :: MODELC_3:7
theorem Thlen04: :: MODELC_3:8
:: deftheorem Deflen02 defines len MODELC_3:def 26 :
theorem :: MODELC_3:9
theorem Thlen07: :: MODELC_3:10
theorem Thlen08: :: MODELC_3:11
theorem Thlen09: :: MODELC_3:12
theorem Thlen10: :: MODELC_3:13
theorem Thlen11: :: MODELC_3:14
lemlen05:
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 Thlen12: :: MODELC_3:15
theorem Thlen1201: :: MODELC_3:16
theorem Thlen1203: :: MODELC_3:17
theorem Thlen13: :: MODELC_3:18
:: deftheorem defLTLNew101 defines LTLNew1 MODELC_3:def 27 :
:: deftheorem defLTLNew201 defines LTLNew2 MODELC_3:def 28 :
lemlen05:
for H, v being LTL-formula st H in Subformulae v holds
len (LTLNew1 H,v) <= (len H) - 1
lemlen06:
for H, v being LTL-formula st H in Subformulae v holds
len (LTLNew2 H,v) <= (len H) - 1
theorem Thlen15: :: MODELC_3:19
theorem Thlen16: :: MODELC_3:20
:: deftheorem defines len MODELC_3:def 29 :
theorem Thlen17: :: MODELC_3:21
theorem Thlen18: :: MODELC_3:22
theorem Thlen19: :: MODELC_3:23
theorem :: MODELC_3:24
theorem ThSucc01: :: MODELC_3:25
theorem ThSucc02: :: MODELC_3:26
theorem ThSucc03: :: MODELC_3:27
theorem ThSucc04: :: MODELC_3:28
theorem ThSucc05: :: MODELC_3:29
theorem ThSucc06: :: MODELC_3:30
theorem ThSucc07: :: MODELC_3:31
theorem ThSucc08: :: MODELC_3:32
theorem ThSucc09: :: MODELC_3:33
theorem ThSucc10: :: MODELC_3:34
theorem ThSucc11: :: MODELC_3:35
theorem ThSucc12: :: MODELC_3:36
theorem ThNext01: :: MODELC_3:37
theorem ThNext02: :: MODELC_3:38
theorem THrelease01: :: MODELC_3:39
theorem THrelease02: :: MODELC_3:40
theorem Thnext03: :: MODELC_3:41
lemUntil01:
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 :: MODELC_3:42
:: deftheorem defLTLNodes defines LTLNodes MODELC_3:def 30 :
:: deftheorem defines LTLStates MODELC_3:def 31 :
theorem :: MODELC_3:43
theorem ThLTLStates02: :: MODELC_3:44
theorem ThLTLStates03: :: MODELC_3:45
lemExistMin:
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 :
defSuccHom:
:: 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 :
defHom:
:: 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 defSuccHom defines is_succ_homomorphism MODELC_3:def 32 :
:: deftheorem defHom defines is_homomorphism MODELC_3:def 33 :
theorem ThLTLNodes01: :: MODELC_3:46
theorem ThLTLNodes02: :: MODELC_3:47
theorem ThLTLNodes03: :: MODELC_3:48
theorem ThLTLNodes04: :: MODELC_3:49
theorem ThLTLNodes05: :: MODELC_3:50
theorem ThLTLNodes06: :: MODELC_3:51
theorem ThLTLStates04: :: MODELC_3:52
lemUntil02:
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 :: MODELC_3:53
lemUntil03:
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 THuntil03: :: 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) ) ) )
theorem ThBOOL01: :: MODELC_3:55
theorem ThBOOL02: :: MODELC_3:56
theorem :: MODELC_3:57
:: deftheorem Defchosenformula defines chosen_formula MODELC_3:def 34 :
theorem Thchoice: :: MODELC_3:58
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 :
Defchosensucc:
:: MODELC_3:def 35
SuccNode1 (chosen_formula U,N),
N if ( ( not
chosen_formula U,
N is
Until &
w |= * (SuccNode1 (chosen_formula U,N),N) ) or (
chosen_formula U,
N is
Until &
w |/= the_right_argument_of (chosen_formula U,N) ) )
otherwise SuccNode2 (chosen_formula U,N),
N;
correctness
coherence
( ( ( ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) or ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ) implies SuccNode1 (chosen_formula U,N),N is strict LTLnode 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 Defchosensucc 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 Thchosensucc01: :: MODELC_3:59
theorem :: MODELC_3:60
for
v being
LTL-formula for
N being
strict LTLnode of
v for
w being
Element of
Inf_seq AtomicFamily for
U being
Choice_Function of
BOOL (Subformulae v) st
w |= * N & 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 :: MODELC_3:61
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 :
Defchoicesuccfunc:
:: MODELC_3:def 36
for
x being
set st
x in LTLNodes v holds
it . x = chosen_succ w,
v,
U,
(CastNode x,v);
existence
ex b1 being Function of (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 Defchoicesuccfunc defines choice_succ_func MODELC_3:def 36 :
theorem Thchoicesuccfunc01: :: MODELC_3:62
:: deftheorem DefNegIM defines neg-inner-most MODELC_3:def 37 :
:: deftheorem DefSubatomic defines Sub_atomic MODELC_3:def 38 :
theorem ThNegIM01: :: MODELC_3:63
theorem ThNegIM02: :: MODELC_3:64
theorem ThNegIM03: :: MODELC_3:65
theorem :: MODELC_3:66
theorem :: MODELC_3:67
:: deftheorem DefBam01 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
[:(LTLStates v),AtomicFamily :],
(LTLStates v) equals :: MODELC_3:def 43
{ y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;
correctness
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 :: MODELC_3:def 44
{(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 thBA01: :: MODELC_3:68
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:
( not
N is
elementary &
w |= * N )
;
func chosen_succ_end_num w,
v,
U,
N -> Nat means :
DefUsuccEndnum:
:: MODELC_3:def 48
( ( for
i being
Nat st
i < it holds
( not
CastNode (((choice_succ_func w,v,U) |** i) . N),
v is
elementary &
CastNode (((choice_succ_func w,v,U) |** (i + 1)) . N),
v is_succ_of CastNode (((choice_succ_func w,v,U) |** i) . N),
v ) ) &
CastNode (((choice_succ_func w,v,U) |** it) . N),
v is
elementary & ( for
i being
Nat st
i <= it holds
w |= * (CastNode (((choice_succ_func w,v,U) |** i) . N),v) ) );
existence
ex b1 being Nat st
( ( for i being Nat st i < b1 holds
( not CastNode (((choice_succ_func w,v,U) |** i) . N),v is elementary & CastNode (((choice_succ_func w,v,U) |** (i + 1)) . N),v is_succ_of CastNode (((choice_succ_func w,v,U) |** i) . N),v ) ) & CastNode (((choice_succ_func w,v,U) |** b1) . N),v is elementary & ( for i being Nat st i <= b1 holds
w |= * (CastNode (((choice_succ_func w,v,U) |** i) . N),v) ) )
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 DefUsuccEndnum 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 :
Defchosennext:
:: MODELC_3:def 49
CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' N))) . ('X' N)),
v if not
'X' N is
elementary otherwise FinalNode v;
correctness
coherence
( ( not 'X' N is elementary implies CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' N))) . ('X' N)),v is strict elementary LTLnode 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 Defchosennext 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 thChoicedNext01: :: MODELC_3:69
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 :
Defchosenrun:
:: MODELC_3:def 50
(
it . 0 = init v & ( for
n being
Nat holds
it . (n + 1) = chosen_next (Shift w,n),
v,
U,
(CastNode (it . n),v) ) );
existence
ex b1 being sequence of (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 Defchosenrun defines chosen_run MODELC_3:def 50 :
LemBA01:
for v being neg-inner-most LTL-formula holds 'X' (CastLTL ({} v)) = {}
theorem thBA02: :: MODELC_3:70
theorem :: MODELC_3:71
theorem thBA04: :: MODELC_3:72
theorem thBA05: :: 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)) )
theorem thBA06: :: MODELC_3:74
theorem thBA07: :: MODELC_3:75
theorem :: MODELC_3:76