# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559052170 -32400
# Node ID 323b561210b538074bf69b753a353831f07b4fda
# Parent  419688a279e0f1d4a84742f854492c887cadca31
...

diff -r 419688a279e0 -r 323b561210b5 ordinal-definable.agda
--- a/ordinal-definable.agda	Tue May 28 11:31:43 2019 +0900
+++ b/ordinal-definable.agda	Tue May 28 23:02:50 2019 +0900
@@ -339,39 +339,44 @@
          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
-         regularity-ord :  (x : Ordinal ) (not :  o∅ o< x ) →
-            (ord→od x ∋ minimul (ord→od x) (∅0 not)) ∧ (Select (minimul (ord→od x) (∅0 not)) (λ x₁ → (minimul (ord→od x) (∅0 not) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
-         proj1 ( regularity-ord x non ) =  minimul<x (ord→od x) (∅0 non) 
-         proj2 ( regularity-ord x non ) = reg1 where
-            reg2 : {y : Ordinal} → ( def (minimul (ord→od x) (∅0 non)) y ∧ (minimul (ord→od x) (∅0 non) ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥ 
+         regularity-ord :  (x : Ordinal ) (not :  ¬ (ord→od x == od∅)) →
+            (ord→od x ∋ minimul (ord→od x) not) ∧ (Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
+         proj1 ( regularity-ord x not ) =  minimul<x (ord→od x) not 
+         proj2 ( regularity-ord x not ) = reg1 where
+            reg2 : {y : Ordinal} → ( def (minimul (ord→od x) not) y ∧ (minimul (ord→od x) not ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥ 
             reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
             ... | p1 | p2 | p3  with is-∋ (ord→od x) ( ord→od y)
             reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 )                         --  ¬ x ∋ ord→od y     empty x case
-            reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) (∅0 non)) (ord→od y)
+            reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) not) (ord→od y)
             reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 )                 --  minimum contains nothing q.e.d.
             reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!}
-            reg0 : {y : Ordinal {suc n}} → Minimumo x → def (Select (minimul (ord→od x) (∅0 non)) (λ z → (minimul (ord→od x) (∅0 non) ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
-            reg0 {y} m t with trio< y (mino (minord (ord→od x) (∅0 non))) 
-            reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} t 
+            reg0 : {y : Ordinal {suc n}} → def (Select (minimul (ord→od x) not) (λ z → (minimul (ord→od x) not ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
+            reg0 {y} t with trio< y (mino (minord (ord→od x) not)) 
+            reg0 {y} t | tri< a ¬b ¬c with reg2 {y} t 
             ... | ()
-            reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) (∅0 non)) ) refl
-                     (def-subst {suc n} {ord→od y} {mino (minord (ord→od x)  (∅0 non))} (proj1 t) refl (sym diso))
+            reg0 {y} t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) not) ) refl
+                     (def-subst {suc n} {ord→od y} {mino (minord (ord→od x)  not)} (proj1 t) refl (sym diso))
                   where
                lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy  → ord→od ox c< ord→od oy  → Lift (suc n) ⊥
                lemma ox oy refl lt =  lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od  oy} refl lt )
-            reg0 {y} m t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) (∅0 non))) (lemma {!!}) c where
-                lemma : def (ord→od (mino (ominimal x (∅5 (λ eq → (∅0 non) (∅7 {!!})))))) y → y o< mino (minord (ord→od x) (∅0 non))
-                lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) (∅0 non)))} 
-                         (def-subst {suc n}  {ord→od (mino (minord (ord→od x) (∅0 non)))} {y} {!!} refl (sym diso))
+            reg0 {y} t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) not)) (lemma {!!}) c where
+                lemma : def (ord→od (mino (minord (ord→od x)  not))) y → y o< mino (minord (ord→od x) not)
+                lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) not))} 
+                         (def-subst {suc n}  {ord→od (mino (minord (ord→od x) not))} {y} {!!} refl (sym diso))
                 lemma d | clt = o<-subst clt ord-iso ord-iso
             ... | ()
-            reg1 :  Select (minimul (ord→od x) (∅0 non)) (λ x₁ → (minimul (ord→od x) (∅0 non) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
-            reg1 = record { eq→ =  reg0 (ominimal x non) ; eq← = λ () } where
+            reg1 :  Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
+            reg1 = record { eq→ = reg0  ; eq← = λ () } where
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  where
          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 with regularity-ord ( od→ord x ) ( ∅9 not )
-         ... | t = ?
-         
+         proj1 (regularity x not ) = minimul<x x not
+         proj2 (regularity x not ) = record { eq→ = reg4 ; eq← = λ () } where
+            reg4 :  {xd : Ordinal } → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) xd → def od∅ xd
+            reg4 {xd} = {!!} (eq→ (proj1 (regularity-ord {!!} {!!} )) )
 
+
+
+
+