# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559102523 -32400
# Node ID f2cb756084e03608cec661cc9520e9a083f53b0e
# Parent  6a1f67a4cc6e9fb5bca7a8cbdc5c0bc34620ec93
fix

diff -r 6a1f67a4cc6e -r f2cb756084e0 ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 29 12:06:43 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 13:02:03 2019 +0900
@@ -355,29 +355,20 @@
             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
          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∅))
+         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  = record { proj1 = minimul<x x not ; proj2 = record {eq→ = reg0 ; eq← = λ () } } where
-               noto : o∅ o< (od→ord (ord→od ox)) 
-               noto = lemma {ox} {od→ord (ord→od ox)} diso (∅10 refl not) where
-                  lemma : { ox oy : Ordinal {suc n}} → oy ≡ ox → o∅ o< ox → o∅ o< oy
-                  lemma refl lt = lt
-               Min : Minimumo ox 
-               Min = ominimal ox (∅10 refl not)
-               Mino : Minimumo (od→ord (ord→od ox )) 
-               Mino = ominimal (od→ord (ord→od ox )) noto
-               m=mo : ox ≡ od→ord (ord→od ox ) → mino Mino ≡ mino Min
-               m=mo eq with ox
-               ... | xx = ?
-               reg0 : {y : Ordinal {suc n}} → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) y → def od∅ y
-               reg0 {y} t with  trio< y ( mino Mino )
-               reg0 {y} t | tri< a ¬b ¬c = {!!}
-               reg0 {y} t | tri≈ ¬a refl ¬c with  o≡→¬c< {suc n} {ord→od (mino Mino)} refl lemma where
-                   lemma : ord→od y c< ord→od (mino Mino)
-                   lemma = subst (λ k → k  c< ord→od (mino Mino) ) oiso {!!} -- (proj1 t)
-               reg0 {y} t | tri≈ ¬a b ¬c | ()
-               reg0 {y} t | tri> ¬a ¬b c with  o<> y (mino Mino) lemma c where
-                   lemma : y o< mino Mino
-                   lemma = {!!}
-               reg0 {y} t | tri> ¬a ¬b c | ()
+             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 } = {!!}