node gilbreath_stream(c: bool) returns (o, probe property: bool)
var
  half: bool;
let
  activate
    if c then
      let
        o = false -> not pre o;
      tel 
    else
      let
        o = true -> not pre o;
      tel
  returns o;

  half = false -> not pre half;

  property = true -> not (half and (o = pre o));

  guarantee p_true : property;
tel

node test(i: int) returns (a, b, c: int; exit: bool)
var
  cond: bool;
  o, prop: bool;
let
  exit = i >= 20;
  cond = i mod 3 = 0 and not (i mod 7 = 2);
  c = if cond then 1 else 0;
  o, prop = gilbreath_stream(cond);
  a = if o then 1 else 0;
  b = if prop then 1 else 0;
tel