# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558787467 -32400
# Node ID 7cb32d22528c85cc837cce5ca96b4f3bddd6d705
# Parent  7c23969befc97c94be27c8ed2169deb6e10e3ca1
...

diff -r 7c23969befc9 -r 7cb32d22528c ordinal-definable.agda
--- a/ordinal-definable.agda	Sat May 25 20:48:20 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 21:31:07 2019 +0900
@@ -232,10 +232,11 @@
             (x ∋ minimul x not) ∧ (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 ( regularity x non ) =  minimul<x x non 
          proj2 ( regularity x non ) = reg1 where
-            reg3 : {y : Ordinal} → ((y ≡ od→ord (ord→od (mino (minord x non)))) ∨ (y ≡ od→ord x) )
-                ∧ ( def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 x eq)))))) (od→ord (ord→od y))
+            reg3 : {y : Ordinal} → ((y ≡ od→ord
+                        (ord→od (mino (minord x non)))) ∨ (y ≡ od→ord x) )
+                ∧ ( def (ord→od (mino (minord x non))) (od→ord (ord→od y))
                 ∧ def x (od→ord (ord→od y))) → Lift n ⊥
-            reg3 = {!!}
+            reg3 {y} = {!!}
             reg0 : {y : Ordinal} → def (Select (minimul x non , x)
                      (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
             reg0 {y} t = reg3 t