I came across an example in which the case-splitting is similar to the
Majority Function.
f :: Nat -> Nat -> Nat -> Nat
f 0 0 0 = 1
f 0 (succ y) z = g1 y z
f (succ x) y 0 = g2 x y
f x 0 (succ z) = g3 x z
f (succ x) (succ y) (succ z) = f (succ x) (succ y) z +
f (succ x) y (succ z) +
f x (succ y) (succ z)
where g1 g2 and g3 were defined beforehand.
As we discussed before, this kind of functions cannot be defined by the
eliminator (of Nat) to satisfy every equation computationally. We have to
modify the function to the one that has 8 cases. However, if we don't care
whether it is total (ie, if we allow partially defined function), then it
can be defined as it is.
Cheers,
Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent
