diff ordinal.agda @ 329:5544f4921a44

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 12:32:09 +0900
parents 1a54dbe1ea4c
children 0faa7120e4b5
line wrap: on
line diff
--- a/ordinal.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -211,7 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
-   ; next = {!!}
+   ; next = next
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -219,10 +219,19 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
-     ; is-limit = {!!}
-     ; next-limit = {!!}
+     ; not-limit = not-limit
+     ; next-limit = next-limit
    }
   } 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)
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+         lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
+         lemma x (case1 lt) = case1 lt
+     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 )
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
      TransFinite1 : { ψ : ord1  → Set (suc n) }