# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594681157 -32400
# Node ID 08d94fec239c42ae4916d86a3388606b72285717
# Parent  cfecd05a4061efdae61b6342ac545afe9fee3f12
Limit ordinal and possible OD bound

diff -r cfecd05a4061 -r 08d94fec239c OD.agda
--- a/OD.agda	Mon Jul 13 22:40:37 2020 +0900
+++ b/OD.agda	Tue Jul 14 07:59:17 2020 +0900
@@ -390,7 +390,7 @@
         u : (y : Ordinal ) → HOD
         u y = Union (ord→od y , (ord→od y , ord→od y))
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-        lemma {o∅} iφ = proj1  next-limit
+        lemma {o∅} iφ = x<nx
         lemma (isuc {y} x) = lemma2 where
             lemma0 : y o< next o∅
             lemma0 = lemma x
diff -r cfecd05a4061 -r 08d94fec239c Ordinals.agda
--- a/Ordinals.agda	Mon Jul 13 22:40:37 2020 +0900
+++ b/Ordinals.agda	Tue Jul 14 07:59:17 2020 +0900
@@ -20,9 +20,7 @@
      ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
-     not-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
-     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y ) ∧
-        ( (x : ord) → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)  ))
+     not-limit-p :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -30,6 +28,11 @@
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
 
+record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
+   field
+     x<nx :    { y : ord } → (y o< next y )
+     osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 
+     ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
@@ -39,6 +42,7 @@
      _o<_ : ord → ord → Set n
      next :  ord → ord
      isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
+     isNext : IsNext ord o∅ osuc _o<_ next
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
@@ -62,7 +66,10 @@
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
         TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
-        next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)
+
+        x<nx = IsNext.x<nx (Ordinals.isNext O)
+        osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 
+        ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) 
 
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
         o<-dom  {x} _ = x
@@ -223,43 +230,26 @@
         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
-        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) (next z) x<nz (subst (λ k → k o< next x) b y<nx)
-           (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (proj1 (proj2 next-limit) w (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
-        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx )
-           (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
+        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
+           (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
+        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
+           (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
 
         osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
         osuc< {x} {y} refl = <-osuc 
 
         nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
-        nexto=n {x} {y} x<noy = next< (proj1 (proj2 next-limit) _ (proj1 next-limit)) x<noy
+        nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
 
         nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
         nexto≡ {x} with trio< (next x) (next (osuc x) ) 
         --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
-        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) _ (proj1 (proj2 next-limit) _ (proj1 next-limit) ) a
-           (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq)))))
+        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
+           (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
         nexto≡ {x} | tri≈ ¬a b ¬c = b
         --    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
-        nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim ((proj2 (proj2 next-limit)) _ (ordtrans <-osuc (proj1 next-limit)) c
-           (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq)))))
-
-        record prev-choiced  ( x : Ordinal ) : Set (suc n) where
-         field
-            prev : Ordinal
-            is-prev : osuc prev ≡ x 
-        not-limit-p :  ( x : Ordinal  ) → Dec ( ¬ ((y : Ordinal) → ¬ (x ≡ osuc y) ))
-        not-limit-p x = {!!} where
-            ψ : ( ox : Ordinal ) → Set (suc n)
-            ψ ox = (( y : Ordinal ) → y o< ox  → ( ¬ (osuc y ≡ x) )) ∨ prev-choiced x
-            ind : (ox : Ordinal) → ((y : Ordinal) → y o< ox → ψ y) → ψ ox 
-            ind ox prev with trio< (osuc ox) x
-            ind ox prev | tri≈ ¬a b ¬c = case2 (record { prev = ox ; is-prev = b })
-            ind ox prev | tri< a ¬b ¬c = case1 (λ y y<ox oy=x → o<> (subst (λ k → k o< osuc ox) oy=x (osucc y<ox )) a ) 
-            --     osuc y = x < osuc ox, y < ox
-            ind ox prev | tri> ¬a ¬b c = {!!}
-            find : (y : Ordinal) → ψ y
-            find ox = TransFinite1 {ψ} ind ox
+        nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
+           (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
 
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field