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

changeset 708:7c0aa5a9ab3f

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 Wed, 13 Jul 2022 10:40:28 +0900
parents e9ddbf84d699
children 6795b58f2f0c
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Jul 13 09:50:10 2022 +0900
+++ b/src/zorn.agda	Wed Jul 13 10:40:28 2022 +0900
@@ -528,8 +528,17 @@
                             * a < * b → odef pchain b
                 zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ⟪ ab , record { u = ? ; u<x = ? ; uchain = ? } ⟫
-                -- ZChain.is-max zc ? (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab ? a<b
+                ... | case2 lt = zc6 where
+                    zc5 : odef pchain a → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a
+                    zc5 za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = ? ; uchain = UChain.uchain (proj2 za)  } ⟫
+                    zc2 : odef (UnionCF A f mf ay (ZChain.supf zc) px ) b
+                    zc2 = ZChain.is-max zc ? (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ab ? a<b
+                    zc3 : (UChain.u (proj2 zc2) o< x) ∨ (UChain.u (proj2 zc2) ≡ y)
+                    zc3 with UChain.u<x (proj2 zc2) 
+                    ... | case1 lt = case1 (ordtrans lt px<x)
+                    ... | case2 eq = case2 eq
+                    zc6 : odef pchain b
+                    zc6 = ⟪ ab , record { u = UChain.u (proj2 zc2) ; u<x = zc3 ; uchain = UChain.uchain (proj2 zc2) } ⟫ 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next