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

changeset 856:d54487b6d43a

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 10:25:49 +0900
parents 2569ace27176
children 266e0b9027cd
files src/zorn.agda
diffstat 1 files changed, 26 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Sep 06 04:38:39 2022 +0900
+++ b/src/zorn.agda	Tue Sep 06 10:25:49 2022 +0900
@@ -914,14 +914,22 @@
                      ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au  
                          , 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
+                         , ch-is-sup u (subst (λ k → u o≤ k) (supfx b=x) u≤x) zc13  zc06 ⟫ where
+                           zc13 : ChainP A f mf ay (supf1 px) u
+                           zc13 with trio< u px 
+                           ... | tri< a ¬b ¬c = CP0→1 supf-mono (o<→≤ a) is-sup
+                           ... | tri≈ ¬a b ¬c = CP0→1 supf-mono (o≤-refl0 b) is-sup
+                           ... | tri> ¬a ¬b px<u = ?
                            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 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 = ?
+                               zc10 with trio< u px 
+                               ... | tri< a ¬b ¬c = refl
+                               ... | tri≈ ¬a b ¬c = refl
+                               ... | tri> ¬a ¬b px<u = eq 
                            ... | 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
@@ -931,14 +939,28 @@
                      ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au  
                          , 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
+                         , ch-is-sup u (subst (λ k → u o≤ k) (supf0=1 b≤px) u≤x) zc13 zc06 ⟫ where
+                           zc13 : ChainP A f mf ay (supf1 px) u
+                           zc13 with trio< u px 
+                           ... | tri< a ¬b ¬c = CP0→1 supf-mono (o<→≤ a) is-sup
+                           ... | tri≈ ¬a b ¬c = CP0→1 supf-mono (o≤-refl0 b) is-sup
+                           ... | tri> ¬a ¬b px<u = ?
                            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 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 = ?
+                               zc10 with trio< u px 
+                               ... | tri< a ¬b ¬c = refl
+                               ... | tri≈ ¬a b ¬c = refl
+                               ... | tri> ¬a ¬b px<u = zc12 where
+                                    zc11 : supf0 u o≤ supf0 px
+                                    zc11 = subst (λ k → k o≤ supf0 px ) (sym eq) ( ZChain.supf-mono zc b≤px )
+                                    zc12 : supf0 u ≡ supf0 px
+                                    zc12 with osuc-≡< zc11
+                                    ... | case1 eq2 = eq2
+                                    ... | case2 lt = ⊥-elim ( o<> px<u (ZChain.supf-inject zc lt ))
                            ... | 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