# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558968356 -32400
# Node ID 9c0a5e28a57250c2034f6aa05764a96f9124f648
# Parent  33fb8228ace99228e3c783179db1077f0ddb5d3c
regurality elimination case

diff -r 33fb8228ace9 -r 9c0a5e28a572 ordinal-definable.agda
--- a/ordinal-definable.agda	Mon May 27 21:58:17 2019 +0900
+++ b/ordinal-definable.agda	Mon May 27 23:45:56 2019 +0900
@@ -297,7 +297,7 @@
        ;   regularity = regularity
        ;   infinity∅ = {!!}
        ;   infinity = {!!}
-       ;   selection = selection
+       ;   selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
        ;   replacement = {!!}
      } where
          open _∧_ 
@@ -332,24 +332,32 @@
          proj2 ( regularity x non ) = reg1 where
             reg2 : {y : Ordinal} → ( def (minimul x non) y ∧ (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥ 
             reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
-            ... | p1 | p2 | p3 = ?
+            ... | p1 | p2 | p3 = {!!}
             reg0 : {y : Ordinal {suc n}} → Minimumo (od→ord x) → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
             reg0 {y} m t with trio< y (mino (minord x non)) 
             reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} ( record {
                     proj1 = (def-subst {suc n} {minimul x  non} (o<→c< a) refl diso ) 
-                  ; proj2 = record { proj1 = {!!}
-                  ; proj2 = {!!}
-                 }} )
+                  ; proj2 = record { proj1 = proj1 (proj2 t )
+                  ; proj2 = proj2 (proj2 t )
+                 }} ) 
             ... | ()
-            reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord x non) ) {!!} where
-               lemma : ( ox oy : Ordinal {suc n} ) → ord→od ox c< ord→od oy  → Lift (suc n) ⊥
-               lemma ox oy lt =  lift ( o≡→¬c< {suc n} refl lt )
-               -- o≡→¬c< {suc n} refl ( c<→o< {suc n} {ord→od y} {ord→od (od→ord (minimul x non))} (proj1 t) )
-            reg0 {y} m t | tri> ¬a ¬b c = lemma y ( mino (minord x non) ) {!!} {!!} where
-               lemma : ( ox oy : Ordinal {suc n} ) → ox o< oy   → ord→od oy c< ord→od ox  → Lift (suc n) ⊥
-               lemma ox oy (case1 x) yc<x = {!!}
-               lemma ox oy (case2 lt) yc<x with d<→lv lt
-               ... | refl = lift ( o<→¬c> {suc n}  (case2 {!!}) yc<x  )
+            reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord x non) ) refl
+                     (def-subst {suc n} {ord→od y} {mino (minord x  non)} (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 x non)) (lemma (proj1 t)) c where
+                lemma : def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 eq)))))) y → y o< mino (minord x non)
+                lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord x non))} 
+                         (def-subst {suc n}  {ord→od (mino (minord x non))} {y} d refl (sym diso))
+                lemma d | clt = o<-subst clt ord-iso ord-iso
+            ... | ()
             reg1 :  Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
             reg1 = record { eq→ =  reg0 (minord x non) ; eq← = λ () }
 
+
+--               (o<-subst {suc n} {y} (c<→o< {suc n} (def-subst {suc n} (proj1 t ) {!!} {!!} )) {!!} {!!} )
+--            c<> {n} (o<→c< {suc n} {mino (minord x  non)} {y} (case2 lto))
+--                  (def-subst {suc n} {ord→od (mino (minord x  non))} {y} lt refl refl ) --            lemma y ( mino (minord x non) )
+--                 (def-subst {suc n} {ord→od y} {mino (minord x  non)} (proj1 t) refl (sym diso))
+--                     {!!} where