# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558402354 -32400
# Node ID 97ff3f7933febb136e39cf02550a0ea70ed0ef64
# Parent  3b0fdb95618e759e170023736d70e5e4877d63d7
fix ordinal

diff -r 3b0fdb95618e -r 97ff3f7933fe ordinal.agda
--- a/ordinal.agda	Tue May 21 00:30:01 2019 +0900
+++ b/ordinal.agda	Tue May 21 10:32:34 2019 +0900
@@ -6,35 +6,36 @@
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 
 open import  Relation.Binary.PropositionalEquality
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Data.Unit using ( ⊤ )
+open import Relation.Nullary
+
+open import Relation.Binary
+open import Relation.Binary.Core
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
    OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
    ℵ_ :  (lv : Nat) → OrdinalD (Suc lv)
 
-record Ordinal {n : Level} : Set n where
-   field
-     lv : Nat
-     ord : OrdinalD {n} lv
-
 data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
    Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
    s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
    ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx) 
    ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  OSuc  (Suc lx) x d< (ℵ lx) 
 
+record Ordinal {n : Level} : Set n where
+   field
+     lv : Nat
+     ord : OrdinalD {n} lv
+     order : ¬ ( ord  ≡ Φ lv ) → { prev : OrdinalD {n} lv } → prev d< ord
+
 open Ordinal
 
 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 
-open import Data.Nat.Properties 
-open import Data.Empty
-open import Data.Unit using ( ⊤ )
-open import Relation.Nullary
-
-open import Relation.Binary
-open import Relation.Binary.Core
 
 ¬ℵ : {n : Level} {lx : Nat } ( x : OrdinalD {n} lx ) → Set 
 ¬ℵ (Φ lv₁) = ⊤
@@ -47,7 +48,7 @@
 s<refl {n} {.(Suc lv₁)} {ℵ lv₁} ()
 
 o∅ : {n : Level} → Ordinal {n}
-o∅  = record { lv = Zero ; ord = Φ Zero }
+o∅  = record { lv = Zero ; ord = Φ Zero ; order = λ n → ⊥-elim (n refl)  }
 
 
 ≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
@@ -100,17 +101,43 @@
 max (Suc x) Zero = (Suc x)
 max (Suc x) (Suc y) = Suc ( max x y )
 
-maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
+maxαd : {n : Level} → { lx : Nat } → (x y : OrdinalD {n} lx ) →  OrdinalD  lx
 maxαd x y with triOrdd x y
 maxαd x y | tri< a ¬b ¬c = y
 maxαd x y | tri≈ ¬a b ¬c = x
 maxαd x y | tri> ¬a ¬b c = x
 
+maxΦ :  {n : Level} → { lx : Nat } → {x y : OrdinalD {n} lx } → maxαd x y ≡ Φ lx → ( x  ≡ Φ lx ) ∧ ( y  ≡ Φ lx  )
+maxΦ {_} {lv} {x} {y} m with triOrdd x y
+maxΦ {_} {lv} {.(Φ lv)} {.(Φ lv)} refl | tri≈ ¬a refl ¬c = record { proj1 = refl ; proj2 = refl }
+maxΦ {_} {lv} {.(Φ lv)} {.(OSuc lv _)} () | tri< Φ< ¬b ¬c
+maxΦ {_} {lv} {.(OSuc lv _)} {.(OSuc lv _)} () | tri< (s< a) ¬b ¬c
+maxΦ {_} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} () | tri< ℵΦ< ¬b ¬c
+maxΦ {_} {.(Suc _)} {.(OSuc (Suc _) _)} {.(ℵ _)} () | tri< ℵ< ¬b ¬c
+maxΦ {_} {lv} {.(OSuc lv _)} {.(Φ lv)} () | tri> ¬a ¬b Φ<
+maxΦ {_} {lv} {.(OSuc lv _)} {.(OSuc lv _)} () | tri> ¬a ¬b (s< c)
+maxΦ {_} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} () | tri> ¬a ¬b ℵΦ<
+maxΦ {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) _)} () | tri> ¬a ¬b ℵ<
+
+maxΦ' : {n : Level} → { lx : Nat } → {x y : OrdinalD {n} lx } → ¬ (maxαd x y ≡ Φ lx ) → ( ¬ x  ≡ Φ lx ) ∨ (¬  y  ≡ Φ lx  )
+maxΦ' {n} {lx} {x} {y} m with triOrdd x y
+maxΦ' {n} {lx} {x} {y} m | tri< a ¬b ¬c = case2 {!!}
+maxΦ' {n} {lx} {x} {y} m | tri≈ ¬a refl ¬c = {!!}
+maxΦ' {n} {lx} {x} {y} m | tri> ¬a ¬b c = {!!}
+
 maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
 maxα x y with <-cmp (lv x) (lv y)
 maxα x y | tri< a ¬b ¬c = x
 maxα x y | tri> ¬a ¬b c = y
-maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) ; order = lemma } where
+   lemma : ¬ maxαd (ord x) (ord y) ≡ Φ (lv y) → {prev : OrdinalD (lv y)} → prev d< maxαd (ord x) (ord y)
+   lemma n with maxΦ' n | triOrdd (ord x) (ord y)
+   lemma n | case1 m | tri< a ¬b ¬c = {!!}
+   lemma n | case2 m | tri< a ¬b ¬c = order y m
+   lemma n | case1 m | tri≈ ¬a refl ¬c = order y m
+   lemma n | case2 m | tri≈ ¬a refl ¬c = order y m
+   lemma n | case1 m | tri> ¬a ¬b c = order x m
+   lemma n | case2 m | tri> ¬a ¬b c = {!!}
 
 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
 a o≤ b  = (a ≡ b)  ∨ ( a o< b )
@@ -150,7 +177,7 @@
    lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
    lemma2 (case1 x) = ¬a x
    lemma2 (case2 x) = trio<> x c
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 {!!} lemma1 where
    lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
@@ -183,8 +210,8 @@
   → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
   → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
-TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
-TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
-    ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = {!!}
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = {!!}
+   -- caseOSuc lv ord₁ ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = {!!} -- caseℵ lv₁