module obj. 
import helmet.

type stack list Element -> o. 
type pop o.
type push Element -> o.
type top  Element -> o.
  
true || pop     || stack (X::S)  --> anti || stack S.
true || push Y  || stack S       --> anti || stack (Y::S).
true || top  X  || stack (X::S)  --> anti || stack (X::S).

kind specifier type.

type point   specifier -> int -> o.
type point2D int -> int -> o. 
type x specifier.
type y specifier.
type move specifier -> int -> o.
type get  specifier -> int -> o.

(Nx is X + Dx) || move Spec Dx    || point   Spec X            --> anti         || point Spec Nx.
write X        || get  Spec X     || point   Spec X            --> anti         || point Spec X.
true           || move Spec D     || point2D X    Y            --> move Spec D  || point x X | point y Y.
true           || get  Spec D     || point2D X    Y            --> get  Spec D  || point x X | point y Y.
true           || anti            || point x X  | point y  Y   --> anti         || point2D X Y.

type start o.
start:- initial (point2D 0 0)  => ehhfsolve (move x 3 | move y 4 | get x Z).