node always_since
  (a: bool;
  b: bool)
returns
  (o: bool);

var
  V9_prev_o: bool;

let
  o = (if b then a else (V9_prev_o and a));
  V9_prev_o = (false -> (pre o));
tel