# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660792965 -32400
# Node ID 497b5db603e7d3e78479523e132f7950f9b6e637
# Parent  c97cc257374b87a5e6a97d7c8c570a5726aa278b
...

diff -r c97cc257374b -r 497b5db603e7 src/zorn.agda
--- a/src/zorn.agda	Thu Aug 18 11:48:29 2022 +0900
+++ b/src/zorn.agda	Thu Aug 18 12:22:45 2022 +0900
@@ -799,7 +799,10 @@
                  ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } =  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
                  sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))
-                 sis {z} z≤x = {!!}
+                 sis {z} z<x with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x  ⟫ )
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip