let F, G, v be LTL-formula; :: thesis: 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 )
let s1, s0, s2 be strict elementary LTLnode of 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 ) )
consider L being FinSequence such that
A4: ( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s0 & L . (len L) = s1 ) by Def215, A1;
set n = len L;
A501: CastNode (L . (len L)),v = s1 by defCastNode01, A4;
then A502: the LTLnew of (CastNode (L . (len L)),v) = {} v by Defelementary;
set F1 = F 'U' G;
a5: CastNode (L . 1),v = 'X' s0 by defCastNode01, A4;
1 < len L by A4, A3, XXREAL_0:1;
then consider m being Nat such that
A7: ( 1 <= m & m < len L ) and
A8: not F 'U' G in the LTLold of (CastNode (L . m),v) and
A9: F 'U' G in the LTLold of (CastNode (L . (m + 1)),v) by ThSucc03, A4, a5, A3, A501;
consider N1, N2 being strict LTLnode of v such that
A10: ( N1 = L . m & N2 = L . (m + 1) & N2 is_succ_of N1 ) by A4, A7, DefFinseq;
A101: CastNode (L . m),v = N1 by defCastNode01, A10;
A102: CastNode (L . (m + 1)),v = N2 by defCastNode01, A10;
A11: N2 is_succ_of N1,F 'U' G by A8, A9, A101, A102, A10, ThSucc04;
A1201: the LTLold of N1 c= the LTLold of s1 by A4, A7, ThSucc07, A501, A101;
set m1 = m + 1;
A120101: ( len L <= len L & m + 1 <= len L & 1 <= m + 1 ) by A7, NAT_1:13;
then A1202: the LTLnext of N2 c= the LTLnext of s1 by A4, ThSucc07, A501, A102;
A1203: the LTLnew of N2 c= the LTLold of s1 by A4, A120101, A502, ThSucc10, A102, A501;
A13: F 'U' G is Until by MODELC_2:def 16;
then A1301: the_left_argument_of (F 'U' G) = F by MODELC_2:def 19;
A1302: the_right_argument_of (F 'U' G) = G by A13, MODELC_2:def 20;
A14: LTLNew1 (F 'U' G) = {F} by A13, A1301, Def203;
A15: LTLNew2 (F 'U' G) = {G} by A13, A1302, Def204;
A16: LTLNext (F 'U' G) = {(F 'U' G)} by A13, Def205;
( not G in the LTLold of s1 implies ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) )

proof

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

now

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 A11, DefSucc01;

suppose B2: ( 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 Def206;
then C1: (LTLNew1 (F 'U' G)) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
C2: F in the LTLold of s1

proof

now

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 A1201; :: thesis: verum

end;

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

F in LTLNew1 (F 'U' G) by A14, TARSKI:def 1;
then F in (LTLNew1 (F 'U' G)) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then F in the LTLnew of N2 by C1;
hence F in the LTLold of s1 by A1203; :: 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 B2, Def206;
then C3: LTLNext (F 'U' G) c= the LTLnext of N2 by XBOOLE_1:7;
F 'U' G in LTLNext (F 'U' G) by A16, TARSKI:def 1;
then F 'U' G in the LTLnext of N2 by C3;
then C4: F 'U' G in the LTLnext of s1 by A1202;
the LTLnext of s1 c= the LTLold of s2 by ThNext01, A2;
hence ( F in the LTLold of s1 & F 'U' G in the LTLold of s2 ) by C4, C2; :: 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 Def207;
then C1: (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

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 A1201; :: thesis: verum

end;

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

G in LTLNew2 (F 'U' G) by A15, TARSKI:def 1;
then G in (LTLNew2 (F 'U' G)) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then G in the LTLnew of N2 by C1;
hence G in the LTLold of s1 by A1203; :: 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 B0; :: 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