# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563577426 -32400
# Node ID ecb329ba38ac904913313f2dd03ae2329039ffa6
# Parent  51189f7b922974181966275f735c0807038f4b8e
ε-induction done

diff -r 51189f7b9229 -r ecb329ba38ac HOD.agda
--- a/HOD.agda	Fri Jul 19 17:16:43 2019 +0900
+++ b/HOD.agda	Sat Jul 20 08:03:46 2019 +0900
@@ -236,62 +236,6 @@
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n})  → L α ∋ x → L β ∋ x 
 
--- another form of regularity 
---
--- {-# 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 (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 (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 = lemma6 {lx} {ly} {lv (od→ord z)} {Φ lx} {oy} {ord (od→ord z)} {!!} ? ? where
-                  lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
-                  lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
-                  lemma6 : { lx ly lz : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } { oz : OrdinalD {suc n} lz } →
-                       lx ≡ ly → ly ≡ lz →  oz d< oy → ψ z 
-                  lemma6 {lx} {ly} {lz} {ox} {oy} {oz} refl refl _ = lemma5 {!!} (case2 {!!} )
-
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
@@ -523,3 +467,59 @@
          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 
+         --
+         -- {-# 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 (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 (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 = lemma6 {ly} {Φ lx} {oy} refl (sym (subst (λ k → lv (od→ord z) ≡  k) lemma1 eq)) where
+                          lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
+                          lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
+                          lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly }  →
+                               lx ≡ ly → ly ≡ lv (od→ord z)  →  ψ z 
+                          lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
+