# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559440432 -32400
# Node ID 714470702a8b88d9c377e6510a766009713733f9
# Parent  819da8c08f05a34fbcfad7c6cbcc0c45d3de4878
Union done

diff -r 819da8c08f05 -r 714470702a8b ordinal.agda
--- a/ordinal.agda	Sat Jun 01 19:19:40 2019 +0900
+++ b/ordinal.agda	Sun Jun 02 10:53:52 2019 +0900
@@ -5,7 +5,7 @@
 open import zf
 
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-
+open import Data.Empty
 open import  Relation.Binary.PropositionalEquality
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
@@ -38,11 +38,34 @@
 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 
+s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
+s<refl {n} {lv} {Φ lv}  = Φ<
+s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
+s<refl {n} {Suc lv} {ℵ lv} = ℵs<
+
+trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
+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)
+
+d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
+d<→lv Φ< = refl
+d<→lv (s< lt) = refl
+d<→lv ℵΦ< = refl
+d<→lv (ℵ< _) = refl
+d<→lv ℵs< = refl
+d<→lv (ℵss< _) = refl
+
 o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
 o<-subst df refl refl = df
 
 open import Data.Nat.Properties 
-open import Data.Empty
 open import Data.Unit using ( ⊤ )
 open import Relation.Nullary
 
@@ -52,11 +75,6 @@
 o∅ : {n : Level} → Ordinal {n}
 o∅  = record { lv = Zero ; ord = Φ Zero }
 
-s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
-s<refl {n} {lv} {Φ lv}  = Φ<
-s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
-s<refl {n} {Suc lv} {ℵ lv} = ℵs<
-
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
 ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
@@ -72,17 +90,6 @@
 ≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
 
-trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
-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<
 
@@ -116,34 +123,16 @@
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
 
-d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
-d<→lv Φ< = refl
-d<→lv (s< lt) = refl
-d<→lv ℵΦ< = refl
-d<→lv (ℵ< _) = refl
-d<→lv ℵs< = refl
-d<→lv (ℵss< _) = refl
-
 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
-osuc record { lv = 0 ; ord = (Φ lv) } = record { lv = 0 ; ord = OSuc 0 (Φ lv) }
-osuc record { lv = Suc lx ; ord = (Φ (Suc lv)) } = record { lv = Suc lx ; ord = ℵ lv }
-osuc record { lv = 0 ; ord = (OSuc 0 ox ) } =  record { lv = 0 ; ord = OSuc 0 (OSuc 0 ox) }
-osuc record { lv = Suc lx ; ord = (OSuc (Suc lx) ox ) } =  record { lv = Suc lx ; ord = OSuc (Suc lx) (OSuc (Suc lx) ox) }
-osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) }
+osuc record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox }
 
 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
-<-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ<
-<-osuc {n} { record { lv = (Suc lv) ; ord = Φ  (Suc lv) } } = case2 ℵΦ<
-<-osuc {n} {record { lv = Zero ; ord = OSuc .0 ox }} = case2 ( s< s<refl )
-<-osuc {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ox }} = case2 ( s< s<refl )
-<-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } =  case2 ℵs< 
+<-osuc {n} {record { lv = lx ; ord = Φ .lx }} =  case2 Φ<
+<-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl )
+<-osuc {n} {record { lv = (Suc lx) ; ord = ℵ lx }} = case2 ℵs<
 
 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
-osuc-lveq {n} {record { lv = 0 ; ord = Φ 0 }} = refl
-osuc-lveq {n} {record { lv = Suc lv ; ord = Φ (Suc lv) }} = refl
-osuc-lveq {n} {record { lv = Zero ; ord = OSuc .0 ord₁ }} = refl
-osuc-lveq {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ord₁ }} = refl
-osuc-lveq {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} = refl
+osuc-lveq {n} = refl
 
 nat-<> : { x y : Nat } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
@@ -151,33 +140,8 @@
 nat-<≡ : { x : Nat } → x < x → ⊥
 nat-<≡  (s≤s lt) = nat-<≡ lt
 
-osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
-osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n))
-osuc-< {n} {record { lv = .0 ; ord = OSuc .0 ord₁ }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n))
-osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2
-osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2
-osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2
-osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) with d<→lv x₂ | osuc-lveq {n} {x}
-... | refl | eq = {!!}
-osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) with d<→lv x₁ | osuc-lveq {n} {x}
-... | refl | eq = {!!}
-osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = Zero ; ord = Φ .0 }} (case2 Φ<) (case2 ())
-osuc-< {n} {record { lv = Suc lv₁ ; ord = Φ .(Suc lv₁) }} {record { lv = Zero ; ord = Φ .0 }} (case2 ()) (case2 x₂)
-osuc-< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = Suc lv₂ ; ord = Φ .(Suc lv₂) }} (case2 x₁) (case2 ())
-osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = Zero ; ord = OSuc .0 ord₁ }} (case2 (s< ())) (case2 Φ<)
-osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .1 ; ord = ℵ Zero }} (case2 ℵs<) (case2 ())
-osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .1 ; ord = ℵ Zero }} (case2 (ℵss< x₁)) (case2 ())
-osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .(Suc (Suc lv₂)) ; ord = ℵ Suc lv₂ }} (case2 ()) (case2 x₂)
-osuc-< {n} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ Suc lv₁ }} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ .(Suc lv₁) }} (case2 ℵs<) (case2 ())
-osuc-< {n} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ Suc lv₁ }} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ .(Suc lv₁) }} (case2 (ℵss< x₁)) (case2 ())
-osuc-< {n} {record { lv = Suc lv₁ ; ord = .(Φ (Suc lv₁)) }} {record { lv = .(Suc lv₁) ; ord = (OSuc (Suc lv₁) y) }} (case2 (ℵ< x)) (case2 Φ<) = {!!}
-osuc-< {n} {record { lv = Zero ; ord = (OSuc 0 ox) }} {record { lv = .0 ; ord = (OSuc 0 oy) }} (case2 (s< c1)) (case2 (s< c2)) = 
-    osuc-< {n} {record { lv = Zero ; ord = ox }} {record { lv = 0 ; ord = oy }} (case2  {!!}) (case2  c2) 
-osuc-< {n} {record { lv = Suc lv₁ ; ord = .(OSuc (Suc lv₁) _) }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) _) }} (case2 (s< c1)) (case2 (s< c2)) = {!!}
-osuc-< {n} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< c1)) (case2 (ℵ< x)) = {!!}
-osuc-< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) (ℵ _)) }} (case2 (s< c1)) (case2 ℵs<) = {!!}
-osuc-< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) }} (case2 (s< c1)) (case2 (ℵss< c2)) = {!!}
-
+¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
 
 xsyℵ :  {n : Level} {lx : Nat} {x y : OrdinalD {n}  lx }   → x d< y → ¬ℵ y → ¬ℵ x
 xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ
@@ -208,6 +172,42 @@
 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 )
 
+osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
+osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt)
+osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case1 refl
+osuc-≡< {n} {record { lv = lv₁ ; ord = OSuc .lv₁ ord₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case2 (case2 Φ<)
+osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) }} (case2 Φ<) = case2 (case2 ℵΦ<)
+osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< ()))
+osuc-≡< {n} {record { lv = la ; ord = OSuc la oa }} {record { lv = la ; ord = (OSuc la ox) }} (case2 (s< lt)) with
+      osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt )
+... | case1 refl = case1 refl
+... | case2 (case2 x) = case2 (case2( s< x) )
+... | case2 (case1 x) = ⊥-elim (¬a≤a  x) where
+osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) (Φ (Suc lv₁))) }} (case2 (s< ℵΦ<)) = case2 (case2 (ℵ< ¬ℵΦ ))
+osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) (OSuc (Suc lx) ox)) }} (case2 (s< (ℵ< x))) with
+   osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) ox) }} (case2 (lemma (ℵ< x)) ) where
+      lemma : OSuc (Suc lx) ox d< (ℵ lx) → OSuc (Suc lx) ox d< ord (osuc (record { lv = Suc lx ; ord = ℵ lx }))
+      lemma lt = orddtrans lt s<refl
+... | case1 ()
+... | case2 ttt = case2 ( case2 (ℵ< (¬ℵs x) ))
+osuc-≡< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 ℵs<) = case1 refl
+osuc-≡< {n} {record { lv = .(Suc _) ; ord = Φ .(Suc _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt)
+osuc-≡< {n} {record { lv = .(Suc _) ; ord = OSuc .(Suc _) ord₁ }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt)
+osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(ℵ lv₁) }} (case2 (ℵss< lt)) = case1 refl
+
+osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
+osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox
+osuc-< {n} {x} {x} y<ox (case1 x₁) | case1 refl = ⊥-elim (¬a≤a x₁)
+osuc-< {n} {x} {x} (case1 x₂) (case2 x₁) | case1 refl = ⊥-elim (¬a≤a x₂)
+osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d<  x₁
+osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₁ x₂
+osuc-< {n} {x} {y} y<ox (case2 x₂) | case2 (case1 x₁) with d<→lv x₂
+... | refl = ⊥-elim (¬a≤a x₁)
+osuc-< {n} {x} {y} y<ox (case1 x₁) | case2 (case2 y<x) with d<→lv y<x
+... | refl = ⊥-elim (¬a≤a x₁)
+osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 (case2 y<x) with d<→lv y<x | d<→lv x<y
+... | refl | refl = trio<> y<x x<y
+
 max : (x y : Nat) → Nat
 max Zero Zero = Zero
 max Zero (Suc x) = (Suc x)