let w be Element of Inf_seq AtomicFamily ; :: thesis: for v being neg-inner-most LTL-formula st w |= v holds
w is-accepted-by BAutomaton v
let v be neg-inner-most LTL-formula; :: thesis: ( w |= v implies w is-accepted-by BAutomaton v )
set B = BAutomaton v;
set LS = LTLStates v;
set LT = Tran_LTL v;
set IS = InitS_LTL v;
set FS = FinalS_LTL v;
assume A1: w |= v ; :: thesis: w is-accepted-by BAutomaton v
ex run being sequence of (LTLStates v) st
( run . 0 in InitS_LTL v & ( for n being Nat holds
( [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] in Tran_LTL v & ( for FSet being set st FSet in FinalS_LTL v holds
{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) )
proof
consider chf being Choice_Function of BOOL (Subformulae v);
deffunc H1( set ) -> Element of LTLStates v = (chosen_run w,v,chf) . (k_nat $1);
A2: for x being set st x in NAT holds
H1(x) in LTLStates v ;
ex run being Function of NAT ,(LTLStates v) st
for x being set st x in NAT holds
run . x = H1(x) from FUNCT_2:sch 2(A2);
 then consider run being sequence of (LTLStates v) such that
A3: for x being set st x in NAT holds
run . x = H1(x) ;
deffunc H2( Nat) -> strict LTLnode of v = CastNode (run . $1),v;
A4: for n being Nat holds
( run . n is strict elementary LTLnode of v & H2(n) is strict elementary LTLnode of v )
proof
let n be Nat; :: thesis: ( run . n is strict elementary LTLnode of v & H2(n) is strict elementary LTLnode of v )
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set Rn = H2(n);
run . n in LTLStates v ;
then consider N being Element of LTLNodes v such that
A5: N = run . n and
A6: N is strict elementary LTLnode of v ;
reconsider N = N as strict elementary LTLnode of v by A6;
the LTLnew of H2(n) = the LTLnew of N by A5, Def16
.= {} by Def11 ;
hence ( run . n is strict elementary LTLnode of v & H2(n) is strict elementary LTLnode of v ) by A5, A6, Def11; :: thesis: verum
end;
A7: for n being Nat holds run . n = (chosen_run w,v,chf) . n
proof
let n be Nat; :: thesis: run . n = (chosen_run w,v,chf) . n
reconsider n = n as Element of NAT by ORDINAL1:def 13;
run . n = H1(n) by A3;
hence run . n = (chosen_run w,v,chf) . n by MODELC_1:def 2; :: thesis: verum
end;
A8: for n being Nat holds
( H2(n + 1) is_next_of H2(n) & Shift w,n |= * H2(n + 1) )
proof
let n be Nat; :: thesis: ( H2(n + 1) is_next_of H2(n) & Shift w,n |= * H2(n + 1) )
set Rn = H2(n);
reconsider Rn = H2(n) as strict elementary LTLnode of v by A4;
set n1 = n + 1;
set w1 = Shift w,n;
A9: run . n = (chosen_run w,v,chf) . n by A7;
H2(n) = CastNode ((chosen_run w,v,chf) . n),v by A7;
then A10: Shift w,n |= * ('X' Rn) by A1, Th73;
run . (n + 1) = (chosen_run w,v,chf) . (n + 1) by A7
.= chosen_next (Shift w,n),v,chf,Rn by A9, Def50 ;
then H2(n + 1) = chosen_next (Shift w,n),v,chf,Rn by Def16;
hence ( H2(n + 1) is_next_of H2(n) & Shift w,n |= * H2(n + 1) ) by A10, Th69; :: thesis: verum
end;
A11: for n being Nat holds (CastSeq w,AtomicFamily ) . n in Label_ H2(n + 1)
proof
let n be Nat; :: thesis: (CastSeq w,AtomicFamily ) . n in Label_ H2(n + 1)
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set Rn = H2(n);
set Rn1 = H2(n + 1);
set w1 = Shift w,n;
set X = (CastSeq w,AtomicFamily ) . n;
reconsider X = (CastSeq w,AtomicFamily ) . n as Subset of atomic_LTL ;
CastSeq (Shift w,n),AtomicFamily = Shift (CastSeq w,AtomicFamily ),n by MODELC_2:81;
then A12: (CastSeq (Shift w,n),AtomicFamily ) . 0 = (CastSeq w,AtomicFamily ) . (0 + n) by MODELC_2:def 45;
A13: Shift w,n |= * H2(n + 1) by A8;
A14: now
assume not Neg_atomic_LTL H2(n + 1) misses X ; :: thesis: contradiction
then (Neg_atomic_LTL H2(n + 1)) /\ X <> {} by XBOOLE_0:def 7;
then consider a being set such that
A15: a in (Neg_atomic_LTL H2(n + 1)) /\ X by XBOOLE_0:def 1;
a in Neg_atomic_LTL H2(n + 1) by A15, XBOOLE_0:def 4;
then consider x being LTL-formula such that
A16: ( x = a & x is atomic ) and
A17: 'not' x in the LTLold of H2(n + 1) ;
'not' x in * H2(n + 1) by A17, Lm1;
then Shift w,n |= 'not' x by A13, MODELC_2:def 68;
then A18: Shift w,n |/= x by MODELC_2:64;
a in X by A15, XBOOLE_0:def 4;
hence contradiction by A12, A16, A18, MODELC_2:63; :: thesis: verum
end;
atomic_LTL H2(n + 1) c= X
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in atomic_LTL H2(n + 1) or a in X )
assume a in atomic_LTL H2(n + 1) ; :: thesis: a in X
then consider x being LTL-formula such that
A19: ( x = a & x is atomic ) and
A20: x in the LTLold of H2(n + 1) ;
x in * H2(n + 1) by A20, Lm1;
then Shift w,n |= x by A13, MODELC_2:def 68;
hence a in X by A12, A19, MODELC_2:63; :: thesis: verum
end;
hence (CastSeq w,AtomicFamily ) . n in Label_ H2(n + 1) by A14; :: thesis: verum
end;
A21: for n being Nat holds [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] in Tran_LTL v
proof
let n be Nat; :: thesis: [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] in Tran_LTL v
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set R = H2(n);
reconsider R = H2(n) as strict elementary LTLnode of v by A4;
set n1 = n + 1;
set r = run . n;
set r1 = run . (n + 1);
set R1 = H2(n + 1);
set gA = (CastSeq w,AtomicFamily ) . n;
set y = [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))];
reconsider R1 = H2(n + 1) as strict elementary LTLnode of v by A4;
[(run . n),((CastSeq w,AtomicFamily ) . n)] in [:(LTLStates v),AtomicFamily :] by ZFMISC_1:106;
then [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] in [:[:(LTLStates v),AtomicFamily :],(LTLStates v):] by ZFMISC_1:106;
then A22: [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] by ZFMISC_1:def 3;
reconsider r1 = run . (n + 1) as strict elementary LTLnode of v by A4;
reconsider r = run . n as strict elementary LTLnode of v by A4;
A23: ( R1 is_next_of R & (CastSeq w,AtomicFamily ) . n in Label_ R1 ) by A8, A11;
( R = r & R1 = r1 ) by Def16;
hence [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] in Tran_LTL v by A22, A23; :: thesis: verum
end;
A24: for n being Nat
for H being LTL-formula st H in the LTLold of H2(n + 1) & H is Until & Shift w,n |= the_right_argument_of H holds
the_right_argument_of H in the LTLold of H2(n + 1)
proof
let n be Nat; :: thesis: for H being LTL-formula st H in the LTLold of H2(n + 1) & H is Until & Shift w,n |= the_right_argument_of H holds
the_right_argument_of H in the LTLold of H2(n + 1)
let H be LTL-formula; :: thesis: ( H in the LTLold of H2(n + 1) & H is Until & Shift w,n |= the_right_argument_of H implies the_right_argument_of H in the LTLold of H2(n + 1) )
set n1 = n + 1;
H2(n + 1) = CastNode ((chosen_run w,v,chf) . (n + 1)),v by A7;
hence ( H in the LTLold of H2(n + 1) & H is Until & Shift w,n |= the_right_argument_of H implies the_right_argument_of H in the LTLold of H2(n + 1) ) by A1, Th74; :: thesis: verum
end;
A25: for FSet being set st FSet in FinalS_LTL v holds
{ k where k is Element of NAT : run . k in FSet } is infinite set
proof
let FSet be set ; :: thesis: ( FSet in FinalS_LTL v implies { k where k is Element of NAT : run . k in FSet } is infinite set )
set FK = { k where k is Element of NAT : run . k in FSet } ;
assume FSet in FinalS_LTL v ; :: thesis: { k where k is Element of NAT : run . k in FSet } is infinite set
then consider x being Element of bool (LTLStates v) such that
A26: FSet = x and
A27: ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL F,v ) ;
consider F being LTL-formula such that
F is_subformula_of v and
A28: F is Until and
A29: x = FinalS_LTL F,v by A27;
set F2 = the_right_argument_of F;
set F1 = the_left_argument_of F;
A30: F = (the_left_argument_of F) 'U' (the_right_argument_of F) by A28, MODELC_2:8;
now
assume { k where k is Element of NAT : run . k in FSet } is not infinite set ; :: thesis: contradiction
then consider L being FinSequence such that
A31: { k where k is Element of NAT : run . k in FSet } = rng L by FINSEQ_1:73;
ex m being Nat st
for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet }
proof
A32: ( len L = 0 or 0 < 0 + (len L) ) ;
now
per cases ( 1 <= len L or len L = 0 ) by A32, NAT_1:19;
suppose A33: 1 <= len L ; :: thesis: ex m being Nat st
for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet }
set LEN = len L;
{ k where k is Element of NAT : run . k in FSet } c= REAL
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : run . k in FSet } or a in REAL )
assume a in { k where k is Element of NAT : run . k in FSet } ; :: thesis: a in REAL
then ex k being Element of NAT st
( a = k & run . k in FSet ) ;
hence a in REAL ; :: thesis: verum
end;
then reconsider L = L as FinSequence of REAL by A31, FINSEQ_1:def 4;
set realMAX = max L;
set iMAX = [/(max L)\];
set natMAX = [/(max L)\] + 1;
0 <= max L
proof
set b = L . (len L);
len L in Seg (len L) by A33, FINSEQ_1:3;
then len L in dom L by FINSEQ_1:def 3;
then L . (len L) in rng L by FUNCT_1:12;
then ex k being Element of NAT st
( k = L . (len L) & run . k in FSet ) by A31;
hence 0 <= max L by A33, RFINSEQ2:1; :: thesis: verum
end;
then reconsider iMAX = [/(max L)\] as Nat by INT_1:80;
iMAX + 1 is Nat ;
then reconsider natMAX = [/(max L)\] + 1 as Nat ;
for k being Nat st natMAX <= k holds
not k in { k where k is Element of NAT : run . k in FSet }
proof
let k be Nat; :: thesis: ( natMAX <= k implies not k in { k where k is Element of NAT : run . k in FSet } )
assume A34: natMAX <= k ; :: thesis: not k in { k where k is Element of NAT : run . k in FSet }
now
assume k in { k where k is Element of NAT : run . k in FSet } ; :: thesis: contradiction
then consider i1 being set such that
A35: i1 in dom L and
A36: k = L . i1 by A31, FUNCT_1:def 5;
reconsider i1 = i1 as Element of NAT by A35;
i1 in Seg (len L) by A35, FINSEQ_1:def 3;
then ( 1 <= i1 & i1 <= len L ) by FINSEQ_1:3;
then k <= max L by A36, RFINSEQ2:1;
hence contradiction by A34, INT_1:57, XXREAL_0:2; :: thesis: verum
end;
hence not k in { k where k is Element of NAT : run . k in FSet } ; :: thesis: verum
end;
hence ex m being Nat st
for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet } ; :: thesis: verum
end;
suppose len L = 0 ; :: thesis: ex m being Nat st
for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet }
then L = {} ;
then for k being Nat st 0 <= k holds
not k in { k where k is Element of NAT : run . k in FSet } by A31;
hence ex m being Nat st
for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet } ; :: thesis: verum
end;
end;
end;
hence ex m being Nat st
for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet } ; :: thesis: verum
end;
then consider m being Nat such that
A37: for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet } ;
A38: for k being Nat st m <= k holds
( F in the LTLold of H2(k) & not the_right_argument_of F in the LTLold of H2(k) )
proof
let k be Nat; :: thesis: ( m <= k implies ( F in the LTLold of H2(k) & not the_right_argument_of F in the LTLold of H2(k) ) )
assume m <= k ; :: thesis: ( F in the LTLold of H2(k) & not the_right_argument_of F in the LTLold of H2(k) )
then A39: not k in { k where k is Element of NAT : run . k in FSet } by A37;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
set r = run . k;
reconsider r = run . k as strict elementary LTLnode of v by A4;
now
assume ( not F in the LTLold of (CastNode r,v) or the_right_argument_of F in the LTLold of (CastNode r,v) ) ; :: thesis: contradiction
then r in FSet by A26, A29;
hence contradiction by A39; :: thesis: verum
end;
hence ( F in the LTLold of H2(k) & not the_right_argument_of F in the LTLold of H2(k) ) ; :: thesis: verum
end;
set w1 = Shift w,m;
set m1 = m + 1;
A40: Shift w,m |= * H2(m + 1) by A8;
m <= m + 1 by NAT_1:11;
then F in the LTLold of H2(m + 1) by A38;
then F in * H2(m + 1) by Lm1;
then Shift w,m |= F by A40, MODELC_2:def 68;
then consider h being Nat such that
for j being Nat st j < h holds
Shift (Shift w,m),j |= the_left_argument_of F and
A41: Shift (Shift w,m),h |= the_right_argument_of F by A30, MODELC_2:68;
set m2 = m + h;
set m3 = (m + h) + 1;
(m + h) + 1 = m + (h + 1) ;
then m <= (m + h) + 1 by NAT_1:11;
then A42: ( F in the LTLold of H2((m + h) + 1) & not the_right_argument_of F in the LTLold of H2((m + h) + 1) ) by A38;
Shift w,(m + h) |= the_right_argument_of F by A41, MODELC_2:80;
hence contradiction by A24, A28, A42; :: thesis: verum
end;
hence { k where k is Element of NAT : run . k in FSet } is infinite set ; :: thesis: verum
end;
run . 0 = (chosen_run w,v,chf) . 0 by A7
.= init v by Def50 ;
then run . 0 in InitS_LTL v by TARSKI:def 1;
hence ex run being sequence of (LTLStates v) st
( run . 0 in InitS_LTL v & ( for n being Nat holds
( [[(run . n),((CastSeq w,AtomicFamily ) . n)],(run . (n + 1))] in Tran_LTL v & ( for FSet being set st FSet in FinalS_LTL v holds
{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) ) by A21, A25; :: thesis: verum
end;
hence w is-accepted-by BAutomaton v by Def39; :: thesis: verum