-- HORSEMAN: relation between men, horses and their heads and feet:
data Nat = O | S Nat
-- translate integers to nat-terms:
int2nat :: Int -> Nat
int2nat n = if n<=0 then O else S(int2nat (n-1))
-- addition on naturals:
add O n = n
add (S m) n = S (add m n)
horseman m h heads feet =
heads =:= add m h & feet =:= add (add m m) (add (add h h) (add h h))
-- How many men and horses have 3 heads and 8 feet?
goal1 m h = horseman m h (S(S(S O))) (S(S(S(S(S(S(S(S O))))))))
-- How many men and horses have 8 heads and 20 feet?
goal2 m h = horseman m h (int2nat 8) (int2nat 20)
-- Relation between men and horses feets with 2 heads:
goal3 m h hd = horseman m h (S (S O)) hd