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

diff -r f2cb756084e0 -r 05494b4689ed ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 29 13:02:03 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 13:41:12 2019 +0900
@@ -349,26 +349,28 @@
          minord x not = ominimal (od→ord x) (∅9 not)
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
          minimul x  not = ord→od ( mino (minord x not))
+         omin→cmin : {x : OD {suc n}}  →  {not :  ¬ x == od∅ } → mino (minord x not)  o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
+         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 = lemma0 (min<x (minord x not)) where
-            lemma0 : mino (minord x not)  o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
-            lemma0 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 not =  omin→cmin {x} {not} (min<x (minord x not)) 
          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
              regularity-ord : (ox : Ordinal ) → {x : OD} → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅))
                   → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
-             regularity-ord ox {x} refl not  with ominimal ox (∅10 refl not)
-             regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case1 () }
-             regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case2 () }
-             regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = min ; min<x = case1 () }
-             regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Suc lv₁ ; ord = ord } ; min<x = case2 () }
-             regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< }
-               = record { proj1 = {!!} ; proj2 = record { eq→ = {!!} ; eq← = λ () }} where
-                lemma : ? -- ominimal ox (∅10 refl not) ≡ minimul x not
-                lemma = {!!}
-             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) } = {!!}
-             regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case1 lt } = {!!}
-             regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case2 () }
-             regularity-ord record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl not | record { mino = min ; min<x = min<x } = {!!}
-             regularity-ord record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } refl not | record { mino = min ; min<x = min<x } = {!!}
+             regularity-ord ox {x} refl not  with ominimal ox (∅10 refl not) | minimul x not | is-o∅ (mino (minord x not)) | is-o∅ ox
+             regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case1 () } | r | t | s
+             regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case2 () } | r | t | s
+             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} = {!!}
+             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  = {!!}
+             regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case1 lt } | r | t | s = {!!}
+             regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case2 () } | r | t | s
+             regularity-ord record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl not | record { mino = min ; min<x = min<x }  | r | t | s = {!!}
+             regularity-ord record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } refl not | record { mino = min ; min<x = min<x } | r | t | s = {!!}