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 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
set chf = the Choice_Function of (BOOL (Subformulae v));
deffunc H1( set ) -> Element of LTLStates v = (chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . (k_nat $1);
A2: for x being set st x in NAT holds
H1(x) in LTLStates v ;
ex run being sequence of (LTLStates v) st
for x being set st x in NAT holds
run . x = H1(x) from FUNCT_2:sch 11(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 over v = CastNode ((run . $1),v);
A4: for n being Nat holds
( run . n is strict elementary LTLnode over v & H2(n) is strict elementary LTLnode over v )
proof
let n be Nat; :: thesis: ( run . n is strict elementary LTLnode over v & H2(n) is strict elementary LTLnode over v )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
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 over v ;
reconsider N = N as strict elementary LTLnode over v by A6;
the LTLnew of H2(n) = the LTLnew of N by A5, Def16
.= {} by Def11 ;
hence ( run . n is strict elementary LTLnode over v & H2(n) is strict elementary LTLnode over v ) by A5, A6, Def11; :: thesis: verum
end;
A7: for n being Nat holds run . n = (chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . n
proof
let n be Nat; :: thesis: run . n = (chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . n
reconsider n = n as Element of NAT by ORDINAL1:def 12;
run . n = H1(n) by A3;
hence run . n = (chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . 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 over v by A4;
set n1 = n + 1;
set w1 = Shift (w,n);
A9: run . n = (chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . n by A7;
H2(n) = CastNode (((chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . n),v) by A7;
then A10: Shift (w,n) |= * ('X' Rn) by A1, Th73;
run . (n + 1) = (chosen_run (w,v, the Choice_Function of (BOOL (Subformulae v)))) . (n + 1) by A7
.= chosen_next ((Shift (w,n)),v, the Choice_Function of (BOOL (Subformulae v)),Rn) by A9, Def50 ;
then H2(n + 1) = chosen_next ((Shift (w,n)),v, the Choice_Function of (BOOL (Subformulae v)),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 12;
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) = (CastSeq (w,AtomicFamily)) ^\ n by MODELC_2:81;
then A12: (CastSeq ((Shift (w,n)),AtomicFamily)) . 0 = (CastSeq (w,AtomicFamily)) . (0 + n) by NAT_1:def 3;
A13: Shift (w,n) |= * H2(n + 1) by A8;
A14: now :: thesis: Neg_atomic_LTL H2(n + 1) misses X
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 object 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;
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 object ; :: 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;
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 12;
set R = H2(n);
reconsider R = H2(n) as strict elementary LTLnode over 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 over v by A4;
[(run . n),((CastSeq (w,AtomicFamily)) . n)] in [:(LTLStates v),AtomicFamily:] by ZFMISC_1:87;
then [[(run . n),((CastSeq (w,AtomicFamily)) . n)],(run . (n + 1))] in [:[:(LTLStates v),AtomicFamily:],(LTLStates v):] by ZFMISC_1:87;
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 over v by A4;
reconsider r = run . n as strict elementary LTLnode over 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, the Choice_Function of (BOOL (Subformulae v)))) . (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 :: thesis: { k where k is Element of NAT : run . k in FSet } is infinite set
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:52;
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 :: 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 }
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 object ; :: 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 consider k being Element of NAT such that
A34: ( a = k & run . k in FSet ) ;
k in REAL by XREAL_0:def 1;
hence a in REAL by A34; :: 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:1;
then len L in dom L by FINSEQ_1:def 3;
then L . (len L) in rng L by FUNCT_1:3;
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:53;
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 A35: natMAX <= k ; :: thesis: not k in { k where k is Element of NAT : run . k in FSet }
now :: thesis: not k in { k where k is Element of NAT : run . k in FSet }
assume k in { k where k is Element of NAT : run . k in FSet } ; :: thesis: contradiction
then consider i1 being object such that
A36: i1 in dom L and
A37: k = L . i1 by A31, FUNCT_1:def 3;
reconsider i1 = i1 as Element of NAT by A36;
i1 in Seg (len L) by A36, FINSEQ_1:def 3;
then ( 1 <= i1 & i1 <= len L ) by FINSEQ_1:1;
then k <= max L by A37, RFINSEQ2:1;
hence contradiction by A35, INT_1:32, 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
A38: for k being Nat st m <= k holds
not k in { k where k is Element of NAT : run . k in FSet } ;
A39: 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 A40: not k in { k where k is Element of NAT : run . k in FSet } by A38;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set r = run . k;
reconsider r = run . k as strict elementary LTLnode over v by A4;
now :: thesis: ( F in the LTLold of (CastNode (r,v)) & not the_right_argument_of F in the LTLold of (CastNode (r,v)) )
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 A40; :: 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;
A41: 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 A39;
then F in * H2(m + 1) by Lm1;
then Shift (w,m) |= F by A41;
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
A42: 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 A43: ( F in the LTLold of H2((m + h) + 1) & not the_right_argument_of F in the LTLold of H2((m + h) + 1) ) by A39;
Shift (w,(m + h)) |= the_right_argument_of F by A42, MODELC_2:80;
hence contradiction by A24, A28, A43; :: 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, the Choice_Function of (BOOL (Subformulae v)))) . 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 ; :: thesis: verum