# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563515968 -32400
# Node ID 8c4d1423d7c43778bfdba3b7b84d1479214f554a
# Parent  729b80df8a8a954b0f47241a60d831d126617afa
non terminateing on ε-induction

diff -r 729b80df8a8a -r 8c4d1423d7c4 HOD.agda
--- a/HOD.agda	Fri Jul 19 08:34:36 2019 +0900
+++ b/HOD.agda	Fri Jul 19 14:59:28 2019 +0900
@@ -238,31 +238,56 @@
 
 -- 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
-ε-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 }
+ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x)))  <-osuc) where
+    ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
+        → (ly < lx) ∨ (oy d< ox  ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
+    ε-induction-ord Zero (Φ 0)  (case1 ())
+    ε-induction-ord Zero (Φ 0)  (case2 ())
+    ε-induction-ord lx  (OSuc lx ox) {ly} {oy} y<x = 
+        ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
+            lemma :  (y : OD) → ord→od record { lv = ly ; ord = 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)) } {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 {!!}
-
+            lemma y lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1  
+    ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =                    
+        ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt )  where  
+            lemma0 : { lx ly : Nat } → ly < Suc lx  → lx < ly → ⊥
+            lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2
+            lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly
+            lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin
+                    lv (od→ord (ord→od (record { lv = ly ; ord = oy })))
+                 ≡⟨ cong ( λ k → lv k ) diso ⟩
+                    lv (record { lv = ly ; ord = oy })
+                 ≡⟨⟩
+                    ly
+                 ∎
+            lemma2 : { lx : Nat } → lx < Suc lx  
+            lemma2 {Zero} = s≤s z≤n
+            lemma2 {Suc lx} = s≤s (lemma2 {lx})
+            --                         lx    Suc lx      (1) z(a) <lx by case1
+            --                 ly(1)   ly(2)             (2) z(b) <lx by case1
+            --           z(a)  z(b)    z(c)                  z(c) <lx by case2 ( ly==z==x)
+            --
+            lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
+            lemma z lt with  c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt
+            lemma z lt | case1 lz<ly with <-cmp lx ly
+            lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
+            lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c =     -- (1)
+                  subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
+            lemma z lt | case1 lz<ly | tri> ¬a ¬b c =       -- z(a)
+                  subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
+            lemma z lt | case2 lz=ly with <-cmp lx ly
+            lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
+            lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly       -- z(b)
+            ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
+            lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly    -- z(c)
+            ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord (Suc lx) (Φ (Suc lx)) {_} {ord (od→ord z)}
+                  (case1 (subst (λ k → k < Suc lx) (trans (sym lemma1) (sym eq)) lemma2 )))
+             
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record {