# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559107706 -32400
# Node ID ba43f7ff60d4426fbba97d44e198758fb4eabd7c
# Parent  05494b4689ed7362c33cf63ff6c1a275910c6955
omin

diff -r 05494b4689ed -r ba43f7ff60d4 ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 29 13:41:12 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 14:28:26 2019 +0900
@@ -353,6 +353,19 @@
          omin→cmin  {x} {not} m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
          minimul<x : (x : OD {suc n} ) →  (not :  ¬ x == od∅ ) → x ∋ minimul x not
          minimul<x x not =  omin→cmin {x} {not} (min<x (minord x not)) 
+         omin∅→min∅ : (ox : Ordinal {suc n}) { x : OD {suc n} } → ( x ≡ ord→od ox ) → {non : ¬ ( ord→od ox == od∅)} →  {not : ¬ (x == od∅)} 
+            → mino (ominimal ox (∅10 refl non)) ≡ o∅ → mino (ominimal (od→ord x) (∅9 not)) ≡ o∅
+         omin∅→min∅ ox {x} refl {non} {not} eq with ominimal ox (∅10 refl non)
+         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  refl eq | record { mino = mino ; min<x = case1 () }
+         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  refl eq | record { mino = mino ; min<x = case2 () }
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl refl | record { mino = .o∅ ; min<x = case1 () }
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl refl | record { mino = .o∅ ; min<x = case2 Φ< } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl eq | record { mino = mino ; min<x = case2 () }
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl refl | record { mino = .o∅ ; min<x = case2 () }
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl refl | record { mino = .o∅ ; min<x = case2 () } 
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          regularity x not = regularity-ord (od→ord x) {x} (sym oiso ) not where
@@ -364,9 +377,7 @@
              regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = min ; min<x = case1 () } | r | t | s
              regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Suc lv₁ ; ord = ord } ; min<x = case2 () } | r | t | s
              regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } | r | yes p | s 
-                = record { proj1 = _ ; proj2 = record { eq→ = {!!}   ; eq← = λ () } } where
-                   lemma : { y : Ordinal } → def ( Select r (λ x₁ → (r ∋ x₁) ∧ (x ∋ x₁))) y → def od∅ y
-                   lemma {y} = {!!}
+                = record { proj1 = {!!}  ; proj2 = record { eq→ = {!!}   ; eq← = λ () } }  
              regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } | r | no ¬p | yes p = {!!}
              regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } | r | no ¬p | no ¬p₁ = {!!}
              regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl not | record { mino = record { lv = Zero ; ord = OSuc .0 ord₂ } ; min<x = case2 (s< lt) } | r | t | s  = {!!}