Quelle bug_3217.v Sprache: Coq

(** [Set Implicit Arguments] causes Coq to run out of memory on [Qed] before c3feef4ed5dec126f1144dec91eee9c0f0522a94 *)
Set Implicit Arguments.

Parameter LEM: forall P : Prop, sumbool P (P -> False).

Definition pmap := option (nat -> option nat).

Definition pmplus (oha ohb: pmap) : pmap :=
match oha, ohb with
| Some ha, Some hb =>
   if LEM (oha = ohb) then None else None
| _, _ => None
end.

Definition pmemp: pmap := Some (fun _ => None).

Lemma foo:
True ->
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
     pmemp))))))))))))
    =
    None -> True.
Proof.
  auto.
Timeout 2 Qed.

quality98%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.