### changeset 321:a81824502ebd

...
author Shinji KONO Fri, 03 Jul 2020 22:22:59 +0900 21203fe0342f a9d380378efd OD.agda Ordinals.agda 2 files changed, 6 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
```--- 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```
```--- 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
```