# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1646116385 -32400
# Node ID 6b26db38367fabf585064b5f9ad4578503122609
# Parent  d1c9f5ae5d0a0ffa0fca2cf4442384a110df32f1
...

diff -r d1c9f5ae5d0a -r 6b26db38367f src/generic-filter.agda
--- a/src/generic-filter.agda	Tue Mar 01 14:31:31 2022 +0900
+++ b/src/generic-filter.agda	Tue Mar 01 15:33:05 2022 +0900
@@ -68,38 +68,40 @@
 
 open CountableModel 
 
-----
---   a(n) ∈ M
---   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
+--
 --
-PGHOD :  (i : Nat) (P : HOD) (C : CountableModel P) → (p : Ordinal) → HOD
-PGHOD i P C p = record { od = record { def = λ x  →
-       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
-   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
+--   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 }
+   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → {!!} }
 
 ---
---   p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
---       is not working well
---       skipped a(n) may cantains extra elements in possible r
-next-p :  (p : Ordinal) → (f : HOD → HOD) → Ordinal
-next-p p f with is-o∅  ( & (f (* p)))  
-next-p p f | yes y = p
-next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
+--   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 )
+--
+
+record BR : Set (suc n) where
+   field
+      b : HOD
+      b>0 : o∅ o< & b 
+
+B :  (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : HOD) →  o∅ o< & x   → BR
+B P C Zero x lt = record { b = x ; b>0 = lt }
+B P C (Suc i) x lt with is-o∅ ( & (BR.b (B P C i x lt) ∩ A i P C ) )
+... | no _ =  record { b = BR.b (B P C i x lt ) ∩ A i P C  ; b>0 = {!!} }
+... | yes y = record { b = BR.b (B P C i x lt) ＼ {!!} ; b>0 = {!!} }
+
+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)
+B⊆ = {!!}
 
 ---
---  search on p(n)
---
-find-p :  (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : Ordinal) → Ordinal
-find-p P C Zero x = x
-find-p P C (Suc i) x = find-p P C i ( next-p x (λ p → PGHOD i P C (& p) ))
-
----
--- G = { r ∈ Power P | ∃ n → r ⊆ p(n) }
+-- G = { r ∈ Power P | ∃ n → b(n) ⊆ r }
 --
 record PDN  (P p : HOD ) (C : CountableModel P)  (x : Ordinal) : Set n where
    field
        gr : Nat
-       pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p P C gr (& p))) y
+       pn<gr : (y : Ordinal) → odef (BR.b (B P C gr p {!!} )) y → odef (* x) y 
        x∈PP  : odef (Power P) x
 
 open PDN
@@ -129,79 +131,35 @@
 
 open _⊆_
 
-find-an :{P p : HOD} → (C : CountableModel P ) → odef (Power P) (& p) → Nat
-find-an = {!!}
-
-found-an :{P p : HOD} → (C : CountableModel P ) → (pw : odef (Power P) (& p)) → * (ctl→ C (find-an C pw)) =h= p
-found-an = {!!}
-
-record ⊆-reduce ( p :  HOD ) : Set (suc n) where
-   field
-     next : HOD
-     is-small :  next ⊆ p ∧ ( ¬ ( next =h= p ))
-
-record ⊆-reduce-∅ (next : HOD → HOD) : Set (suc n) where
-   field
-     p : HOD
-     is-∅ :  & (next p) ≡ o∅
-
-⊆-reduction : (next : (x : HOD) → ⊆-reduce x ) → (x : HOD) → ¬ ( x ∈ ( ⊆-reduce.next (next x )))
-⊆-reduction  next x = subst (λ k → ¬ (x ∈ ⊆-reduce.next (next k))) *iso (r02 x) where
-    r01 : (x₁ : Ordinal) → ((y : Ordinal) → y o< x₁ → ¬ odef (⊆-reduce.next (next (* y))) y) →
-            ¬ odef (⊆-reduce.next (next (* x₁))) x₁
-    r01 = {!!}
-    r02 : (x : HOD) → ¬ (x ∈ ⊆-reduce.next (next (* (& x))))
-    r02 x = TransFinite0 {λ x → ¬ ( odef ( ⊆-reduce.next (next (* x))) x) } r01 (& x) 
-
-next-x≡∅ : (next : HOD → HOD)  → ( (x : HOD) → ¬ ( x ∈ next x) ) →  ⊆-reduce-∅ next
-next-x≡∅ = {!!}
  
 P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel P) → GenericFilter P
 P-GenericFilter P p0 Pp0 C = record {
       genf = record { filter = PDHOD P p0 C ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
     ; generic = λ D → {!!}
    } where
-        PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i P C x ⊆ Power P
+        PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  {!!} ⊆ Power P
         PGHOD∈PL i x = record { incl = λ {x} p → proj1 p }
-        find-p-⊆P :  (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p P C i x)) y → odef P y 
+        find-p-⊆P :  (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef {!!} y → odef P y 
         find-p-⊆P Zero x y Px Py = subst (λ k → odef P k ) &iso
             ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
-        find-p-⊆P (Suc i) x y Px Py with is-o∅  ( & (PGHOD i P C (& (* x))))
+        find-p-⊆P (Suc i) x y Px Py with is-o∅  {!!}
         ... | yes y1 = find-p-⊆P i x y Px Py
         ... | no not = find-p-⊆P i (& fmin) y pg-01 Py where
             fmin : HOD
-            fmin = ODC.minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
-            fmin∈PGHOD : PGHOD i P C (& (* x)) ∋ fmin
-            fmin∈PGHOD = ODC.x∋minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
+            fmin = ODC.minimal O {!!} (λ eq → not (=od∅→≡o∅ eq))
+            fmin∈PGHOD : {!!} ∋ fmin
+            fmin∈PGHOD = ODC.x∋minimal O {!!} (λ eq → not (=od∅→≡o∅ eq))
             pg-01 : Power P ∋ fmin 
-            pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i P C k ∋ fmin ) &iso  fmin∈PGHOD )
+            pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → {!!} ∋ fmin ) &iso  fmin∈PGHOD )
         f⊆PL :  PDHOD P p0 C ⊆ Power P
         f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
-             find-p-⊆P (gr lt) _ (& y) Pp0 (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
+             find-p-⊆P (gr lt) _ (& y) Pp0 {!!}) }
         f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q
         f1 {p} {q}  q⊆P PD∋p p⊆q =  record { gr = {!!} ;  pn<gr = {!!} ; x∈PP = {!!} }  where
-           --  reduction : {ψ : (x : HOD) → x =h= od∅ → P x} → 
-           --  q ∈ a(∃ n) ⊆ P → ( p n ⊆ q →  PDHOD P p0 C ∋ q )
-           --                 ∨ (¬ (p n ⊆ q) → induction on (p n - q) 
-           -- PDNp :  {!!} -- PD⊆⊆N P C (& p)
-           -- PDNp = PD∋p
-           f02 : {x : Ordinal} → odef q x → odef P x
-           f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) )
-           f03 : {x : Ordinal} → odef p x → odef q x
-           f03 {x} lt = subst (λ k → def (od q) k) &iso (incl p⊆q (subst (λ k → def (od p) k) (sym &iso) lt) )
-           next1 : Ordinal
-           next1 = {!!} -- find-p P C (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) P C (& p₁))) 
-           -- f05 : next1 o< ctl-M C
-           -- f05 = {!!}
-           -- f06 : odef (Power P) (& q)
-           -- f06 = {!!}
-           -- f07 :  (y : Ordinal) → odef (* (& q)) y → odef (* {!!} ) y
-           -- f07 = {!!}
         f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
         f2 {p} {q} PD∋p PD∋q = {!!}
 
 
-
 open GenericFilter
 open Filter