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

changeset 751:71ad137dd101

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, 22 Jul 2022 19:18:05 +0900
parents b96491f7c775
children 2be90b90deb3
files src/zorn.agda
diffstat 1 files changed, 20 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 22 16:52:17 2022 +0900
+++ b/src/zorn.agda	Fri Jul 22 19:18:05 2022 +0900
@@ -449,10 +449,29 @@
                       (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
-        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where
+        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = ? ; order = order } where
            px = Oprev.oprev op
+           px<x : px o< x
+           px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
            zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
            zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+           fcy<sup :  {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
+           fcy<sup {a} {b} a<x fcb with trio< a px
+           ... | tri< a<px ¬b ¬c = ZChain1.fcy<sup (prev px px<x) a<px fcb
+           ... | tri≈ ¬a a=px ¬c = ?
+           ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) a<x ⟫ )
+           order : {b sup1 z1 : Ordinal} → b o< x →
+                sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+           order {b} {sup1} {z1} b<x s<b fcz with trio< b px
+           ... | tri< b<px ¬b ¬c = ZChain1.order (prev px px<x) b<px s<b fcz
+           ... | tri≈ ¬a b=px ¬c = ?
+           ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
+           sup=u : {b : Ordinal} {ab : odef A b} → b o< x →
+                IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab → ZChain.supf zc b ≡ b
+           sup=u {b} {ab} b<x is-sup with trio< b px
+           ... | tri< b<px ¬b ¬c = ZChain1.sup=u (prev px px<x) b<px is-sup
+           ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ? is-sup
+           ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
@@ -461,8 +480,6 @@
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
            ... | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            ... | case2  ¬fy<x  = m01 where
-                 px<x : px o< x
-                 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)