# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647255234 -32400
# Node ID 31f0a5a745a54e83177fb2cf86c61fbb35c95af0
# Parent  b27d92694ed53bfd6ef44f06cb06650f3c8084ac
...

diff -r b27d92694ed5 -r 31f0a5a745a5 src/BAlgbra.agda
--- a/src/BAlgbra.agda	Mon Mar 14 17:51:16 2022 +0900
+++ b/src/BAlgbra.agda	Mon Mar 14 19:53:54 2022 +0900
@@ -50,6 +50,13 @@
 _＼_ : ( A B : HOD  ) → HOD
 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
 
+¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
+¬∅∋ {x} = ¬x<0
+
+[a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
+[a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
+     ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
+
 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
diff -r b27d92694ed5 -r 31f0a5a745a5 src/generic-filter.agda
--- a/src/generic-filter.agda	Mon Mar 14 17:51:16 2022 +0900
+++ b/src/generic-filter.agda	Mon Mar 14 19:53:54 2022 +0900
@@ -222,13 +222,19 @@
     p⊆P : p ⊆ P
     p⊆P =  ODC.power→⊆ O _ _ PP∋p
     df : {x : HOD} → x ⊆ P → HOD
-    df {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x
-    ... | case1 q = Incompatible.q (I p p⊆P) 
-    ... | case2 r = Incompatible.r (I p p⊆P) 
+    df {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x
+    ... | case1 q = Incompatible.q (I x PP∋x)
+    ... | case2 r = Incompatible.r (I x PP∋x)
+    df¬⊆ : {x : HOD} → (lt : x ⊆ P) → ¬ ( df lt  ⊆ x )
+    df¬⊆ {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x
+    ... | case1 q = {!!}
+    ... | case2 r = {!!}
     df-d : {x : HOD} → (lt : x ⊆ P) → D ∋ df lt
-    df-d = {!!}
+    df-d {x} lt = {!!}
     df-p : {x : HOD} → (lt : x ⊆ P) → x ⊆ df lt
-    df-p = {!!}
+    df-p {x} lt with Incompatible.incompatible (I x lt) x lt
+    ... | case1 q = Incompatible.p⊆q (I x lt) 
+    ... | case2 r = Incompatible.p⊆r (I x lt) 
     D-Dense : Dense P
     D-Dense = record {
            dense = D
@@ -238,7 +244,7 @@
        ;   dense-p = df-p
      }
     D∩G=∅ : ( D ∩ G ) =h= od∅ 
-    D∩G=∅ = {!!}
+    D∩G=∅ = ≡od∅→=od∅ ([a-b]∩b=0 {Power P} {G})
     D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ )
     D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq )