# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657542409 -32400
# Node ID 0e28091e9271d2dec7b2c5861f47b2cb1bd2dfac
# Parent  7c0bb8ed7193eed130a7cbff7ac659ec4560be08
...

diff -r 7c0bb8ed7193 -r 0e28091e9271 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 11 16:46:18 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 21:26:49 2022 +0900
@@ -531,7 +531,11 @@
          → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
      ind f mf {y} ay x zc0 prev with trio< o∅ x
      ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
-     ... | tri≈ ¬a x=0 ¬c = ?
+     ... | tri≈ ¬a refl ¬c = record { initial = initial1 } where
+          initial1 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)) z → * y ≤ * z 
+          initial1 {z} uz = ? where
+             zc01 : odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z
+             zc01 = uz
      ... | tri< 0<x ¬b ¬c with Oprev-p x
      ... | yes op = {!!} where
           --
@@ -546,10 +550,10 @@
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain {!!}) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain {!!} ) ab →
+          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain zc ) ab →
                             * a < * b → odef (ZChain.chain zc ) b ) → ZChain A f mf ay zc0 x
-          no-extenion is-max = {!!} 
+          no-extenion is-max  = record { initial = ZChain.initial zc ; chain∋init = ZChain.chain∋init zc }
 
           zc4 : ZChain A f mf ay zc0 x 
           zc4 with o≤? x o∅
@@ -570,8 +574,8 @@
                             HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
                             * a < * b → odef (ZChain.chain zc ) b
                 zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max zc za {!!} ab P a<b
-                ... | case1 b=x = {!!} -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
+                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
+                ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}