# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661665578 -32400
# Node ID 710574600659a91f9e971ea06daa73a8f1d533a1
# Parent  1a5bb940fceb28ed9ace0af5c6a175abe62f7117
...

diff -r 1a5bb940fceb -r 710574600659 src/zorn.agda
--- a/src/zorn.agda	Sun Aug 28 09:15:52 2022 +0900
+++ b/src/zorn.agda	Sun Aug 28 14:46:18 2022 +0900
@@ -755,7 +755,11 @@
                           zc12 (fsuc x fc) with zc12 fc
                           ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                           ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
-                          zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu  , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) ? (init ? ? ) ⟫ 
+                          zc12 (init asu su=z ) with trio< u px
+                          ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu  , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) 
+                              record { fcy<sup = ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫ 
+                          ... | tri≈ ¬a b ¬c = ?
+                          ... | tri> ¬a ¬b c = ?
                      zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
                      zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                      zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where