# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559384380 -32400
# Node ID 819da8c08f05a34fbcfad7c6cbcc0c45d3de4878
# Parent  dd430a95610fafc6174bc06851ea34a1eb119955
ordinal atomical successor?

diff -r dd430a95610f -r 819da8c08f05 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jun 01 18:17:24 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 19:19:40 2019 +0900
@@ -360,7 +360,8 @@
              lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl diso
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
-         union→ X y u xx | tri< a ¬b ¬c = {!!}
+         union→ X y u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
+         union→ X y u xx | tri< a ¬b ¬c | ()
          union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
              lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
              lemma refl lt = lt
diff -r dd430a95610f -r 819da8c08f05 ordinal.agda
--- a/ordinal.agda	Sat Jun 01 18:17:24 2019 +0900
+++ b/ordinal.agda	Sat Jun 01 19:19:40 2019 +0900
@@ -41,12 +41,6 @@
 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
 
-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 = lx ; ord = (OSuc lx ox ) } =  record { lv = lx ; ord = OSuc lx (OSuc lx ox) }
-osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) }
-
 open import Data.Nat.Properties 
 open import Data.Empty
 open import Data.Unit using ( ⊤ )
@@ -63,36 +57,6 @@
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
 s<refl {n} {Suc lv} {ℵ lv} = ℵs<
 
-<-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-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
-
-nat-<> : { x y : Nat } → x < y → y < x → ⊥
-nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
-
-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 = lx ; ord = xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) with osuc-lveq  {n} {record { lv = lx ; ord = xo }}
-osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
-osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
-osuc-< {n} {record { lv = Zero ; ord = OSuc .0 xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
-osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
-osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | refl = nat-<> lt1 lt2
-osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) = {!!}
-osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) = {!!}
-osuc-< {n} {x} {y} (case2 x₁) (case2 x₂) = {!!}
-
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
 ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
@@ -160,6 +124,61 @@
 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 : {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-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
+
+nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+
+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)) = {!!}
+
+
 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)