# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1645535324 -32400
# Node ID 87b5303ceeb50ddc05e82a5bdb8fd469e4ecfc99
# Parent  b18ca68d115a87f93b02acd4f689e837ad8ecaf6
...

diff -r b18ca68d115a -r 87b5303ceeb5 src/generic-filter.agda
--- a/src/generic-filter.agda	Sun Feb 20 22:39:17 2022 +0900
+++ b/src/generic-filter.agda	Tue Feb 22 22:08:44 2022 +0900
@@ -54,7 +54,7 @@
 import OPair
 open OPair O
 
-record CountableModel : Set (suc (suc n)) where
+record CountableModel (P : HOD) : Set (suc (suc n)) where
    field
        ctl-M : Ordinal
        ctl→ : Nat → Ordinal
@@ -62,6 +62,9 @@
        is-Model : (x : Nat) → ctl→ x o< ctl-M
        ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M)  → ctl→ (ctl← x lt ) ≡ x 
        ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (is-Model x)  ≡ x
+       ctl-P⊆M : Power P ⊆ * ctl-M
+
+-- we expect ¬ G ∈ * ctl-M, so  ¬ P ∈ * ctl-M
 
 open CountableModel 
 
@@ -69,13 +72,13 @@
 --   a(n) ∈ M
 --   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
 --
-PGHOD :  (i : Nat) → (C : CountableModel) → (P : HOD) → (p : Ordinal) → HOD
-PGHOD i C P p = record { od = record { def = λ x  →
+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) }  
 
 ---
---   p(n+1) = if (f n) then qn otherwise p(n)
+--   p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
 --
 next-p :  (p : Ordinal) → (f : HOD → HOD) → Ordinal
 next-p p f with is-o∅  ( & (f (* p)))  
@@ -85,17 +88,17 @@
 ---
 --  search on p(n)
 --
-find-p :  (C : CountableModel) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
-find-p C P Zero x = x
-find-p C P (Suc i) x = find-p C P i ( next-p x (λ p → PGHOD i C P (& p) ))
+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) }
 --
-record PDN  (C : CountableModel) (P : HOD ) (x : Ordinal) : Set n where
+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 C P gr o∅)) y
+       pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p P C gr (& p))) y
        x∈PP  : odef (Power P) x
 
 open PDN
@@ -103,8 +106,8 @@
 ---
 -- G as a HOD
 --
-PDHOD :  (C : CountableModel) → (P : HOD ) → HOD
-PDHOD C P = record { od = record { def = λ x →  PDN C P x }
+PDHOD :  (P p : HOD ) (C : CountableModel P ) → HOD
+PDHOD P p C  = record { od = record { def = λ x →  PDN P p C x }
     ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } 
 
 open PDN
@@ -125,53 +128,47 @@
 
 open _⊆_
 
-P-GenericFilter : (C : CountableModel) → (P : HOD ) → GenericFilter P
-P-GenericFilter C P = record {
-      genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
+P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P
+P-GenericFilter P p0 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 C P x ⊆ Power P
+        PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i P C x ⊆ 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 C P i x)) y → odef P y 
+        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 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 C P (& (* x))))
+        find-p-⊆P (Suc i) x y Px Py with is-o∅  ( & (PGHOD i P C (& (* x))))
         ... | 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 C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
-            fmin∈PGHOD : PGHOD i C P (& (* x)) ∋ fmin
-            fmin∈PGHOD = ODC.x∋minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
+            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))
             pg-01 : Power P ∋ fmin 
-            pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i C P k ∋ fmin ) &iso  fmin∈PGHOD )
-        f⊆PL :  PDHOD C P ⊆ Power P
+            pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i P C 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) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
-        f1 : {p q : HOD} → q ⊆ P → PDHOD C P ∋ p → p ⊆ q → PDHOD C P ∋ q
-        f1 {p} {q}  q⊆P PD∋p p⊆q = f01 (& p) (& q) (⊆→o≤ f02) PD∋p (⊆→o≤ f03) where
+             find-p-⊆P (gr lt) {!!} (& y) {!!} (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
+        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
+           --  ¬ p ⊆ a n ⊆ p m
+           --  a(n) ∈ M, ¬ (∃ q ∈ a(n) ∧ p(n) ⊆ q ) ∨ (∃ q ∈ a(n) ∧ 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) )
-           f04 : (ip : Ordinal) → PDN C P ip → (x : Ordinal) → ((y : Ordinal) → y o< x → ip o< osuc y → PDN C P y) → ip o< osuc x → PDN C P x
-           f04 ip PD x prev lt with trio< ip (osuc x)
-           ... | tri≈ ¬a b ¬c = {!!}
-           ... | tri> ¬a ¬b c = ⊥-elim ( o<> c lt )
-           ... | tri< a ¬b ¬c with osuc-≡< a
-           ... | case1 ip=x = {!!}
-           ... | case2 ip<x = record { gr = ctl← C (find-p C P (PDN.gr PD) ( next-p x (λ p → PGHOD (PDN.gr PD) C P (& p)))) f05
-               ;  pn<gr = f07 ; x∈PP = f06 } where
-               next1 : Ordinal
-               next1 = find-p C P (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) C P (& p₁))) 
-               f05 : next1 o< ctl-M C
-               f05 = {!!}
-               f06 : odef (Power P) x
-               f06 = {!!}
-               f07 :  (y : Ordinal) → odef (* x) y → odef (* (find-p C P (ctl← C next1 f05) o∅)) y
-               f07 = {!!}
-           f01 : (ip iq : Ordinal) → iq o< osuc (& P) → PDN C P ip → ip o< osuc iq → PDN C P iq
-           f01 ip iq q<P PD = TransFinite0 {λ x → ip o< osuc x → PDN C P x } (f04 ip PD ) iq
-        f2 : {p q : HOD} → PDHOD C P ∋ p → PDHOD C P ∋ q → PDHOD C P ∋ (p ∩ q)
+           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 = {!!}
 
 
@@ -187,8 +184,9 @@
           → ( p ⊆ q P∋p)   ∧ ( p ⊆ r P∋p)  
           → ∀ ( s : HOD ) →  Power P ∋ s → ¬ (( q P∋p  ⊆ s  ) ∧ ( r P∋p  ⊆ s ))
 
-lemma725 : (C : CountableModel) (P : HOD ) 
-    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter C P )))
+lemma725 : (P p : HOD ) (C : CountableModel P) 
+    →  * (ctl-M C) ∋ Power P
+    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p C )))
 lemma725 = {!!}
 
 open import PFOD O
@@ -201,13 +199,28 @@
 lemma725-1 :   Incompatible HODω2
 lemma725-1 = {!!}
 
-lemma726 :  (C : CountableModel) (P : HOD ) 
-    →  Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2
+lemma726 :  (C : CountableModel HODω2) 
+    →  Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p C )))) =h= ω→2
 lemma726 = {!!}
 
 --
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
+
+
+record valR (x y P : HOD) (G : GenericFilter P) : Set (suc n) where
+   field
+     p : HOD
+     p∈G : filter (genf G) ∋ p 
+     is-val : x ∋ < y , p > 
+
+val : (x : HOD) (P : HOD ) 
+    →  (G : GenericFilter P)
+    →  HOD
+val x P G = record { od = record { odef = ε-induction { λ y → (z : Ordinal) → odef y (& z) → {!!}  } (λ {z} Prev → {!!} ) }
+    ; odmax = {!!} ; <odmax = {!!} }
+
+--
 --   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
 --