# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595765437 -32400
# Node ID 43b0a6ca76023bcb994eeac198653a4c6ddf3277
# Parent  55f44ec2a0c6c3198604993c03227408f679968d
...

diff -r 55f44ec2a0c6 -r 43b0a6ca7602 OD.agda
--- a/OD.agda	Sat Jul 25 17:36:27 2020 +0900
+++ b/OD.agda	Sun Jul 26 21:10:37 2020 +0900
@@ -238,6 +238,12 @@
    lemma {z} (case1 refl) = case1 refl
    lemma {z} (case2 refl) = case1 refl
 
+pair-<xy : {x y : HOD} → {n : Ordinal}  → od→ord x o< next n →  od→ord y o< next n  → od→ord (x , y) o< next n
+pair-<xy {x} {y} {o} x<nn y<nn with trio< (od→ord x) (od→ord y) | inspect (omax (od→ord x)) (od→ord y)
+... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< 
+... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< 
+... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< 
+
 --  another form of infinite
 -- pair-ord< :  {x : Ordinal } → Set n
 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
@@ -427,8 +433,8 @@
     lemma {o∅} iφ = x<nx
     lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
 
-ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
-ω<next-o∅ ho< {y} lt = <odmax infinite lt
+ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
+ω<next-o∅ {y} lt = <odmax infinite lt
 
 nat→ω : Nat → HOD
 nat→ω Zero = od∅
diff -r 55f44ec2a0c6 -r 43b0a6ca7602 Ordinals.agda
--- a/Ordinals.agda	Sat Jul 25 17:36:27 2020 +0900
+++ b/Ordinals.agda	Sun Jul 26 21:10:37 2020 +0900
@@ -227,6 +227,12 @@
           → ¬ p
         FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+        nexto∅ : {x : Ordinal} → o∅ o< next x
+        nexto∅ {x} with trio< o∅ x
+        nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
+        nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
+        nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+
         next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
         next< {x} {y} {z} x<nz y<nx with trio< y (next z)
         next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
@@ -256,6 +262,9 @@
             y<nx : y o< next x
             y<nx = osuc< (sym eq)
 
+        omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
+        omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal
diff -r 55f44ec2a0c6 -r 43b0a6ca7602 generic-filter.agda
--- a/generic-filter.agda	Sat Jul 25 17:36:27 2020 +0900
+++ b/generic-filter.agda	Sun Jul 26 21:10:37 2020 +0900
@@ -84,15 +84,27 @@
 
 HODω2 :  HOD
 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<
-    lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
-    lemma = {!!}
+    P  : (i j : Nat) (x : Ordinal ) → HOD
+    P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x
+    nat0 : (i : Nat) → od→ord (nat→ω i) o< next o∅ 
+    nat0 i = <odmax infinite (ω∋nat→ω {i})
+    lemma3 : (i j : Nat) → od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) o< next o∅ 
+    lemma3 i j = pair-<xy (pair-<xy (nat0 i) (nat0 i) ) (pair-<xy (nat0 i) (nat0 j) )
+    lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x
+    lemma1 i j x = osuc<nx ( next< lemma2 ho<  ) where
+       lemma2 :  odmax (((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x) o< next x
+       lemma2 with trio<  (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j))) (od→ord (ord→od x))
+           |   inspect (omax (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)))) (od→ord (ord→od x))
+       lemma2 | tri< a ¬b ¬c | _ = osuc<nx (subst (λ k → k o< next x ) (sym diso) x<nx )
+       lemma2 | tri≈ ¬a b ¬c | record { eq = eq1 } = subst₂ (λ j k → j o< next k ) (trans (omax≡  _ _ b ) eq1 ) diso (osuc<nx x<nx)
+       lemma2 | tri> ¬a ¬b c | record { eq = eq1 } =  osuc<nx ( next< nexto∅ (lemma3 i j))
+    lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x
+    lemma i j x = next< (lemma1 i j x ) ho<
     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})
+    ... | 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
 
 3→Hω2 : List (Maybe Two) → HOD