# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559123457 -32400
# Node ID 87df00599a0e19f26e2c0bbdefa9038af45c57c8
# Parent  ba43f7ff60d4426fbba97d44e198758fb4eabd7c
equal

diff -r ba43f7ff60d4 -r 87df00599a0e ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 29 14:28:26 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 18:50:57 2019 +0900
@@ -353,19 +353,35 @@
          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 () } 
+         omin∅≡min∅ : (ox : Ordinal {suc n}) → {not : ¬ ( ord→od ox == od∅)} 
+            → mino (ominimal ox (∅10 refl not)) ≡ mino (ominimal (od→ord (ord→od ox)) (∅9 not)) 
+         omin∅≡min∅ ox  {not} with ominimal ox (∅10 refl not)
+         omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) }  | record { mino = mino ; min<x = case1 () }
+         omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) }  | record { mino = mino ; min<x = case2 () }
+         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  | record { mino = _ ; min<x = case1 () }
+         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  | record { mino = record { lv = 0 ; ord = Φ 0 } ; min<x = case2 Φ< } =  {!!}
+         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } {_} | record { mino = record { lv = .0 ; ord = .(OSuc 0 _) } ; min<x = case2 (s< x)}  = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  | record { mino = mino ; min<x = case2 () }
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  | record { mino = _ ; min<x = case2 lt } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  | record { mino = _ ; min<x = case2 lt }  = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = ord } {not} | record { mino = mino ; min<x = min<x } = {!!}
+         omin∅→min∅ : (ox : Ordinal {suc n}) { x : OD {suc n} } →  {not : ¬ ( ord→od ox == od∅)} 
+            → mino (ominimal ox (∅10 refl not)) ≡ o∅ → mino (ominimal (od→ord (ord→od ox)) (∅9 not)) ≡ o∅
+         omin∅→min∅ ox {x} {not} eq with ominimal ox (∅10 refl not)
+         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  eq | record { mino = mino ; min<x = case1 () }
+         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  eq | record { mino = mino ; min<x = case2 () }
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl | record { mino = .o∅ ; min<x = case1 () }
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl | record { mino = .o∅ ; min<x = case2 Φ< } = 
+               subst (λ k → ?  ≡ k  ) ? (omin∅→min∅ o∅ {!!})
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  eq | record { mino = mino ; min<x = case2 () }
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl | record { mino = .o∅ ; min<x = case2 () }
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  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