let r be Element of Inf_seq AtomicFamily; :: thesis: for W being Subset of LTL_WFF holds
( r |= 'X' W iff Shift (r,1) |= W )
let W be Subset of LTL_WFF; :: thesis: ( r |= 'X' W iff Shift (r,1) |= W )
A1: ( Shift (r,1) |= W implies r |= 'X' W )

proof

assume A2: Shift (r,1) |= W ; :: thesis: r |= 'X' W
A3: for u being LTL-formula st u in W holds
r |= 'X' u by A2, Th67;
for H being LTL-formula st H in 'X' W holds
r |= H

proof

let H be LTL-formula; :: thesis: ( H in 'X' W implies r |= H )
assume H in 'X' W ; :: thesis: r |= H
then ex x being LTL-formula st
( H = x & ex u being LTL-formula st
( u in W & x = 'X' u ) ) ;
hence r |= H by A3; :: thesis: verum

end;

hence r |= 'X' W ; :: thesis: verum

end;

( r |= 'X' W implies Shift (r,1) |= W )

proof

assume A4: r |= 'X' W ; :: thesis: Shift (r,1) |= W
for H being LTL-formula st H in W holds
Shift (r,1) |= H

proof

let H be LTL-formula; :: thesis: ( H in W implies Shift (r,1) |= H )
set u = 'X' H;
assume H in W ; :: thesis: Shift (r,1) |= H
then 'X' H in 'X' W ;
then r |= 'X' H by A4;
hence Shift (r,1) |= H by Th67; :: thesis: verum

end;

hence Shift (r,1) |= W ; :: thesis: verum

end;

hence ( r |= 'X' W iff Shift (r,1) |= W ) by A1; :: thesis: verum