# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594684824 -32400
# Node ID adc3c3a3730842f46358731fa154cea956ba499a
# Parent  08d94fec239c42ae4916d86a3388606b72285717
...

diff -r 08d94fec239c -r adc3c3a37308 Ordinals.agda
--- a/Ordinals.agda	Tue Jul 14 07:59:17 2020 +0900
+++ b/Ordinals.agda	Tue Jul 14 09:00:24 2020 +0900
@@ -32,7 +32,7 @@
    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)) 
+     ¬nx<nx :  {x y : ord} → y o< x → x o< osuc (next y) →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
@@ -230,25 +230,28 @@
         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 (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
+        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (ordtrans (subst (λ k → k o< next x) b y<nx) <-osuc )
            (λ 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 )
+        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans (ordtrans c y<nx ) <-osuc )
            (λ 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 
 
+        next-is-limit : {x : Ordinal} →  ¬ ((y : Ordinal) → ¬ (next x ≡ osuc y))
+        next-is-limit {x} = ¬nx<nx {next x} {x} x<nx <-osuc 
+
         nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
         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 (¬nx<nx (osuc<nx  x<nx ) a
+        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) (ordtrans a <-osuc)
            (λ 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 (¬nx<nx (ordtrans <-osuc x<nx) c
+        nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) (ordtrans c <-osuc)
            (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
 
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
diff -r 08d94fec239c -r adc3c3a37308 ordinal.agda
--- a/ordinal.agda	Tue Jul 14 07:59:17 2020 +0900
+++ b/ordinal.agda	Tue Jul 14 09:00:24 2020 +0900
@@ -220,18 +220,23 @@
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
      ; TransFinite1 = TransFinite2
-     ; not-limit = not-limit
-     ; next-limit = next-limit
+     ; not-limit-p = not-limit
+   } ;
+   isNext = record {
+        x<nx = x<nx 
+      ; osuc<nx = λ {x} {y} → osuc<nx {x} {y}
+      ; ¬nx<nx = ¬nx<nx 
    }
   } where
      next : Ordinal {suc n} → Ordinal {suc n}
      next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
-     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) ∧
-        ( (x : Ordinal) → y o< x → x o< next y →  ¬ ((z : Ordinal) → ¬ (x ≡ osuc z)  ))
-     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = record { proj1 = lemma ; proj2 = lemma2 } } where
-         lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
-         lemma x (case1 lt) = case1 lt
-         lemma2 : (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ x ≡ osuc z)
+     x<nx :    { y : Ordinal } → (y o< next y )
+     x<nx = case1 a<sa
+     osuc<nx : { x y : Ordinal } → x o< next y → osuc x o< next y 
+     osuc<nx (case1 lt) = case1 lt 
+     ¬nx<nx :  {x y : Ordinal} → y o< x → x o< osuc (next y) →  ¬ ((z : Ordinal) → ¬ (x ≡ osuc z)) 
+     ¬nx<nx {x} {y} = lemma2 x where
+         lemma2 : (x : Ordinal) → y o< x → x o< osuc (next y) → ¬ ((z : Ordinal) → ¬ x ≡ osuc z)
          lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not
          lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl
          lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
@@ -239,6 +244,9 @@
          lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
              lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
              lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
+         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 lt) (case2 lt2) not = {!!}
+         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) os)) lt (case2 lt2) not = {!!}
+
      not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
      not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
      not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )