let H, v be LTL-formula; :: thesis:
let N be strict LTLnode over v; :: thesis:
let w be Element of Inf_seq AtomicFamily; :: thesis:
assume that
A1: H in the LTLnew of N and
A2: H is Until ; :: thesis:
set NX = the LTLnext of N;
set SN1 = SuccNode1 (H,N);
A3: H in * N by A1, Lm1;
set SN1X = the LTLnext of (SuccNode1 (H,N));
LTLNext H = {H} by A2, Def3;
then A4: the LTLnext of (SuccNode1 (H,N)) = the LTLnext of N \/ {H} by A1, Def4;
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SN2 = SuccNode2 (H,N);
set H2 = the_right_argument_of H;
set SN2N = the LTLnew of (SuccNode2 (H,N));
LTLNew2 H = {(the_right_argument_of H)} by A2, Def2;
then A5: the LTLnew of (SuccNode2 (H,N)) = ( the LTLnew of N \ {H}) \/ ({(the_right_argument_of H)} \ the LTLold of N) by A1, Def5;
set H1 = the_left_argument_of H;
set XNX = 'X' (CastLTL the LTLnext of N);
set XSN1X = 'X' (CastLTL the LTLnext of (SuccNode1 (H,N)));
set SN1N = the LTLnew of (SuccNode1 (H,N));
set SN1O = the LTLold of (SuccNode1 (H,N));
A6: the LTLold of (SuccNode1 (H,N)) = the LTLold of N \/ {H} by A1, Def4;
LTLNew1 H = {(the_left_argument_of H)} by A2, Def1;
then A7: the LTLnew of (SuccNode1 (H,N)) = ( the LTLnew of N \ {H}) \/ ({(the_left_argument_of H)} \ the LTLold of N) by A1, Def4;
A8: for F being LTL-formula holds
( not F in * (SuccNode1 (H,N)) or F in * N or F = the_left_argument_of H or F = 'X' H )

proof

let F be LTL-formula; :: thesis:
assume A9: F in * (SuccNode1 (H,N)) ; :: thesis:

now :: thesis:

per cases by A9, Lm1;

suppose F in the LTLold of (SuccNode1 (H,N)) ; :: thesis:

then ( F in the LTLold of N or F in {H} ) by A6, XBOOLE_0:def 3;
hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by A3, Lm1, TARSKI:def 1; :: thesis:

end;

suppose F in the LTLnew of (SuccNode1 (H,N)) ; :: thesis:

then ( F in the LTLnew of N \ {H} or F in {(the_left_argument_of H)} \ the LTLold of N ) by A7, XBOOLE_0:def 3;
then ( F in the LTLnew of N or F in {(the_left_argument_of H)} ) by XBOOLE_0:def 5;
hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by Lm1, TARSKI:def 1; :: thesis:

end;

suppose F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N))) ; :: thesis:

then consider G being LTL-formula such that
A10: F = G and
A11: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of (SuccNode1 (H,N)) & G = 'X' G1 ) ;
consider G1 being LTL-formula such that
A12: G1 in the LTLnext of (SuccNode1 (H,N)) and
A13: G = 'X' G1 by A11;
A14: ( G1 in the LTLnext of N or G1 in {H} ) by A4, A12, XBOOLE_0:def 3;

now :: thesis:

per cases by A14, TARSKI:def 1;

suppose G1 in the LTLnext of N ; :: thesis:

then F in 'X' (CastLTL the LTLnext of N) by A10, A13;
hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by Lm1; :: thesis:

end;

suppose G1 = H ; :: thesis:

hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by A10, A13; :: thesis:

end;

hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) ; :: thesis:

end;

hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) ; :: thesis:

end;

set SN2X = the LTLnext of (SuccNode2 (H,N));
set XSN2X = 'X' (CastLTL the LTLnext of (SuccNode2 (H,N)));
set SN2O = the LTLold of (SuccNode2 (H,N));
A15: the LTLold of (SuccNode2 (H,N)) = the LTLold of N \/ {H} by A1, Def5;
A16: the LTLnext of (SuccNode2 (H,N)) = the LTLnext of N by A1, Def5;
A17: for F being LTL-formula holds
( not F in * (SuccNode2 (H,N)) or F in * N or F = the_right_argument_of H )

proof

let F be LTL-formula; :: thesis:
assume A18: F in * (SuccNode2 (H,N)) ; :: thesis:

now :: thesis:

per cases by A18, Lm1;

suppose F in the LTLold of (SuccNode2 (H,N)) ; :: thesis:

then ( F in the LTLold of N or F in {H} ) by A15, XBOOLE_0:def 3;
hence ( F in * N or F = the_right_argument_of H ) by A3, Lm1, TARSKI:def 1; :: thesis:

end;

suppose F in the LTLnew of (SuccNode2 (H,N)) ; :: thesis:

then ( F in the LTLnew of N \ {H} or F in {(the_right_argument_of H)} \ the LTLold of N ) by A5, XBOOLE_0:def 3;
then ( F in the LTLnew of N or F in {(the_right_argument_of H)} ) by XBOOLE_0:def 5;
hence ( F in * N or F = the_right_argument_of H ) by Lm1, TARSKI:def 1; :: thesis:

end;

suppose F in 'X' (CastLTL the LTLnext of (SuccNode2 (H,N))) ; :: thesis:

hence ( F in * N or F = the_right_argument_of H ) by A16, Lm1; :: thesis:

end;

hence ( F in * N or F = the_right_argument_of H ) ; :: thesis:

end;

H = (the_left_argument_of H) 'U' (the_right_argument_of H) by A2, MODELC_2:8;
then ( w |= H iff w |= (the_right_argument_of H) 'or' ((the_left_argument_of H) '&' ('X' H)) ) by MODELC_2:75;
then A19: ( w |= H iff ( w |= the_right_argument_of H or w |= (the_left_argument_of H) '&' ('X' H) ) ) by MODELC_2:66;
A20: ( not w |= * N or w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )

proof

assume A21: w |= * N ; :: thesis:

now :: thesis:

per cases by A3, A19, A21, MODELC_2:65;

suppose A22: ( w |= the_left_argument_of H & w |= 'X' H ) ; :: thesis:

for F being LTL-formula st F in * (SuccNode1 (H,N)) holds
w |= F by A8, A21, A22;
hence ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis:

end;

suppose A23: w |= the_right_argument_of H ; :: thesis:

for F being LTL-formula st F in * (SuccNode2 (H,N)) holds
w |= F by A17, A21, A23;
hence ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis:

end;

hence ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis:

end;

A24: for F being LTL-formula st F in * N holds
( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

proof

let F be LTL-formula; :: thesis:
assume A25: F in * N ; :: thesis:

now :: thesis:

per cases by A25, Lm1;

suppose F in the LTLold of N ; :: thesis:

then ( F in the LTLold of (SuccNode1 (H,N)) & F in the LTLold of (SuccNode2 (H,N)) ) by A6, A15, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by Lm1; :: thesis:

end;

suppose A26: F in the LTLnew of N ; :: thesis:

now :: thesis:

per cases ;

suppose F = H ; :: thesis:

then F in {H} by TARSKI:def 1;
then ( F in the LTLold of (SuccNode1 (H,N)) & F in the LTLold of (SuccNode2 (H,N)) ) by A6, A15, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by Lm1; :: thesis:

end;

suppose F <> H ; :: thesis:

then not F in {H} by TARSKI:def 1;
then F in the LTLnew of N \ {H} by A26, XBOOLE_0:def 5;
then ( F in the LTLnew of (SuccNode1 (H,N)) & F in the LTLnew of (SuccNode2 (H,N)) ) by A7, A5, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by Lm1; :: thesis:

end;

hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) ; :: thesis:

end;

suppose F in 'X' (CastLTL the LTLnext of N) ; :: thesis:

then consider G being LTL-formula such that
A27: F = G and
A28: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of N & G = 'X' G1 ) ;
consider G1 being LTL-formula such that
A29: G1 in the LTLnext of N and
A30: G = 'X' G1 by A28;
G1 in the LTLnext of (SuccNode1 (H,N)) by A4, A29, XBOOLE_0:def 3;
then A31: F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N))) by A27, A30;
F in 'X' (CastLTL the LTLnext of (SuccNode2 (H,N))) by A16, A27, A29, A30;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by A31, Lm1; :: thesis:

end;

hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) ; :: thesis:

end;

( ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) implies w |= * N )

proof

assume A32: ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis:
for F being LTL-formula st F in * N holds
w |= F

proof

let F be LTL-formula; :: thesis:
assume A33: F in * N ; :: thesis:
then A34: F in * (SuccNode2 (H,N)) by A24;
A35: F in * (SuccNode1 (H,N)) by A24, A33;

now :: thesis:

per cases by A32;

suppose w |= * (SuccNode1 (H,N)) ; :: thesis:

hence w |= F by A35; :: thesis:

end;

suppose w |= * (SuccNode2 (H,N)) ; :: thesis:

hence w |= F by A34; :: thesis:

end;

hence w |= F ; :: thesis:

end;

hence w |= * N ; :: thesis:

end;

hence ( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ) by A20; :: thesis: