# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593870529 -32400
# Node ID 1a54dbe1ea4c261c02dca9fb0cb6303158aa450d
# Parent  fbabb20f222ef021d811d5f5499ce44a93fe28b1
...

diff -r fbabb20f222e -r 1a54dbe1ea4c OD.agda
--- a/OD.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/OD.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -329,14 +329,17 @@
             lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt }
         lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
         lemma3 {x} = od⊆→o≤ lemma1
+        lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x))
+        lemma4 {x} = ordtrans (<odmax (x , x) {!!}) {!!}
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
         lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →
                 infinite-d x → x o< (next  o∅)
            ind o∅  prev iφ = proj1 next-limit
-           ind x prev (isuc lt) = lemma0 where
-              lemma0 : {x : Ordinal} → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
-              lemma0 {x} = {!!}
+           ind x prev (isuc lt) = lemma0 {_} {x} {!!} where
+              lemma0 : {x z : Ordinal} → x o< od→ord (Union (ord→od z , (ord→od z , ord→od z))) → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
+              lemma0 {x} with prev x {!!}
+              ... | t = {!!}
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y
diff -r fbabb20f222e -r 1a54dbe1ea4c ordinal.agda
--- a/ordinal.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/ordinal.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -211,7 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
-   ; next = ?
+   ; next = {!!}
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -219,8 +219,8 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
-     ; is-limit = ?
-     ; next-limit = ?
+     ; is-limit = {!!}
+     ; next-limit = {!!}
    }
   } where
      ord1 : Set (suc n)