Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1257:004d8794697f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Mar 2023 00:30:43 +0900
parents 0b7e4eb68afc
children 04fc80af6f77
files src/generic-filter.agda
diffstat 1 files changed, 6 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- 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)