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

changeset 747:c35a5001a0f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial chain separation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 21 Jul 2022 13:20:04 +0900
parents 4a3ba4ad59d4
children 6c8ba542d11b
files src/zorn.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jul 21 09:53:57 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 13:20:04 2022 +0900
@@ -674,8 +674,16 @@
               sup=u :  {b : Ordinal} {ab : odef A b} → b o< x 
                     → IsSup A (UnionCF A f mf ay supf0 x) ab 
                     → supf0 b ≡ b
-              sup=u {b} b<x is-sup with trio< b px
-              ... | tri< a ¬b ¬c = ZChain.sup=u zc a ?
+              sup=u {b} {ab} b<x is-sup with trio< b px
+              ... | tri< a ¬b ¬c = ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
+                     pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
+                     pc20 {z} ⟪ az , record { u = u0 ; u<x = u<x ; uchain = ch-init _ fc } ⟫ = 
+                         IsSup.x<sup is-sup ⟪ az , record { u = u0 ; u<x = case2 refl  ; uchain = ch-init _ fc } ⟫ 
+                     pc20 {z} ⟪ az , record { u = u0 ; u<x = u<x ; uchain = ch-is-sup is-sup-c fc } ⟫ with u<x 
+                     ... | case2 u=0 = ?
+                     ... | case1 u<px = IsSup.x<sup is-sup ⟪ az , record { u = u0 
+                       ; u<x = case1 (subst (λ k → u0 o< k) (Oprev.oprev=x op) (ordtrans u<px <-osuc))
+                       ; uchain = ch-is-sup is-sup-c fc } ⟫ 
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
               order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b