# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563474478 -32400
# Node ID b25a4eca06a60a3a964e340fd1cce38fb71808c2
# Parent  4724f7be00e3fc5ba3b8664ea94c566912be8b77
...

diff -r 4724f7be00e3 -r b25a4eca06a6 HOD.agda
--- a/HOD.agda	Thu Jul 18 16:06:41 2019 +0900
+++ b/HOD.agda	Fri Jul 19 03:27:58 2019 +0900
@@ -467,16 +467,23 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
+         -- another form of regularity 
+         --
          ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}
               → ( {x : OD {suc n} } → ({ y : OD {suc n} } →  x ∋ y → ψ y ) → ψ x )
               → (x : OD {suc n} ) → ψ x
-         ε-induction {n} {m} {ψ} ind x with od→ord x  | oiso {suc n} {x}
-         ε-induction {n} {m} {ψ} ind x | record { lv = Zero ; ord = Φ 0 } | refl = ind (lemma o∅≡od∅  ) where
-               lemma : { y : OD {suc n} } → x ≡ od∅  → x ∋ y → ψ y 
-               lemma {y} eq lt with empty y (o<-subst (c<→o< lt) refl diso )
-               lemma {y} eq lt | ()
-         ε-induction {n} {m} {ψ} ind x | record { lv = Zero ; ord = OSuc 0 ox } | refl = {!!}
-         ε-induction {n} {m} {ψ} ind x | record { lv = Suc lx ; ord = Φ (Suc lx) } | refl = {!!}
-         ε-induction {n} {m} {ψ} ind x | record { lv = Suc lx ; ord = OSuc (Suc lx) ox } | refl = {!!}
+         ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x))  <-osuc) where
+             ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox  → ψ (ord→od oy)
+             ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case1 ())
+             ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case2 ())
+             ε-induction-ord record { lv = lx ; ord = (OSuc lx ox) } {oy} y<x = 
+                 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where
+                     lemma :  (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox }
+                     lemma y lt with osuc-≡< y<x
+                     lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso
+                     lemma y lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1
+             ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = OSuc ly oy }} (case1 (s≤s x)) =
+               ind {ord→od record { lv = ly ; ord = OSuc ly oy }} (
+                 λ {y} lt →  subst ( λ k → ψ k ) oiso ( ε-induction-ord record { lv = lx ; ord = (Φ lx) } {od→ord y} {!!})) where
+             ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = Φ ly }} (case1 (s≤s x)) = {!!}
 
---              subst (λ k → ψ k ) oiso (TransFinite {suc n} {suc (suc n) ⊔ m} {λ x → ({y : Ordinal } → y o< x → ψ y ) → ψ (ord→od x) } {!!} {!!} {!!} {!!})