coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Yves Strub <pierre-yves AT strub.nu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] 2048
- Date: Sun, 30 Mar 2014 16:51:18 +0200
With an oracle, thm1 is ok. For thm2...
Lemma thm1 : exists ms, g2048 seed ms.
Proof.
set (ms := Dm :: Dm :: Dm :: Dm :: Rm :: Dm :: Rm ::
Dm :: Rm :: Dm :: Lm :: Rm :: Dm :: Rm ::
Rm :: Rm :: Dm :: Rm :: Dm :: Lm :: Dm ::
Dm :: Rm :: Dm :: Dm :: Rm :: Dm :: Dm ::
Rm :: Rm :: Dm :: Rm :: Dm :: Rm :: Dm ::
Dm :: Rm :: Dm :: Dm :: Dm :: Dm :: Dm ::
Rm :: Rm :: Rm :: Dm :: Rm :: Dm :: Rm ::
Rm :: Dm :: Dm :: Rm :: Dm :: Dm :: Rm ::
Rm :: Dm :: Lm :: Dm :: Rm :: Dm :: Dm ::
Rm :: Lm :: Rm :: Dm :: Lm :: Dm :: Rm ::
Dm :: Dm :: Lm :: Dm :: Lm :: Rm :: Dm ::
Dm :: Rm :: Dm :: Dm :: Rm :: Rm :: Dm ::
Dm :: Lm :: Dm :: Rm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Dm :: Rm :: Dm :: Lm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Rm :: Rm ::
Dm :: Dm :: Lm :: Dm :: Rm :: Dm :: Dm ::
Lm :: Dm :: Dm :: Lm :: Rm :: Dm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Dm :: Dm ::
Rm :: Dm :: Lm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Rm :: Dm :: Dm :: Rm :: Dm ::
Dm :: Rm :: Dm :: Dm :: Lm :: Rm :: Dm ::
Dm :: Rm :: Rm :: Dm :: Dm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Rm :: Dm :: Dm :: Dm :: Rm :: Lm :: Rm ::
Dm :: Lm :: Rm :: Dm :: Lm :: Dm :: Dm ::
Lm :: Dm :: Rm :: Dm :: Dm :: Rm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Dm :: Dm ::
Dm :: Rm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Lm :: Dm :: Rm :: Rm :: Dm :: Dm :: Dm ::
Dm :: Dm :: Rm :: Dm :: Lm :: Dm :: Dm ::
Lm :: Dm :: Rm :: Dm :: Lm :: Dm :: Rm ::
Dm :: Dm :: Dm :: Dm :: Rm :: Dm :: Lm ::
Lm :: Rm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Lm :: Dm :: Rm :: Dm :: Dm :: Dm ::
Dm :: Dm :: Lm :: Rm :: Dm :: Dm :: Rm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Lm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Rm :: Lm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Dm :: Lm :: Rm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Rm :: Rm ::
Rm :: Dm :: Lm :: Dm :: Rm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Dm :: Dm :: Dm :: Rm ::
Dm :: Lm :: Rm :: Lm :: Dm :: Rm :: Dm ::
Lm :: Rm :: Dm :: Lm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Lm :: Rm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Rm :: Dm :: Dm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Dm :: Lm ::
Dm :: Dm :: Lm :: Dm :: Rm :: Rm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Rm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Rm :: Dm :: Lm :: Dm :: Dm ::
Lm :: Lm :: Dm :: Lm :: Dm :: Dm :: Dm ::
Rm :: Dm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Dm :: Lm :: Dm :: Lm :: Dm :: Rm ::
Rm :: Dm :: Dm :: Rm :: Dm :: Dm :: Rm ::
Dm :: Dm :: Lm :: Rm :: Dm :: Lm :: Dm ::
Rm :: Dm :: Dm :: Dm :: Dm :: Dm :: Rm ::
Dm :: Lm :: Rm :: Dm :: Dm :: Lm :: Dm ::
Rm :: Rm :: Lm :: Dm :: Rm :: Dm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Dm :: Lm ::
Dm :: Dm :: Lm :: Dm :: Lm :: Dm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Rm :: Lm :: Dm ::
Dm :: Dm :: Dm :: Lm :: Rm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Dm :: Rm :: Dm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Dm :: Dm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Lm :: Rm :: Dm ::
Lm :: Dm :: Dm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Dm :: Lm :: Rm :: Dm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Rm :: Lm :: Dm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Rm :: Dm :: Lm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Lm :: Dm :: Dm ::
Lm :: Dm :: Rm :: Dm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Dm :: Lm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Rm :: Lm ::
Dm :: Lm :: Dm :: Rm :: Lm :: Dm :: Lm ::
Rm :: Lm :: Dm :: Rm :: Dm :: Lm :: Lm ::
Dm :: Dm :: Rm :: Rm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Rm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Dm :: Dm :: Lm :: Dm ::
Lm :: Dm :: Rm :: Dm :: Dm :: Lm :: Dm ::
Rm :: Dm :: Rm :: Dm :: Lm :: Dm :: Dm ::
Lm :: Dm :: Rm :: Dm :: Rm :: Dm :: Lm ::
Dm :: Rm :: Dm :: Lm :: Rm :: Dm :: Lm ::
Dm :: Dm :: Rm :: Dm :: Lm :: Dm :: Rm ::
Dm :: Lm :: Dm :: Rm :: Dm :: Dm :: Rm ::
Dm :: Dm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Lm :: Dm :: Dm :: Dm :: Lm ::
Dm :: Lm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Rm :: Dm :: Dm :: Dm :: Lm ::
Rm :: Dm :: Rm :: Dm :: Rm :: Dm :: Dm ::
Lm :: Dm :: Rm :: Dm :: Lm :: Dm :: Rm ::
Dm :: Dm :: Dm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Rm :: Dm :: Lm ::
Dm :: Dm :: Lm :: Dm :: Lm :: Dm :: Rm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Dm :: Dm :: Dm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Rm :: Lm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Rm :: Dm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Lm :: Dm ::
Dm :: Lm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Dm :: Lm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Lm :: Dm :: Dm :: Rm :: Lm ::
Dm :: Lm :: Dm :: Rm :: Dm :: Dm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Rm :: Lm :: Dm ::
Rm :: Lm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Rm :: Lm :: Dm :: Lm :: Dm :: Rm :: Lm ::
Dm :: Rm :: Lm :: Dm :: Rm :: Lm :: Lm ::
Rm :: Lm :: Dm :: Dm :: Lm :: Dm :: Rm ::
Rm :: Dm :: Dm :: Dm :: Dm :: Dm :: Dm ::
Dm :: Dm :: Dm :: Lm :: Dm :: Rm :: Dm ::
Dm :: Lm :: Dm :: Dm :: Rm :: Dm :: Lm ::
Dm :: Dm :: Lm :: Lm :: Dm :: Lm :: Lm ::
Dm :: Dm :: Dm :: Rm :: Dm :: Lm :: Dm ::
Dm :: Dm :: Dm :: Rm :: Dm :: Rm :: Dm ::
Dm :: Dm :: Lm :: Dm :: Dm :: Rm :: Dm ::
Dm :: Lm :: Dm :: Rm :: Dm :: Lm :: Lm ::
Dm :: Dm :: Rm :: Dm :: Lm :: Dm :: Rm ::
Dm :: Lm :: Dm :: Lm :: Dm :: Rm :: Dm ::
Lm :: Dm :: Lm :: Dm :: Lm :: Dm :: Dm ::
Rm :: Lm :: Dm :: Dm :: Lm :: Dm :: Dm ::
Lm :: Dm :: Rm :: Lm :: Dm :: Dm :: Dm ::
Dm :: Dm :: Rm :: Lm :: Dm :: Dm :: Lm ::
Dm :: Dm :: Dm :: Rm :: Lm :: Dm :: Dm ::
Dm :: Lm :: Rm :: Lm :: Dm :: Lm :: Dm ::
Rm :: Lm :: Dm :: Rm :: Lm :: Dm :: Rm ::
Lm :: Lm :: Rm :: Lm :: Dm :: Dm :: Lm ::
Dm :: Rm :: Lm :: Dm :: Dm :: Dm :: Dm ::
Rm :: Lm :: Dm :: Dm :: Dm :: Lm :: Rm ::
Lm :: Dm :: Lm :: Dm :: Dm :: Rm :: Lm ::
Dm :: Rm :: Dm :: Lm :: Dm :: Rm :: Lm ::
Dm :: Rm :: Lm :: Rm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Lm :: Dm :: Rm :: Lm :: Dm ::
Rm :: Lm :: Lm :: Rm :: Lm :: Dm :: Dm ::
Dm :: Lm :: Rm :: Lm :: Dm :: Lm :: Rm ::
Lm :: Dm :: Rm :: Dm :: Rm :: Rm :: Lm ::
Rm :: Dm :: Dm :: Lm :: Lm :: Dm :: Lm ::
Dm :: Dm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Rm :: Lm :: Dm :: Lm :: Dm :: Rm ::
Lm :: Dm :: Lm :: Rm :: Lm :: Dm :: Rm ::
Lm :: Lm :: Rm :: Lm :: Dm :: Rm :: Dm ::
Rm :: Rm :: Dm :: Dm :: Lm :: Dm :: Lm ::
Dm :: Dm :: Rm :: Lm :: Dm :: Rm :: Dm ::
Dm :: Rm :: Lm :: Dm :: Lm :: Rm :: Lm ::
Lm :: Rm :: Dm :: Lm :: Rm :: Dm :: Lm ::
Dm :: Lm :: Lm :: Dm :: Rm :: Rm :: nil).
exists ms; vm_compute; trivial.
Qed.
Pierre-Yves.
- [Coq-Club] 2048, Laurent Théry, 03/30/2014
- Re: [Coq-Club] 2048, Kevin Sullivan, 03/30/2014
- Re: [Coq-Club] 2048, Matthieu Sozeau, 03/30/2014
- Re: [Coq-Club] 2048, AUGER Cédric, 03/30/2014
- Re: [Coq-Club] 2048, Pierre-Yves Strub, 03/30/2014
- Re: [Coq-Club] 2048, Laurent Théry, 03/30/2014
- Re: [Coq-Club] 2048, Laurent Théry, 03/30/2014
- Re: [Coq-Club] 2048, Gabriel Scherer, 03/30/2014
- Re: [Coq-Club] 2048, Pierre-Yves Strub, 03/30/2014
Archive powered by MHonArc 2.6.18.