node always(i : bool) returns (o : bool);
var prev : bool;
let
  prev = true -> pre o;
  o = if i then prev else false; 
tel

node count_true(i : bool) returns (o : int);
var prev : int;
let
  prev = 0 -> pre o;
  o = if i then prev + 1 else prev;
tel

node count_succ_true(i : bool) returns (o : int);
var
  prev_i : bool;
  prev_o : int;
let
  prev_i = false -> pre i;
  prev_o = 0 -> pre o;
  o = if i and prev_i then prev_o + 1 else prev_o;
tel

node bounds(i : int) returns (min, max : int);
var prev_min, prev_max : int;
let
  prev_min = i -> pre min;
  prev_max = i -> pre max;
  min = if (i < prev_min) then i else prev_min;
  max = if (i > prev_max) then i else prev_max;
tel