coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Possible bug in specification of the problem "Termination of tak"

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: i AT yoichihirai.com, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Possible bug in specification of the problem "Termination of tak"
Date: Tue, 7 Jan 2014 13:46:03 +0200

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.)

[Coq-Club] Possible bug in specification of the problem "Termination of tak", Ilmārs Cīrulis, 01/07/2014
- Re: [Coq-Club] Possible bug in specification of the problem "Termination of tak", Ilmārs Cīrulis, 01/07/2014