let F, G, v be LTL-formula; :: thesis: for s0, s1, s2 being strict elementary LTLnode over 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 )
let s0, s1, s2 be strict elementary LTLnode over v; :: thesis: ( 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 implies ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) )
assume that
A1: s1 is_next_of s0 and
A2: s2 is_next_of s1 and
A3: F 'U' G in the LTLold of s1 ; :: thesis: ( G in the LTLold of s1 or ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) )
set F1 = F 'U' G;
consider L being FinSequence such that
A4: 1 <= len L and
A5: L is_Finseq_for v and
A6: L . 1 = 'X' s0 and
A7: L . (len L) = s1 by A1;
A8: CastNode ((L . 1),v) = 'X' s0 by A6, Def16;
set n = len L;
A9: CastNode ((L . (len L)),v) = s1 by A7, Def16;
1 < len L by A3, A4, A6, A7, XXREAL_0:1;
then consider m being Nat such that
A10: ( 1 <= m & m < len L ) and
A11: ( not F 'U' G in the LTLold of (CastNode ((L . m),v)) & F 'U' G in the LTLold of (CastNode ((L . (m + 1)),v)) ) by A3, A5, A9, A8, Th27;
consider N1, N2 being strict LTLnode over v such that
A12: N1 = L . m and
A13: N2 = L . (m + 1) and
A14: N2 is_succ_of N1 by A5, A10;
set m1 = m + 1;
A15: CastNode ((L . (m + 1)),v) = N2 by A13, Def16;
A16: F 'U' G is Until ;
then A17: LTLNext (F 'U' G) = {(F 'U' G)} by Def3;
the_right_argument_of (F 'U' G) = G by A16, MODELC_2:def 20;
then A18: LTLNew2 (F 'U' G) = {G} by A16, Def2;
the_left_argument_of (F 'U' G) = F by A16, MODELC_2:def 19;
then A19: LTLNew1 (F 'U' G) = {F} by A16, Def1;
A20: CastNode ((L . m),v) = N1 by A12, Def16;
then A21: the LTLold of N1 c= the LTLold of s1 by A5, A9, A10, Th31;
A22: ( m + 1 <= len L & 1 <= m + 1 ) by A10, NAT_1:13;
then A23: the LTLnext of N2 c= the LTLnext of s1 by A5, A9, A15, Th31;
the LTLnew of (CastNode ((L . (len L)),v)) = {} v by A9, Def11;
then A24: the LTLnew of N2 c= the LTLold of s1 by A5, A9, A15, A22, Th34;
A25: N2 is_succ_of N1,F 'U' G by A11, A14, A20, A15, Th28;
( not G in the LTLold of s1 implies ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) )

proof

assume A26: not G in the LTLold of s1 ; :: thesis: ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 )

now :: thesis: ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 )

per cases ( ( F 'U' G in the LTLnew of N1 & N2 = SuccNode1 ((F 'U' G),N1) ) or ( F 'U' G in the LTLnew of N1 & ( F 'U' G is disjunctive or F 'U' G is Until or F 'U' G is Release ) & N2 = SuccNode2 ((F 'U' G),N1) ) ) by A25;

suppose A27: ( F 'U' G in the LTLnew of N1 & N2 = SuccNode1 ((F 'U' G),N1) ) ; :: thesis: ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 )

then the LTLnew of N2 = ( the LTLnew of N1 \ {(F 'U' G)}) \/ ((LTLNew1 (F 'U' G)) \ the LTLold of N1) by Def4;
then A28: (LTLNew1 (F 'U' G)) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
A29: F in the LTLold of s1

proof

now :: thesis: F in the LTLold of s1

per cases ( F in the LTLold of N1 or not F in the LTLold of N1 ) ;

suppose F in the LTLold of N1 ; :: thesis: F in the LTLold of s1

hence F in the LTLold of s1 by A21; :: thesis: verum

end;

suppose A30: not F in the LTLold of N1 ; :: thesis: F in the LTLold of s1

F in LTLNew1 (F 'U' G) by A19, TARSKI:def 1;
then F in (LTLNew1 (F 'U' G)) \ the LTLold of N1 by A30, XBOOLE_0:def 5;
then F in the LTLnew of N2 by A28;
hence F in the LTLold of s1 by A24; :: thesis: verum

end;

end;

end;

hence F in the LTLold of s1 ; :: thesis: verum

end;

the LTLnext of N2 = the LTLnext of N1 \/ (LTLNext (F 'U' G)) by A27, Def4;
then A31: LTLNext (F 'U' G) c= the LTLnext of N2 by XBOOLE_1:7;
F 'U' G in LTLNext (F 'U' G) by A17, TARSKI:def 1;
then F 'U' G in the LTLnext of N2 by A31;
then A32: F 'U' G in the LTLnext of s1 by A23;
the LTLnext of s1 c= the LTLold of s2 by A2, Th37;
hence ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) by A29, A32; :: thesis: verum

end;

suppose ( F 'U' G in the LTLnew of N1 & ( F 'U' G is disjunctive or F 'U' G is Until or F 'U' G is Release ) & N2 = SuccNode2 ((F 'U' G),N1) ) ; :: thesis: ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 )

then the LTLnew of N2 = ( the LTLnew of N1 \ {(F 'U' G)}) \/ ((LTLNew2 (F 'U' G)) \ the LTLold of N1) by Def5;
then A33: (LTLNew2 (F 'U' G)) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
G in the LTLold of s1

proof

now :: thesis: G in the LTLold of s1

per cases ( G in the LTLold of N1 or not G in the LTLold of N1 ) ;

suppose G in the LTLold of N1 ; :: thesis: G in the LTLold of s1

hence G in the LTLold of s1 by A21; :: thesis: verum

end;

suppose A34: not G in the LTLold of N1 ; :: thesis: G in the LTLold of s1

G in LTLNew2 (F 'U' G) by A18, TARSKI:def 1;
then G in (LTLNew2 (F 'U' G)) \ the LTLold of N1 by A34, XBOOLE_0:def 5;
then G in the LTLnew of N2 by A33;
hence G in the LTLold of s1 by A24; :: thesis: verum

end;

end;

end;

hence G in the LTLold of s1 ; :: thesis: verum

end;

hence ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) by A26; :: thesis: verum

end;

end;

end;

hence ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) ; :: thesis: verum

end;

hence ( G in the LTLold of s1 or ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) ) ; :: thesis: verum