node ok_since_n_instants(b:bool; n:int) returns (res:bool) = exist cpt: int in assert res = (b and (cpt <= 0)) in cpt = n fby loop { cpt = (if b then (pre cpt-1) else n) }