The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Or not. My apologies then for the fail.

I thought that it's related to the previous Takeuchi function problem (and therefore with the same function).

On Tue, Jan 7, 2014 at 1:46 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Require Import ZArith.
Open Scope Z_scope.

Inductive tak : Z -> Z -> Z -> Z -> Prop :=
  | tak_base : forall x y z, x <= y -> tak x y z z
  | tak_call : forall x y z a b c r,
    y < x ->
    tak (x-1) y z a -> 
    tak (y-1) z x b ->
    tak (z-1) x y c ->
    tak a b c r ->
    tak x y z r.

I believe that there must be "tak_base : forall x y z, x <= y -> tak x y z y", not "tak x y z z".

(I don't know poster of the problem, so I sent this email to coq-club too.)