# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1679267710 -32400
# Node ID 440ebaf9f70759fa69874a6d3036ee4bee1d58bf
# Parent  d04fb4b2c72b8ff40f6a8b46ba4fa310b887e54f
generic filter done

diff -r d04fb4b2c72b -r 440ebaf9f707 src/generic-filter.agda
--- a/src/generic-filter.agda	Sun Mar 19 18:30:40 2023 +0900
+++ b/src/generic-filter.agda	Mon Mar 20 08:15:10 2023 +0900
@@ -352,21 +352,34 @@
 --
 
 val< : {x y p : Ordinal} → odef (* x) ( & < * y , * p >  ) → y o< x
-val< = ?
+val< {x} {y} {p} xyp = osucprev ( begin
+    osuc y ≤⟨ osucc (odef< (subst (λ k → odef (* y , * y)  k) &iso (v00 _  _ ) )) ⟩
+    & (* y , * y) <⟨ c<→o< (v01 _ _)  ⟩
+    & < * y , * p > <⟨ odef< xyp ⟩
+    & (* x) ≡⟨ &iso ⟩
+    x ∎ ) where 
+       v00 : (x y : HOD) → odef (x , y) (& x)
+       v00 _ _ = case1 refl
+       v01 : (x y : HOD) → < x , y > ∋ (x , x) 
+       v01 _ _ = case1 refl
+       open o≤-Reasoning O
 
 record valS (G : HOD) (x z : Ordinal) (val : (y : Ordinal) → y o< x → HOD): Set n where
    field
      y p : Ordinal
      G∋p : odef G p
      is-val : odef (* x) ( & < * y , * p >  )
-     x=valy : z ≡ & (val y (val< is-val))
+     z=valy : z ≡ & (val y (val< is-val))
+     z<x : z o< x
 
 val : (x : HOD) {P L M : HOD } {LP : L ⊆ Power P}
     →  (G : GenericFilter {L} {P} LP M )
     →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
-  ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z  valy  } ; odmax = {!!} ; <odmax = {!!} }
+  ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z  valy  } ; odmax = x ; <odmax = v02 } where
+      v02 : {z : Ordinal} → valS (⊆-Ideal.ideal (genf G)) x z valy → z o< x
+      v02 {z} lt = valS.z<x lt