module prog. 
import helmet.

type new o. 
type count   int -> o. 
type inc     int -> o.
type howmany int -> int -> o.
type nocounters o.

new  ||  anti  --> anti || count 0.

type p int -> int -> int -> o.
type go  o.
 
p X Z Y  :- Y is X + Z.
 
p X Z Y >> 
  inc Z || (count X) -->  anti  || count Y.

howmany N N || anti.  

(Z is N + 1) >>
   howmany N M || (count X) --> howmany Z M || anti.   

nocounters  || anti      --> howmany 0 0 || anti. 
go          || anti      -->  
         (nocounters & (new | (inc 1) | (inc 3))) || anti. 

type start o.
initial anti.

start:- ehhfsolve go.
start:- spyon => ehhfsolve go.