let rec clock clk a =
  match a with
  | Variable _
  | True
  | Clock    _
  | Posedge  _
  | Negedge  _   -> a
  | Not   a      -> not_ (clock clk a)
  | And   (a, b) -> and_ (clock clk a) (clock clk b)
  | Next  a      -> until true (not_ clk) (and_ clk (next true (until true (not_ clk) (and_ clk (clock clk a)))))
  | Until (a, b) -> until true (imply clk (clock clk a)) (and_ clk (clock clk b))