# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595063473 -32400
# Node ID 1a8ca713bc32b77e32a8836b977d111f541bbb58
# Parent  7f919d6b045b73bc9ef4013d80f45c05f53e020b
...

diff -r 7f919d6b045b -r 1a8ca713bc32 filter.agda
--- a/filter.agda	Sat Jul 18 12:29:38 2020 +0900
+++ b/filter.agda	Sat Jul 18 18:11:13 2020 +0900
@@ -159,26 +159,34 @@
    ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 
 
 
-data Hω2 : ( x : Ordinal  ) → Set n where
-  hφ :  Hω2 o∅
-  h0 : {x : Ordinal  } → Hω2 x  →
-    Hω2 (od→ord < nat→ω 0 , ord→od x >)
-  h1 : {x : Ordinal  } → Hω2 x  →
-    Hω2 (od→ord < nat→ω 1 , ord→od x >)
-  h2 : {x : Ordinal  } → Hω2 x  →
-    Hω2 (od→ord < nat→ω 2 , ord→od x >)
+data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
+  hφ :  Hω2 0 o∅
+  h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) ,  ord→od x )))
+  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) ,  ord→od x )))
+  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) x
+
+record  Hω2r (x : Ordinal) : Set n where
+  field
+    count : Nat
+    hω2 : Hω2 count x
+
+open Hω2r
 
 HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where
+HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
     ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
     ω<next = ω<next-o∅ ho<
-    lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n  → od→ord < ord→od n , ord→od y > o< next y
-    lemma0 {n} {y} hw2 inf = nexto=n {!!} 
-    odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅
-    odmax0 {o∅} hφ = x<nx
-    odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {0} )))
-    odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {1} )))
-    odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {2} )))
+    lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
+    lemma = {!!}
+    odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
+    odmax0 {y} r with hω2 r
+    ... | hφ = x<nx
+    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
+    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
+    ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
 
 HODω2-Filter : Filter HODω2
 HODω2-Filter = record {