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

diff -r d1c9f5ae5d0a -r eb4049abad70 src/generic-filter.agda
--- a/src/generic-filter.agda	Tue Mar 01 14:31:31 2022 +0900
+++ b/src/generic-filter.agda	Sun Mar 13 08:05:15 2022 +0900
@@ -59,12 +59,17 @@
        ctl-M : Ordinal
        ctl→ : Nat → Ordinal
        ctl← : (x : Ordinal )→  x o< ctl-M → Nat
-       is-Model : (x : Nat) → ctl→ x o< ctl-M
+       ctl<M : (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-iso← : { x : Nat }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
        ctl-P∈M : Power P ∈ * ctl-M
+--
+-- almmost universe
+-- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
+-- 
 
--- we expect ¬ G ∈ * ctl-M, so  ¬ P ∈ * ctl-M
+
+-- we expect  P ∈ * ctl-M ∧ G  ⊆ Power P  , ¬ G ∈ * ctl-M, 
 
 open CountableModel 
 
@@ -79,8 +84,7 @@
 
 ---
 --   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
@@ -94,12 +98,12 @@
 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 → p(n) ⊆ q }
 --
 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 (* (find-p P C gr (& p))) y → odef (* x) y 
        x∈PP  : odef (Power P) x
 
 open PDN
@@ -127,35 +131,21 @@
 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
 
+open import Data.Nat.Properties
+open import nat
 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 ))
+p-monotonic1 :  (P p : HOD ) (C : CountableModel P ) → {n : Nat} → (* (find-p P C n (& p))) ⊆ (* (find-p P C (Suc n) (& p)))
+p-monotonic1 = {!!}
 
-record ⊆-reduce-∅ (next : HOD → HOD) : Set (suc n) where
-   field
-     p : HOD
-     is-∅ :  & (next p) ≡ o∅
+p-monotonic :  (P p : HOD ) (C : CountableModel P ) → {n m : Nat} → n ≤ m → (* (find-p P C n (& p))) ⊆ (* (find-p P C m (& p)))
+p-monotonic P p C {Zero} {Zero} n≤m = refl-⊆
+p-monotonic P p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic P p C {Zero} {m} z≤n ) (p-monotonic1 P p C {m} )  
+p-monotonic P p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
+... | tri< a ¬b ¬c = trans-⊆ (p-monotonic P p C {Suc n} {m}  {!!} ) (p-monotonic1 P p C {m} )  
+... | tri≈ ¬a refl ¬c = refl-⊆
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
-⊆-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 }
@@ -176,27 +166,14 @@
             pg-01 : Power P ∋ fmin 
             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) _ (& y) Pp0 (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
+        f⊆PL = record { incl = λ {x} lt →  x∈PP lt  }
         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) )
+        f1 {p} {q}  q⊆P PD∋p p⊆q =  record { gr = gr PD∋p ;  pn<gr = f04 ; x∈PP = power←  _ _ (incl q⊆P) } where
            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 = {!!}
+           f04 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
+           f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (incl p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y  lt1 )))
+               -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
         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 = {!!}
 
diff -r d1c9f5ae5d0a -r eb4049abad70 src/nat.agda
--- a/src/nat.agda	Tue Mar 01 14:31:31 2022 +0900
+++ b/src/nat.agda	Sun Mar 13 08:05:15 2022 +0900
@@ -10,6 +10,9 @@
 nat-<> : { x y : Nat } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
+nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+
 nat-<≡ : { x : Nat } → x < x → ⊥
 nat-<≡  (s≤s lt) = nat-<≡ lt