# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558520651 -32400
# Node ID 88b77cecaeba89fa770c42ec3857f99929ed9a9e
# Parent  c9ad0d97ce4125a9d68809d453ea73e9081603a7
ordinal fixed

diff -r c9ad0d97ce41 -r 88b77cecaeba ordinal.agda
--- a/ordinal.agda	Wed May 22 11:52:49 2019 +0900
+++ b/ordinal.agda	Wed May 22 19:24:11 2019 +0900
@@ -28,6 +28,7 @@
    ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx) 
    ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x  →  OSuc  (Suc lx) x d< (ℵ lx) 
    ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx)
+   ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x 
 
 open Ordinal
 
@@ -58,6 +59,12 @@
 trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
 trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ())
 trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs<
+trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
+trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< ()
+trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ())
+trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y
+trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ)
+trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x)
 
 trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
 trio<≡ refl = ≡→¬d<
@@ -68,15 +75,25 @@
 triO : {n : Level} →  {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
 triO  {n} {lx} {ly} x y = <-cmp lx ly
 
+fin : {n : Level} →  {lx : Nat} → {y : OrdinalD {n} (Suc lx) } → y d< (ℵ lx) → ¬ℵ y
+fin {_} {_} {Φ (Suc _)} ℵΦ< = ¬ℵΦ
+fin {_} {_} {OSuc (Suc _) _} (ℵ< x) = ¬ℵs x
+
 triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
 triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
 triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  (ℵΦ<  {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) )
 triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ<  {_} {lv} {Φ (Suc lv)} )
-triOrdd  {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} {!!})  ) (λ ()) (ℵ< {_} {lv} {y} {!!})
+triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y
+triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) )
+triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri<  ℵs< (λ ()) ( λ lt → trio<> lt  ℵs< )
+triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt ( ℵ< (fin c))  ) (λ ()) ( ℵ< (fin c) )
 triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
-triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< (ℵ< {!!}) (λ ()) (λ lt → trio<> lt (ℵ< {!!}) )
+triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) with triOrdd x (ℵ lv)
+triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri< a ¬b ¬c = tri< (ℵ< (fin a ) ) (λ ()) (  λ lt → trio<> lt (ℵ< (fin a ))) 
+triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri≈ ¬a refl ¬c = tri> (λ lt → trio<> lt ℵs< ) (λ ()) ℵs< 
+triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri> ¬a ¬b c = tri> (λ lt → trio<> lt (ℵss< c  )) (λ ()) ( ℵss< c  )
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
@@ -88,20 +105,36 @@
 d<→lv ℵΦ< = refl
 d<→lv (ℵ< _) = refl
 d<→lv ℵs< = refl
+d<→lv (ℵss< _) = refl
+
+xsyℵ :  {n : Level} {lx : Nat} {x y : OrdinalD {n}  lx }   → x d< y → ¬ℵ y → ¬ℵ x
+xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ
+xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t)
+xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) ()
+xsyℵ {_} {_} {ℵ lv₁} {.(OSuc (Suc lv₁) (ℵ lv₁))} ℵs< (¬ℵs t) = t
+xsyℵ (ℵss< ()) (¬ℵs ¬ℵΦ)
+xsyℵ (ℵss< x<y) (¬ℵs t) = xsyℵ x<y t
 
 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
 orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< {_} {lx} {y}
 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
 orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ)
-orddtrans {_} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc lx) (OSuc (Suc lx) y)} {.(ℵ lx)} (s< x<y) (ℵ< (¬ℵs nℵ)) = ℵ< lemma where
-   lemma : ¬ℵ x
-   lemma = {!!}
-orddtrans ℵΦ< ℵs< = {!!}
-orddtrans (ℵ< ¬ℵΦ) ℵs< = {!!}
-orddtrans (ℵ< (¬ℵs nℵ)) ℵs< = {!!}
-orddtrans ℵs< (s< ℵs<) = {!!}
 orddtrans ℵs< (ℵ< ())
+orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t )
+orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ<
+orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s< ( ℵΦ< {_} {_} {ℵ k} )
+orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t )
+orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs<
+orddtrans ℵΦ< (ℵss< y<z) = Φ<
+orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans (ℵΦ< {_} {_} {k})  y<z)
+orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z) 
+orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z) 
+orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z )
+orddtrans (ℵss< ()) (ℵ< ¬ℵΦ)
+orddtrans (ℵss< ℵs<) (ℵ< (¬ℵs ()))
+orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x )
+orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z )
 
 max : (x y : Nat) → Nat
 max Zero Zero = Zero