# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662744923 -32400
# Node ID 06f692bf7a97292f20134465b496b82e10904a5d
# Parent  f5fc3f5f618fb5fb57cd6872c0849675bb510875
...

diff -r f5fc3f5f618f -r 06f692bf7a97 src/zorn.agda
--- a/src/zorn.agda	Fri Sep 09 20:20:39 2022 +0900
+++ b/src/zorn.agda	Sat Sep 10 02:35:23 2022 +0900
@@ -780,13 +780,15 @@
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                  zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup  fc  ⟫
                  zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
-                        → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( supf0 px ≡ px )
+                        → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
                  zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
                  zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px 
                  ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc  ⟫ 
-                 ... | tri≈ ¬a eq ¬c  = case2 (subst (λ k → supf0 k ≡ k) eq s1u=u) where
+                 ... | tri≈ ¬a eq ¬c  = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 fc ⟫ where
                         s1u=u : supf0 u1 ≡ u1
                         s1u=u = ChainP.supu=u u1-is-sup
+                        zc12 : supf0 u1 ≡ px 
+                        zc12 = trans (ChainP.supu=u u1-is-sup) eq
                  zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
@@ -815,9 +817,12 @@
                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                         zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl)
                                  ; is-sup = record { x<sup = x<sup } }
-                 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where
+                 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where
                         eq : u1 ≡ x 
-                        eq = ?
+                        eq with trio< u1 x
+                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
+                        ... | tri≈ ¬a b ¬c = b
+                        ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c )
                         zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
                         zc20 {z} (init asu su=z ) = zc13 where
                           zc14 : x ≡ z
@@ -844,9 +849,13 @@
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 {w} lt = SUP.x<sup zc32 ? where
-                         zc35 : odef (UnionCF A f mf ay supf0 x) (& w)
-                         zc35 = subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt 
+                     zc34 {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt) 
+                     ... | case1 lt = SUP.x<sup zc32 lt 
+                     ... | case2 P = ?
+                     --  FClosure A f px z
+                     -- where
+                     --    zc35 : odef (UnionCF A f mf ay supf0 x) (& w)
+                     --     zc35 = 
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
                  sup=u : {b : Ordinal} (ab : odef A b) →