# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593782579 -32400
# Node ID a81824502ebdacd3a3e647d50c0dbfa47c700f8c
# Parent  21203fe0342f45776b2c0410a0631c67a4c3bb00
...

diff -r 21203fe0342f -r a81824502ebd OD.agda
--- a/OD.agda	Fri Jul 03 21:58:01 2020 +0900
+++ b/OD.agda	Fri Jul 03 22:22:59 2020 +0900
@@ -311,8 +311,10 @@
     infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
         lemma {o∅} iφ = proj1 next-limit
-        lemma {n} (isuc i) = {!!} where
-            lemma1 = proj2 next-limit
+        lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i )
+           lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
+           lemma1 = ?
+
 
 
     _=h=_ : (x y : HOD) → Set n
diff -r 21203fe0342f -r a81824502ebd Ordinals.agda
--- a/Ordinals.agda	Fri Jul 03 21:58:01 2020 +0900
+++ b/Ordinals.agda	Fri Jul 03 22:22:59 2020 +0900
@@ -21,7 +21,7 @@
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      is-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
-     next-limit : { x : ord } → (x o< next x )∧ (¬ ((y : ord) → next x ≡ osuc y) )
+     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y )
      TransFinite : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -58,7 +58,7 @@
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
         next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)
-        
+
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
         o<-dom  {x} _ = x