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

changeset 1416:4d9b60eed372

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
looks connected
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Jun 2023 20:14:26 +0900
parents 85842347e270
children 04bb6152f691
files src/cardinal.agda
diffstat 1 files changed, 17 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Fri Jun 30 19:03:50 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 20:14:26 2023 +0900
@@ -351,13 +351,24 @@
       cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x) → CC0 (h⁻¹ bx cc1 ) 
       cc10 = ?
 
-      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
-      be72 x bx (case1 x₁)  = trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁))
-      be72 x bx (case2 x₁)  = trans ? (a-UC-iso1 x ? )
+      cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x) → CC1 (h ax cc0 ) 
+      cc11 = ?
 
-      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ ? ? ≡ x
-      be73 x bx (case1 x₁)  = trans ? (UC-iso0 x (subst (λ k → odef k x) (sym *iso) ? ))
-      be73 x bx (case2 x₁)  = trans ? (a-UC-iso0 x ? )
+      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
+      be72 x bx (case1 x₁)  with cc10 bx (case1 x₁)
+      ... | case1 c1 = trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁))
+      ... | case2 c2 = ⊥-elim ( c2 ? )
+      be72 x bx (case2 x₁)  with cc10 bx (case2 x₁)
+      ... | case1 c1 = ⊥-elim ( x₁ ? )
+      ... | case2 c2 = trans ? (a-UC-iso1 x ? )
+
+      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x
+      be73 x ax (case1 x₁) with cc11 ax (case1 x₁)
+      ... | case1 c1 = trans ? (UC-iso0 x (subst (λ k → odef k x) (sym *iso) ? ))
+      ... | case2 c2 = ?
+      be73 x ax (case2 x₁) with cc11 ax (case2 x₁)
+      ... | case1 c1 = ⊥-elim ( x₁ ? )
+      ... | case2 c2 = trans ? (a-UC-iso0 x ? )
 
 
 _c<_ : ( A B : HOD ) → Set n