From 6865a76609fda63e65a5c3d6ab0a928eb5a62762 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 5 Nov 2024 08:38:30 -0500
Subject: [PATCH] checkpoint

---
 .../Queries/UnboundedMax/Privacy.lean         | 22 +++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean b/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean
index 11050fa6..43e1ee16 100644
--- a/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean
+++ b/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean
@@ -140,17 +140,17 @@ lemma sv8_G_comm : sv8_G (A ++ B) vp v0 vf = sv8_G (B ++ A) vp v0 vf := by
     congr 1
     apply IH
 
--- IDK
-lemma sv8_G_cons : sv8_G (x :: L) vp v0 vf = 0 := by
-  revert vp v0
-  induction vf
-  · intros v0 vp
-    simp [sv8_G]
-    sorry
-  · intro vp v0
-    simp [sv8_G]
-    sorry
-    -- unfold sv8_G
+-- -- IDK
+-- lemma sv8_G_cons : sv8_G (x :: L) vp v0 vf = 0 := by
+--   revert vp v0
+--   induction vf
+--   · intros v0 vp
+--     simp [sv8_G]
+--     s orry
+--   · intro vp v0
+--     simp [sv8_G]
+--     s orry
+--     -- unfold sv8_G
 
 lemma exactDiffSum_nonpos : exactDiffSum point L ≤ 0 := by
   simp [exactDiffSum, exactClippedSum]