# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563492876 -32400
# Node ID 729b80df8a8a954b0f47241a60d831d126617afa
# Parent  c96f28c3c387f0e2dbc95c40bfb1cb1ede0f2811
...

diff -r c96f28c3c387 -r 729b80df8a8a HOD.agda
--- a/HOD.agda	Fri Jul 19 07:04:13 2019 +0900
+++ b/HOD.agda	Fri Jul 19 08:34:36 2019 +0900
@@ -238,7 +238,7 @@
 
 -- another form of regularity 
 --
-{-# TERMINATING #-}
+-- {-# TERMINATING #-}
 ε-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
@@ -252,12 +252,16 @@
             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 = oy }} (case1 (s≤s x)) with <-cmp lx ly
-    ... | tri< a ¬b ¬c = ⊥-elim (lemma a x ) where  
-            lemma : {lx ly : Nat} → Suc lx ≤ ly → ly ≤ lx → ⊥
-            lemma (s≤s lt1) (s≤s lt2) = lemma lt1 lt2
-    ... | tri≈ ¬a refl ¬c = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso ? 
-    ... | tri> ¬a ¬b c =  ε-induction-ord record { lv = lx ; ord = (Φ lx) }  (case1 c)
+    ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {oy} =  
+        TransFinite {suc n} {suc n ⊔ m} {λ x → x o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od x)} lemma1 lemma2 oy where
+            lemma1 : (ly : Nat) →
+                    record { lv = ly ; ord = Φ ly } o< record { lv = Suc lx ; ord = Φ (Suc lx) } →
+                    ψ (ord→od (record { lv = ly ; ord = Φ ly }))
+            lemma1 ly lt = ind {!!} 
+            lemma2  : (ly : Nat) (oy : OrdinalD ly) →
+                    (record { lv = ly ; ord = oy } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od (record { lv = ly ; ord = oy }))) →
+                    record { lv = ly ; ord = OSuc ly oy } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od (record { lv = ly ; ord = OSuc ly oy }))
+            lemma2 ly oy p lt = ind {!!}
 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}