# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558588835 -32400
# Node ID 20cddbb2fc90190d29f4e030c156db893bd31806
# Parent  f10ceee99d00f41df942575eea45a53882bfddde
...

diff -r f10ceee99d00 -r 20cddbb2fc90 ordinal-definable.agda
--- a/ordinal-definable.agda	Thu May 23 13:48:27 2019 +0900
+++ b/ordinal-definable.agda	Thu May 23 14:20:35 2019 +0900
@@ -115,27 +115,10 @@
 ∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ<
 ∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n)
 
-postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
+-- postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
-∅7 : {n : Level} →  { x : OD {n} } → ((z :  OD {n}) → ¬ ( z c< x ))  → x ≡ od∅
-∅7 {n} {x} not = cong ( λ k → record { def = k } ) lemma2 where
-   ⊥-eq :  ⊥ ≡ ⊥
-   ⊥-eq = refl
-   ⊥-leq : lift {_} {n} ⊥ ≡ lift {_} {n} ⊥
-   ⊥-leq = refl
-   lemma0 : Lift n ⊥ → ⊥
-   lemma0 (lift t ) = t
-   lemma0' :  ⊥ → Lift n ⊥
-   lemma0' t = lift t
-   lemma : (y : Ordinal {n}) → ¬ def x y
-   lemma y t = ⊥-elim ( not (ord→od y) (def-subst {n} {x} {y} t refl (sym diso) ) )
-   lemmak : (y : Ordinal {n}) → {m : Level}  → ¬ (Lift m (def x y ))
-   lemmak = {!!}
-   lemma1 : ( y : Ordinal {n}) → def x y ≡ def od∅ y 
-   lemma1 y with ⊥-leq 
-   lemma1 y | refl = {!!}
-   lemma2 : def x ≡ def od∅
-   lemma2 = extensionality ( λ y → lemma1 y )
+-- ∅7 : {n : Level} →  { x : OD {n} } → ((z :  OD {n}) → ¬ ( z c< x ))  → x ≡ od∅
+-- ∅7 {n} {x} not = cong ( λ k → record { def = k } ) lemma2 where
 
 ∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅
 ∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x
@@ -143,14 +126,13 @@
 ∅6 {n} x lt refl | tri≈ ¬a b ¬c =  ¬a lt
 ∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl
 
-∅2 : {n : Level} →  ( x : OD {n} )  → ¬ ( x  ≡ od∅ {n} ) → od∅ {n} c< x
-∅2 {n} x not with od→ord x
-... | ox = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (o∅ {n}))}  (o<→c< (∅5 (od→ord x) lemma )) oiso lemma0 where
-   lemma0 : od→ord (ord→od (o∅ {n})) ≡ od→ord (od∅ {n})
-   lemma0 = trans diso (sym ( ∅4 (od∅ {n}) refl)  )
-   lemma : ¬ (od→ord x) ≡ o∅
-   lemma = {!!}
+∅7 : {n : Level} →  ( x : OD {n} )   → od→ord x ≡ o∅ {n} →  x  ≡ od∅ {n}
+∅7 = {!!}
 
+∅9 : {n : Level} → (x : OD {n} ) → ¬ x ≡ od∅ → o∅ o< od→ord x
+∅9 x not = ∅5 ( od→ord x) lemma where
+   lemma : ¬ od→ord x ≡ o∅
+   lemma eq = not ( ∅7 x eq )
 
 open Ordinal
 
@@ -221,7 +203,7 @@
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
          minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} 
-         minimul record { def = def } not = {!!}
+         minimul x  not = ord→od ( ominimal (od→ord x) (∅9 x not) )
          regularity : (x : OD) → (not : ¬ x ≡ od∅ ) →
                 Lift (suc n) (x ∋ minimul x not ) ∧
                 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)