diff ordinal.agda @ 330:0faa7120e4b5

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 15:49:00 +0900
parents 5544f4921a44
children feb0fcc430a9
line wrap: on
line diff
--- a/ordinal.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -219,6 +219,7 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
+     ; TransFinite1 = TransFinite2
      ; not-limit = not-limit
      ; next-limit = next-limit
    }
@@ -244,4 +245,15 @@
         caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
+