# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660567157 -32400
# Node ID ae0f958e648bb710267b7f1ae726b8d6c56f076d
# Parent  ab5aa49abde0889d6fe3d692d4ae0a7226858231
...

diff -r ab5aa49abde0 -r ae0f958e648b src/zorn.agda
--- a/src/zorn.agda	Mon Aug 15 20:14:35 2022 +0900
+++ b/src/zorn.agda	Mon Aug 15 21:39:17 2022 +0900
@@ -714,14 +714,20 @@
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
                   order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
                     (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-                  order {s} {z2} s<u1 with trio< s px | inspect supf1 s
-                  ... | tri< a ¬b ¬c | record { eq = eq1 } = ?
-                  ... | tri≈ ¬a b ¬c | record{ eq = eq1 } = ?
-                  ... | tri> ¬a ¬b c | record{ eq = eq1 } = ?
+                  order {s} {z2} s<u1 fc with trio< s px 
+                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
                   fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
+                  order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
+                    (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
+                  order {s} {z2} s<u1 fc with trio< s px 
+                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
               ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px)
               ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
               ... | case2 lt = ⊥-elim ( o<> lt px<u1 )