# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678980643 -32400
# Node ID 004d8794697f568f3601ac29c4f99c2f4ed6a187
# Parent  0b7e4eb68afcbe0a7c99a921a4f96b487a4fc76b
...

diff -r 0b7e4eb68afc -r 004d8794697f src/generic-filter.agda
--- a/src/generic-filter.agda	Thu Mar 16 19:01:47 2023 +0900
+++ b/src/generic-filter.agda	Fri Mar 17 00:30:43 2023 +0900
@@ -321,22 +321,24 @@
             q = NotCompatible.q (NC Lp)
             r : HOD
             r = NotCompatible.r (NC Lp)
+            Lr : L ∋ r
+            Lr = NotCompatible.Lr (NC Lp)
             Lq : L ∋ q
             Lq = NotCompatible.Lq (NC Lp)
             exp1 : Expansion L D Lp
             exp1  with ODC.p∨¬p O (rgf ∋ q)
-            ... | case2 ngq = record { expansion = q  ; dense∋exp = ? ; p⊆exp = ? }  
+            ... | case2 ngq = record { expansion = q  ; dense∋exp = ⟪ Lq , ngq ⟫ ; p⊆exp = NotCompatible.p⊆q (NC Lp)}  
             ... | case1 gq with ODC.p∨¬p O (rgf ∋ r)
-            ... | case2 ngr = record { expansion = q  ; dense∋exp = ? ; p⊆exp = ? }  
+            ... | case2 ngr = record { expansion = r  ; dense∋exp = ⟪ Lr , ngr ⟫ ; p⊆exp = NotCompatible.p⊆r (NC Lp)}  
             ... | case1 gr = ⊥-elim ( ll02 ⟪ ? , ? ⟫ ) where
                 ll02 : ¬ ( (q ⊆ p) ∧ (r ⊆ p) )
                 ll02 = NotCompatible.¬compat (NC Lp) p ? 
                 ll05 : ¬ ( (q ⊆ (q ∪ r) ∧ (r ⊆ (q ∪ r)) ))
                 ll05 = NotCompatible.¬compat (NC Lp )  (q ∪ r) ?
                 ll03 : rgf ∋ p → rgf ∋ q → rgf ∋ (p ∪ q)
-                ll03 rp rq = ? -- Ideal.ideal2 GF ⟪ rp , rq ⟫ 
+                ll03 rp rq = Ideal.ideal2 GF rp rq ? -- ⟪ rp , rq ⟫ 
                 ll04 : rgf ∋ p → q ⊆ p → rgf ∋ q
-                ll04 rp q⊆p = ? -- Ideal.ideal1 GF rp q⊆p ?
+                ll04 rp q⊆p = Ideal.ideal1 GF Lq rp q⊆p 
     ¬rgf∩D=0 : ¬ ( (D ∩ rgf ) =h= od∅ )
     ¬rgf∩D=0 eq =  generic PG DD M∋D (==→o≡ eq)