Change Admitted to Qed

huynhtrankhanh · Nov 12, 2024 · cf6b85e · cf6b85e
1 parent d1fca00
commit cf6b85e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/DisjointSetUnionCode2.v b/theories/DisjointSetUnionCode2.v
@@ -1275,7 +1275,7 @@ Proof.
            varsfuncdef_0__main) withLocalVariablesReturnValue () ()) = _) unfoldInvoke_S_Done.
   apply (ltac:(intros T U mm ma mb mc; subst ma; reflexivity) : forall (T U : Type) (g : T) (a b : U), a = b -> Some (g, a) = Some (g, b)).
   apply functional_extensionality_dep. intro x. unfold update. unfold stateAfterInteractions. repeat case_decide; easy.
-Admitted.
+Qed.
 
 Lemma firstInteraction (a b : Z) (hLt1 : Z.lt a 100) (hLt2 : Z.lt b 100) : invokeContract (repeat 1%Z 20) (repeat 0%Z 20) 0%Z state state [a; b] 1 = Some ([a; b], stateAfterInteractions (fun x => match x with | arraydef_0__result => [0%Z] | arraydef_0__hasBeenInitialized => [1%Z] | arraydef_0__dsu => convertToArray (unite (repeat (Ancestor Unit) 100) (Z.to_nat a) (Z.to_nat b)) end) (dsuScore (unite (repeat (Ancestor Unit) 100) (Z.to_nat a) (Z.to_nat b)))).
 Proof.