# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1646902695 -32400
# Node ID 8c43e804581e4e03fa05e02fbd72755cbf6aae21
# Parent  3681cac8d6a89f428b622830982377c46229e04f
generic filter does not work

diff -r 3681cac8d6a8 -r 8c43e804581e src/generic-filter.agda
--- a/src/generic-filter.agda	Wed Mar 09 17:42:22 2022 +0900
+++ b/src/generic-filter.agda	Thu Mar 10 17:58:15 2022 +0900
@@ -68,9 +68,43 @@
 
 open CountableModel 
 
---
+b02 : {x : HOD} → o∅ o< & x → ¬ ( x =h= od∅ )
+b02 = ∅7
+
+b07 : {x : HOD} → ¬ ( x =h= od∅ ) → o∅ o< & x 
+b07 {x} not with trio< o∅ (& x)
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( not ( ≡o∅→=od∅ (sym b) ))
+... | tri> ¬a ¬b c = ⊥-elim (  ¬x<0 c )
+
+b08 : {a x : HOD} → ( a =h= od∅ ) → ¬ ( x ∈  a )
+b08 {a} {x} eq lt with trio< o∅ (& x)
+... | tri< a₁ ¬b ¬c = ⊥-elim ( o<¬≡ (sym (=od∅→≡o∅ {a} eq)) (ordtrans a₁ (c<→o< lt )) )
+... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym (=od∅→≡o∅ eq)) (subst (λ k → k o< & a) (sym b) (c<→o< lt ) ))
+... | tri> ¬a ¬b c = ⊥-elim (  ¬x<0 c )
+
+open _==_
+
+b01 : {an bn : HOD} → o∅ o< & bn  →  &( bn ∩ an ) ≡ o∅  → o∅ o< &( bn ＼ an )
+b01 {an} {bn} 0<b ba=0 = b07 (b03 (b02 0<b) (≡o∅→=od∅ ba=0)) where
+   -- b =< a, ba=b
+   b04 : ( ( bn ＼ an ) =h= od∅ ) → ( bn ∩ an ) =h= bn 
+   b04 b-a=0 = record { eq→  = b05 ; eq← = b06 } where
+      b05 : {x : Ordinal} → OD.def (od (bn ∩ an)) x → OD.def (od bn) x
+      b05 {x} p = proj1 p
+      b06 : {x : Ordinal} → OD.def (od bn) x → OD.def (od (bn ∩ an)) x
+      b06 {x} x∈b with ODC.∋-p O an (* x)
+      ... | yes y = ⟪ x∈b , subst (λ k → odef an k) &iso y ⟫ 
+      ... | no n = ⊥-elim ( b08 {bn ＼ an} b-a=0 ⟪ subst ( λ k → odef bn k ) (sym &iso) x∈b , (λ y →  n y) ⟫ )
+   b03 :  ¬ ( bn =h= od∅ ) →  ( bn ∩ an ) =h= od∅ → ¬ ( ( bn ＼ an ) =h= od∅ )
+   b03 b>0 ba=0 b-a=0 = ⊥-elim ( b>0 (==-trans (==-sym (b04 b-a=0 ))ba=0 ))
+
+b11 : {an bn x : HOD} → an ⊆ bn → ¬ ( x ∈ an ) → an ⊆ ( bn ＼ x )
+b11 = {!!}
+
 --
 --   a(n) = /\ { a | a ∈ m (n) ∧ m (n) ∈ Power P) }
+--
 A :  (i : Nat) (P : HOD) (C : CountableModel P) → HOD
 A i P C  = record { od = record { def = λ x  →
        odef (Power P) (ctl→ C i)  ∧  odef (* (ctl→ C i)) x }
@@ -78,7 +112,7 @@
 
 ---
 --   b(0) = p
---   b(n+1) = if (b(n) ∩ a(n)) != ∅ then b(n) ∩ a(n) otherwise b(n) - a ( a ∈ ( b(n) - a(n)) from choice )
+--   b(n+1) = if (b(n) ∩ a(n)) != ∅ then b(n) ∩ a(n) otherwise b(n) - a ( a ∈ a(n) s.t. ( b(n) - a !=  ∅) from choice )
 --
 
 record BR : Set (suc n) where
@@ -92,13 +126,16 @@
 ... | yes _ = B P C i x lt
 ... | no _  with is-o∅ ( & (BR.b (B P C i x lt) ∩ A i P C ) )
 ... | no ne =  record { b = BR.b (B P C i x lt ) ∩ A i P C  ; b>0 = ¬≡o∅< ne } 
-... | yes y = record { b = BR.b (B P C i x lt) ＼ (ODC.minimal O b03 (b02 (b01 (BR.b>0 (B P C i x lt)) y ))) ; b>0 = {!!} } where
+... | yes y = record { b = BR.b (B P C i x lt) ＼ (ODC.minimal O b03 (b02 (b01 (BR.b>0 (B P C i x lt)) y ))) ; b>0 = b12 } where
+    -- b01 : {an bn : HOD} → o∅ o< & bn  →  &( bn ∩ an ) ≡ o∅  → o∅ o< &( bn ＼ an )
     b03 : HOD 
     b03 = BR.b (B P C i x lt) ＼ A i P C
-    b02 : {x : HOD} → o∅ o< & x → ¬ ( x =h= od∅ )
-    b02 = ∅7
-    b01 : {an bn : HOD} → o∅ o< & bn  →  &( bn ∩ an ) ≡ o∅  → o∅ o< &( bn ＼ an )
-    b01 {an} {bn} 0<b ba=0 = {!!}
+    b09 : A i P C ⊆ BR.b (B P C i x lt)  
+    b09 = {!!}
+    b10 : A i P C ⊆ ( BR.b (B P C i x lt) ＼ (ODC.minimal O b03 (b02 (b01 (BR.b>0 (B P C i x lt)) y ))) )
+    b10 = {!!}
+    b12 : o∅ o< & ( BR.b (B P C i x lt) ＼ (ODC.minimal O b03 (b02 (b01 (BR.b>0 (B P C i x lt)) y ))) )
+    b12 = {!!}
        
 
 B⊆ : (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : HOD) →  (lt : o∅ o< & x) → BR.b (B P C (Suc i) x lt) ⊆  BR.b (B P C (Suc i) x lt)