changeset 325:1a54dbe1ea4c

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Jul 2020 22:48:49 +0900
parents fbabb20f222e
children feeba7fd499a
files OD.agda ordinal.agda
diffstat 2 files changed, 9 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/OD.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -329,14 +329,17 @@
             lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt }
         lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
         lemma3 {x} = od⊆→o≤ lemma1
+        lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x))
+        lemma4 {x} = ordtrans (<odmax (x , x) {!!}) {!!}
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
         lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →
                 infinite-d x → x o< (next  o∅)
            ind o∅  prev iφ = proj1 next-limit
-           ind x prev (isuc lt) = lemma0 where
-              lemma0 : {x : Ordinal} → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
-              lemma0 {x} = {!!}
+           ind x prev (isuc lt) = lemma0 {_} {x} {!!} where
+              lemma0 : {x z : Ordinal} → x o< od→ord (Union (ord→od z , (ord→od z , ord→od z))) → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
+              lemma0 {x} with prev x {!!}
+              ... | t = {!!}
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y
--- a/ordinal.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/ordinal.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -211,7 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
-   ; next = ?
+   ; next = {!!}
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -219,8 +219,8 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
-     ; is-limit = ?
-     ; next-limit = ?
+     ; is-limit = {!!}
+     ; next-limit = {!!}
    }
   } where
      ord1 : Set (suc n)