# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662406719 -32400
# Node ID 2569ace27176757dd19d92659188d7f0cf23669e
# Parent  a28bb57c88e60320b01aa119d63d7404a5e9b8e4
...

diff -r a28bb57c88e6 -r 2569ace27176 src/zorn.agda
--- a/src/zorn.agda	Tue Sep 06 01:18:54 2022 +0900
+++ b/src/zorn.agda	Tue Sep 06 04:38:39 2022 +0900
@@ -915,8 +915,16 @@
                          , 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
+                           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 = ?
+                           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 = ?
+                           ... | 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
                            zc07 : FClosure A f (supf0 u)  (supf0 px)
                            zc07 = fc
                      zc05 | case1 b≤px with ZChain.csupf zc b≤px 
@@ -924,8 +932,16 @@
                          , 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
+                           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 = ?
+                           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 = ?
+                           ... | 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
                            zc07 : FClosure A f (supf0 u)  (supf0 b)
                            zc07 = fc
                  sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px z ≡ & (SUP.sup (sup z≤x))