let w be Element of Inf_seq AtomicFamily; :: thesis: for v being neg-inner-most LTL-formula
for N being strict LTLnode over v st w |= * N holds
Shift (w,1) |= * ('X' N)
let v be neg-inner-most LTL-formula; :: thesis: for N being strict LTLnode over v st w |= * N holds
Shift (w,1) |= * ('X' N)
let N be strict LTLnode over v; :: thesis: ( w |= * N implies Shift (w,1) |= * ('X' N) )
set XN = 'X' N;
assume A1: w |= * N ; :: thesis: Shift (w,1) |= * ('X' N)
for H being LTL-formula st H in 'X' (CastLTL the LTLnext of N) holds
w |= H

proof

let H be LTL-formula; :: thesis: ( H in 'X' (CastLTL the LTLnext of N) implies w |= H )
assume H in 'X' (CastLTL the LTLnext of N) ; :: thesis: w |= H
then H in * N by Lm1;
hence w |= H by A1; :: thesis: verum

end;

then A2: w |= 'X' (CastLTL the LTLnext of N) ;
* ('X' N) = CastLTL the LTLnext of N by Lm33;
hence Shift (w,1) |= * ('X' N) by A2, MODELC_2:77; :: thesis: verum