# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656314799 -32400
# Node ID 3f0963e1c79f76b629812661701cf38196e61696
# Parent  ce4dbd14cf441d7039ab4069a48389f240d0940a
...

diff -r ce4dbd14cf44 -r 3f0963e1c79f src/zorn.agda
--- a/src/zorn.agda	Mon Jun 27 11:35:51 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 16:26:39 2022 +0900
@@ -606,8 +606,22 @@
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
              ... | case2 ¬x=sup =  ?
          ... | no  ¬ox  = record { zc = zcu ; chain-mono = sz03 ; f-total = ? } where
+              pzc :  (z : Ordinal) → z o< x → ZChain A y f z
+              pzc z z<x = ind f mf ay z (λ w w<px → zc (prev z z<x) (o<→≤ w<px) )
+              Uz⊆A : {z : Ordinal} → UZFChain A f x y pzc z ∨ FClosure A f y z → odef A z
+              Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( pzc (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
+              Uz⊆A (case2 lt) = A∋fc _ f mf lt 
+              uzc : {z : Ordinal} → (u : UZFChain A f x y pzc z) → ZChain A y f (UZFChain.u u)
+              uzc {z} u =  pzc (UZFChain.u u) (UZFChain.u<x u) 
+              Uz : HOD
+              Uz = record { od = record { def = λ z → UZFChain A f x y pzc z ∨ FClosure A f y z } ; odmax = & A
+                 ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
+              zcu1 : { z : Ordinal } → z o≤ x → ZChain1 y f z
+              zcu1 {z} z≤x with  osuc-≡< z≤x
+              ... | case1 z=x = record { zc = ? ; chain-mono = ? ; f-total = ? }
+              ... | case2 z<x = prev z z<x 
               zcu : { z : Ordinal } → z o≤ x → ZChain A y f z
-              zcu = ?
+              zcu {z} z≤x = ind f mf ay z (λ w w<px → zc (zcu1 z≤x ) (o<→≤ w<px) )
               sz03 : {a b : Ordinal} → (a≤b : a o≤ b) → (b≤x : b o≤ x ) →  chain (zcu {a} (OrdTrans a≤b b≤x))  ⊆' chain (zcu b≤x ) 
               sz03 = ?