### changeset 341:27d2933c4bd7

...
author Shinji KONO Mon, 13 Jul 2020 13:29:38 +0900 639fbb6284d8 b1ccdbb14c92 OD.agda Ordinals.agda 2 files changed, 18 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jul 13 09:26:34 2020 +0900
+++ b/OD.agda	Mon Jul 13 13:29:38 2020 +0900
@@ -393,16 +393,22 @@
lemma6 = <odmax (ord→od y , (ord→od y , ord→od y)) (subst ( λ k → def (od (ord→od y , (ord→od y , ord→od y))) k ) diso (case1 refl))
lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
lemma8 = ho<
+            lemmab : {x  : HOD} → od→ord (x , x) o< next (od→ord x)
+            lemmab {x} = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1  where
+               lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
+               lemmab0 = {!!}
+               lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
+               lemmab1 = ho<
+            lemmac : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< od→ord (y , y)
+            lemmac = {!!}
+            lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
+            lemmaa x<y = ordtrans (lemmac x<y) lemmab
lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
lemma81 = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-            lemma7 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (odmax (ord→od y , (ord→od y , ord→od y)))
lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
lemma91 = c<→o< (case1 refl)
-            lemma92 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next y
-            lemma92 = {!!}
lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
-            lemma9 = next< {!!} lemma92
-            lemma7 = ho<
+            lemma9 = lemmaa {!!}
lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
lemma71 = next< lemma81 lemma9
lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
--- a/Ordinals.agda	Mon Jul 13 09:26:34 2020 +0900
+++ b/Ordinals.agda	Mon Jul 13 13:29:38 2020 +0900
@@ -231,6 +231,13 @@
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≡ : {x : Ordinal} → next x ≡ next (osuc x)
+        nexto≡ {x} with trio< (next x) (next (osuc x) )
+        nexto≡ {x} | tri< a ¬b ¬c = {!!}
+        nexto≡ {x} | tri≈ ¬a b ¬c = b
+        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) _ (ordtrans <-osuc (subst (λ k → k o< next (osuc x)) eq {!!} )))))
+
record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
field
os→ : (x : Ordinal) → x o< maxordinal → Ordinal