Add DisjointSetUnionCode3.v

huynhtrankhanh · Nov 16, 2024 · 31f07b9 · 31f07b9
1 parent cf6b85e
commit 31f07b9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -28,5 +28,6 @@ theories/DisjointSetUnion.v
 theories/CountingBits.v
 theories/DisjointSetUnionCode.v
 theories/DisjointSetUnionCode2.v
+theories/DisjointSetUnionCode3.v
 -R generated-coq/ Generated
 generated-coq/DisjointSetUnion.v
diff --git a/theories/DisjointSetUnionCode3.v b/theories/DisjointSetUnionCode3.v
@@ -0,0 +1,5 @@
+From CoqCP Require Import DisjointSetUnionCode Options.
+From stdpp Require Import numbers list.
+
+Lemma maxScoreIsAttainable : interact state (map (fun x => (0%Z, Z.of_nat x)) (seq 1 99)) = 5049%Z.
+Proof. reflexivity. Qed.