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

changeset 895:aa496c232604

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sp1 = supf (& A)
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Oct 2022 16:43:09 +0900
parents b09e39629d86
children 1f3a93bb4229
files src/zorn.agda
diffstat 1 files changed, 6 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Oct 06 15:57:08 2022 +0900
+++ b/src/zorn.agda	Thu Oct 06 16:43:09 2022 +0900
@@ -707,6 +707,7 @@
      fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
+           sp1 : SUP A chain
            sp1 = sp0 f mf as0 zc 
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab 
@@ -715,7 +716,11 @@
            z21 : supf (& (SUP.sup sp1)) o< supf (& A)
            z21 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (c<→o< ( SUP.as sp1))) )
            ... | case2 lt = lt
-           ... | case1 eq = ?
+           ... | case1 eq = ? where
+               z24 : supf (& (SUP.sup sp1)) ≡ & (SUP.sup sp1) 
+               z24 = ZChain.sup=u zc ? ? ?
+               z25 : supf (& A) ≡ MinSUP.sup ( ZChain.minsup zc o≤-refl )
+               z25 = ZChain.supf-is-minsup zc o≤-refl 
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )