# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651004371 -32400
# Node ID 27bb51b7f012f615ac4a2a8f2f7670e92e30d6ff
# Parent  f0b45446c7ea00396ec174507ee1c5d0904f56ec
...

diff -r f0b45446c7ea -r 27bb51b7f012 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 27 04:04:30 2022 +0900
+++ b/src/zorn.agda	Wed Apr 27 05:19:31 2022 +0900
@@ -361,10 +361,19 @@
                 chain = ZChain.chain zc0
                 zc7 :  ZChain A sa f mf supO x
                 zc7 with ODC.∋-p O  (ZChain.chain zc0) (* ( f x ) )
-                ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
-                     ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
+                ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  zc20 (ZChain.f-next zc0)
+                     ; f-immediate =  ZChain.f-immediate zc0 ; ¬chain∋x>z = z22 ; chain∋x  =  ZChain.chain∋x zc0
+                     ; is-max = λ za ba a<x → zc20 (λ za a<x → ZChain.is-max zc0 za ba a<x ) za a<x  }  where -- no extention
+                    z22 : {a : Ordinal} → x o< osuc a → ¬ odef (ZChain.chain zc0) a
+                    z22 {a} x<oa = ZChain.¬chain∋x>z zc0 (ordtrans (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc ) x<oa )
+                    zc20 : {P : Ordinal →  Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a)
+                       → {a : Ordinal} → (za : odef (ZChain.chain zc0) a ) → (a<x : a o< x) →  P a
+                    zc20 {P} prev {a} za a<x with trio< a px
+                    ... | tri< a₁ ¬b ¬c = prev za a₁
+                    ... | tri≈ ¬a b ¬c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (subst (λ k → k o< osuc a) b <-osuc ) za )
+                    ... | tri> ¬a ¬b c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (ordtrans c <-osuc ) za )
                 ... | no not = record { chain = zc5 ; chain⊆A =  ⊆-zc5
-                    ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where
+                    ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; ¬chain∋x>z = {!!} ; is-max = {!!} } where
                 --   extend with f x -- cahin ∋ y ∧  chain ∋ f y ∧ x ≡ f ( f y )
                     zc5 : HOD
                     zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} }