----------------- MODULE AltImplementsOsc  -----------------
EXTENDS Alternation, Naturals

OscSpec == (x=0) /\ [][x' = (x+1)%2]_x

THEOREM AltSpec => OscSpec
=============================================================