# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664526937 -32400
# Node ID 3c2ab35da199d04c63e669de3e1ba989a38587a5
# Parent  d4839adf694dcb9a9090b5edad7d89b1bf3f1137
...

diff -r d4839adf694d -r 3c2ab35da199 src/zorn.agda
--- a/src/zorn.agda	Fri Sep 30 14:38:07 2022 +0900
+++ b/src/zorn.agda	Fri Sep 30 17:35:37 2022 +0900
@@ -914,10 +914,18 @@
                  ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 lt)) (sym sfpx=px) ( supf-mono z≤w )
                  supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
                  ... | tri< a ¬b ¬c = zc19 where
-                       zc19 : supf0 z o≤ sp1
-                       zc19 = ?
+                       zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
+                       zc21 = ZChain.minsup zc (o<→≤ a)
+                       zc23 : odef A sp1
+                       zc23 = MinSUP.asm sup1
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 ?
+                       zc19 : supf0 z o≤ sp1 
+                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a))) ( MinSUP.minsup zc21 zc23 zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
-                       zc18 : px o≤ sp1
+                       zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
+                       zc21 = ZChain.minsup zc (o≤-refl0 b)
+                       zc18 : px o≤ sp1 -- supf0 z ≡ px 
                        zc18 = ?
                  ... | tri> ¬a ¬b c = o≤-refl
 
@@ -1086,7 +1094,7 @@
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc32 = ZChain.sup zc o≤-refl 
                      zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 ne {w} lt with zc11 P ? 
+                     zc34 ne {w} lt with zc11 P ⟪ proj1 lt , ? ⟫
                      ... | case1 lt = SUP.x<sup zc32 lt 
                      ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)