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

changeset 853:2569ace27176

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 Tue, 06 Sep 2022 04:38:39 +0900
parents a28bb57c88e6
children 14bd0c9ad267 d54487b6d43a
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Sep 06 01:18:54 2022 +0900
+++ b/src/zorn.agda	Tue Sep 06 04:38:39 2022 +0900
@@ -915,8 +915,16 @@
                          , ch-init (subst₂ (λ j k → FClosure A f j k  ) refl (supfx b=x) fc) ⟫ 
                      ... | ⟪ au , ch-is-sup u u≤x is-sup fc  ⟫  = ⟪ subst (λ k → odef A k) (supfx b=x) au  
                          , ch-is-sup u (subst (λ k → u o≤ k) (supfx b=x) u≤x) ? zc06 ⟫ where
+                           zc08 : supf0 u o≤ supf0 px
+                           zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x
                            zc06 : FClosure A f (supf1 px u)  (supf1 px b)
-                           zc06 = ?
+                           zc06 with osuc-≡< zc08
+                           ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supfx b=x)  fc where
+                               zc10 : supf0 u ≡ supf1 px u 
+                               zc10 = ?
+                           ... | case2 lt = subst₂ (λ j k → FClosure A f j k ) (supf0=1 (o<→≤ zc09)) (supfx b=x)  fc where
+                               zc09 : u o< px
+                               zc09 = supf-inject0 (ZChain.supf-mono zc) lt
                            zc07 : FClosure A f (supf0 u)  (supf0 px)
                            zc07 = fc
                      zc05 | case1 b≤px with ZChain.csupf zc b≤px 
@@ -924,8 +932,16 @@
                          , ch-init (subst₂ (λ j k → FClosure A f j k  ) refl (supf0=1 b≤px) fc) ⟫ 
                      ... | ⟪ au , ch-is-sup u u≤x is-sup fc  ⟫  = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au  
                          , ch-is-sup u (subst (λ k → u o≤ k) (supf0=1 b≤px) u≤x) ? zc06 ⟫ where
+                           zc08 : supf0 u o≤ supf0 b
+                           zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x
                            zc06 : FClosure A f (supf1 px u)  (supf1 px b)
-                           zc06 = ?
+                           zc06 with osuc-≡< zc08
+                           ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supf0=1 b≤px)  fc where
+                               zc10 : supf0 u ≡ supf1 px u 
+                               zc10 = ?
+                           ... | case2 lt = subst₂ (λ j k → FClosure A f j k ) (supf0=1 zc09) (supf0=1 b≤px)  fc where
+                               zc09 : u o≤ px 
+                               zc09 = ordtrans (supf-inject0 (ZChain.supf-mono zc) lt) b≤px
                            zc07 : FClosure A f (supf0 u)  (supf0 b)
                            zc07 = fc
                  sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px z ≡ & (SUP.sup (sup z≤x))