let w be Element of Inf_seq AtomicFamily; :: thesis: for v being neg-inner-most LTL-formula
for U being Choice_Function of (BOOL (Subformulae v))
for s being strict elementary LTLnode over v st w |= * ('X' s) holds
( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
let v be neg-inner-most LTL-formula; :: thesis: for U being Choice_Function of (BOOL (Subformulae v))
for s being strict elementary LTLnode over v st w |= * ('X' s) holds
( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
let U be Choice_Function of (BOOL (Subformulae v)); :: thesis: for s being strict elementary LTLnode over v st w |= * ('X' s) holds
( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
let s be strict elementary LTLnode over v; :: thesis: ( w |= * ('X' s) implies ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) ) )
set LN = LTLNodes v;
set N = 'X' s;
assume A1: w |= * ('X' s) ; :: thesis: ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
set n = chosen_succ_end_num (w,v,U,('X' s));
set f = choice_succ_func (w,v,U);
set nextnode = CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' s)))) . ('X' s)),v);
A2: 'X' s in LTLNodes v by Def30;
now :: thesis: ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
per cases ( not 'X' s is elementary or 'X' s is elementary ) ;
suppose A3: not 'X' s is elementary ; :: thesis: ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
deffunc H1( set ) -> strict LTLnode over v = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat ((CastNat $1) - 1))) . ('X' s)),v);
set n1 = (chosen_succ_end_num (w,v,U,('X' s))) + 1;
ex L being FinSequence st
( len L = (chosen_succ_end_num (w,v,U,('X' s))) + 1 & ( for k being Nat st k in dom L holds
L . k = H1(k) ) ) from FINSEQ_1:sch 2();
then consider L being FinSequence such that
A4: len L = (chosen_succ_end_num (w,v,U,('X' s))) + 1 and
A5: for k being Nat st k in dom L holds
L . k = H1(k) ;
A6: Seg ((chosen_succ_end_num (w,v,U,('X' s))) + 1) = dom L by A4, FINSEQ_1:def 3;
A7: for k being Nat st 1 <= k & k <= (chosen_succ_end_num (w,v,U,('X' s))) + 1 holds
L . k = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat (k - 1))) . ('X' s)),v)
proof
let k be Nat; :: thesis: ( 1 <= k & k <= (chosen_succ_end_num (w,v,U,('X' s))) + 1 implies L . k = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat (k - 1))) . ('X' s)),v) )
assume ( 1 <= k & k <= (chosen_succ_end_num (w,v,U,('X' s))) + 1 ) ; :: thesis: L . k = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat (k - 1))) . ('X' s)),v)
then k in Seg ((chosen_succ_end_num (w,v,U,('X' s))) + 1) by FINSEQ_1:1;
then L . k = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat ((CastNat k) - 1))) . ('X' s)),v) by A5, A6;
hence L . k = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat (k - 1))) . ('X' s)),v) by MODELC_2:def 1; :: thesis: verum
end;
for k being Nat st 1 <= k & k < len L holds
ex N1, M1 being strict LTLnode over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )
proof
let k be Nat; :: thesis: ( 1 <= k & k < len L implies ex N1, M1 being strict LTLnode over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) )
assume that
A8: 1 <= k and
A9: k < len L ; :: thesis: ex N1, M1 being strict LTLnode over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )
set k1 = k - 1;
reconsider k1 = k - 1 as Nat by A8, NAT_1:21;
set M1 = CastNode ((((choice_succ_func (w,v,U)) |** (k1 + 1)) . ('X' s)),v);
set kp = k + 1;
( 1 <= k + 1 & k + 1 <= (chosen_succ_end_num (w,v,U,('X' s))) + 1 ) by A4, A8, A9, NAT_1:13;
then A10: L . (k + 1) = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat ((k + 1) - 1))) . ('X' s)),v) by A7
.= CastNode ((((choice_succ_func (w,v,U)) |** (k1 + 1)) . ('X' s)),v) by MODELC_2:def 1 ;
set N1 = CastNode ((((choice_succ_func (w,v,U)) |** k1) . ('X' s)),v);
k - 1 < ((chosen_succ_end_num (w,v,U,('X' s))) + 1) - 1 by A4, A9, XREAL_1:14;
then A11: CastNode ((((choice_succ_func (w,v,U)) |** (k1 + 1)) . ('X' s)),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** k1) . ('X' s)),v) by A1, A3, Def48;
L . k = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat k1)) . ('X' s)),v) by A4, A7, A8, A9
.= CastNode ((((choice_succ_func (w,v,U)) |** k1) . ('X' s)),v) by MODELC_2:def 1 ;
hence ex N1, M1 being strict LTLnode over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) by A11, A10; :: thesis: verum
end;
then A12: L is_Finseq_for v ;
A13: 1 <= (chosen_succ_end_num (w,v,U,('X' s))) + 1 by NAT_1:11;
then A14: L . (len L) = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat (((chosen_succ_end_num (w,v,U,('X' s))) + 1) - 1))) . ('X' s)),v) by A4, A7
.= CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' s)))) . ('X' s)),v) by MODELC_2:def 1 ;
A15: CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' s)))) . ('X' s)),v) = chosen_next (w,v,U,s) by A1, A3, Def49;
L . 1 = CastNode ((((choice_succ_func (w,v,U)) |** (CastNat (1 - 1))) . ('X' s)),v) by A13, A7
.= CastNode ((((choice_succ_func (w,v,U)) |** 0) . ('X' s)),v) by MODELC_2:def 1
.= CastNode (((id (LTLNodes v)) . ('X' s)),v) by FUNCT_7:84
.= CastNode (('X' s),v) by A2, FUNCT_1:18
.= 'X' s by Def16 ;
hence ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) ) by A1, A3, A15, A13, A4, A14, A12, Def48; :: thesis: verum
end;
suppose 'X' s is elementary ; :: thesis: ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )
then the LTLnew of ('X' s) = the LTLnew of (FinalNode v) ;
then A16: chosen_next (w,v,U,s) = 'X' s by A1, Def49;
set L = <*('X' s)*>;
A17: Seg 1 = dom <*('X' s)*> by FINSEQ_1:38;
A18: for n being Nat st n in dom <*('X' s)*> holds
<*('X' s)*> . n = 'X' s
proof
let n be Nat; :: thesis: ( n in dom <*('X' s)*> implies <*('X' s)*> . n = 'X' s )
assume n in dom <*('X' s)*> ; :: thesis: <*('X' s)*> . n = 'X' s
then n = 1 by A17, FINSEQ_1:2, TARSKI:def 1;
hence <*('X' s)*> . n = 'X' s by FINSEQ_1:40; :: thesis: verum
end;
for k being Nat st 1 <= k & k < len <*('X' s)*> holds
ex N1, M1 being strict LTLnode over v st
( N1 = <*('X' s)*> . k & M1 = <*('X' s)*> . (k + 1) & M1 is_succ_of N1 ) by FINSEQ_1:39;
then A19: <*('X' s)*> is_Finseq_for v ;
1 in Seg 1 by FINSEQ_1:1;
then ( len <*('X' s)*> = 1 & <*('X' s)*> . 1 = 'X' s ) by A17, A18, FINSEQ_1:39;
hence ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) ) by A1, A16, A19; :: thesis: verum
end;
end;
end;
hence ( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) ) ; :: thesis: verum