# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650785601 -32400
# Node ID adbac273d2a65be0a46780a805353c9c31b8e471
# Parent  854908eb70f252f9e83153bec0a35fd1f4e156e1
...

diff -r 854908eb70f2 -r adbac273d2a6 src/zorn.agda
--- a/src/zorn.agda	Sun Apr 24 14:10:06 2022 +0900
+++ b/src/zorn.agda	Sun Apr 24 16:33:21 2022 +0900
@@ -288,8 +288,6 @@
                ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               c1 : SUP.sup sp1 < * (f ( & ( SUP.sup sp1 ))) 
-               c1 = c
                z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
                z15  = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso)  (ZChain.f-next zc z12) )
                z17 : ⊥
@@ -314,7 +312,8 @@
           zc0 : ZChain A sa f mf supO (Oprev.oprev op) 
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
           zc1 : ZChain A sa f mf supO x 
-          zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; is-max = {!!} }
+          zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
+             ; chain∋x  = {!!} ; is-max = {!!} }
      ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
           zc0 : ZChain A sa f mf supO (Oprev.oprev op) 
@@ -323,10 +322,16 @@
           --   x has some y which y < x ∧ f y ≡ x
           --   x has no y which y < x 
           zc4 : ZChain A sa f mf supO x
-          zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; is-max = {!!} }
+          zc4 with ODC.p∨¬p O ( Prev< A ax f )
+          ... | case1 y = record { chain = zc5 ; chain⊆A = record { incl = λ lt → proj1 lt  }
+                    ; f-total = {!!} ; f-next = {!!} ; chain∋x  = ⟪ subst (λ k → odef A (& k)) *iso sa , case1 (ZChain.chain∋x zc0)  ⟫ ; is-max = {!!} } where
+                zc5 : HOD
+                zc5 = record { od = record { def = λ z → odef A z ∧ (odef (ZChain.chain zc0) z ∨ (z ≡ x) ∨ (z ≡ f x)) } ; odmax = & A ; <odmax = z07 }
+          ... | case2 not = {!!}
+          --  zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; chain∋x  = {!!} ; is-max = {!!} }
      ind f mf x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
-              ; is-max = {!!} } where
+              ; chain∋x  = {!!}  ; is-max = {!!} } where
           zc0 = prev (& A) a
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = {!!}