Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 173:e6e1bdbda450

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Jul 2019 15:28:20 +0900
parents 8c4d1423d7c4
children ad7a6185b6d5
files HOD.agda
diffstat 1 files changed, 6 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Fri Jul 19 14:59:28 2019 +0900
+++ b/HOD.agda	Fri Jul 19 15:28:20 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
@@ -285,8 +285,11 @@
             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 )))
+            ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx
+               (ox lz=ly  -- ord (od→ord z) d< ord (od→ord (ord→od (record { lv = lx ; ord = oy })))
+                    (subst (λ k → lv (od→ord z) ≡ k ) lemma1 eq) ) {_} {ord (od→ord z)} (case2 {!!})) where
+                 ox : {lx lz : Nat} → {oy : OrdinalD {suc n} lz} {oz : OrdinalD {suc n} lx} → {!!} d< {!!} → lz ≡ lx → OrdinalD {suc n} lx
+                 ox = ?
              
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}