# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651114038 -32400
# Node ID f007e044b2c66cf31fabf60d3694412934c23e1f
# Parent  5ad7a31df4f4dd7ffc4b50f755e9dba35382f49f
...

diff -r 5ad7a31df4f4 -r f007e044b2c6 src/zorn.agda
--- a/src/zorn.agda	Thu Apr 28 10:29:47 2022 +0900
+++ b/src/zorn.agda	Thu Apr 28 11:47:18 2022 +0900
@@ -340,41 +340,30 @@
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
-          ... | yes ax with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ay f )
-          ... | case1 pr = zc7 where -- we have previous <
+          ... | yes ax with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO px
+          ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+                zc9 :  ZChain A ay f mf supO x
+                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
                 ay0 : odef A (& (* y))
                 ay0 = (subst (λ k → odef A k ) (sym &iso) ay )
                 Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x)
                 Afx {x} ax = (subst (λ k → odef A k ) (sym &iso) (proj2 (mf x (subst (λ k → odef A k ) &iso ax))))
                 chain = ZChain.chain zc0
                 zc7 :  ZChain A ay f mf supO x
-                zc7 with ODC.∋-p O  (ZChain.chain zc0) (* ( f y ) )
-                ... | yes pr = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = z22
-                         ; is-max = {!!} }  where -- no extention
-                    z22 : odef (ZChain.chain zc0) y  --   y ≡ f pr , chain ∋ f y ≡ f (f pr)
-                    z22 = {!!}
-                    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 = {!!}
-                    ... | tri> ¬a ¬b c = {!!}
-                    z21 :  {a : Ordinal} → odef (ZChain.chain zc0) a → a o< x → odef (ZChain.chain zc0) (f a)
-                    z21 {a} za a<x with trio< a x
-                    ... | tri< a₁ ¬b ¬c = ZChain.f-next zc0 za 
-                    ... | tri≈ ¬a b ¬c = {!!}
-                    ... | tri> ¬a ¬b c = ⊥-elim ( o<> c a<x )
-                ... | no not = record { chain = zc5 ; chain⊆A =  ⊆-zc5
-                    ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x  = case1 {!!} ; ¬chain∋x>z = {!!} ; is-max = {!!} } where
-                --   extend with f x -- cahin ∋ y ∧  chain ∋ f y ∧ x ≡ f ( f y )
+                zc7 with trio< (Prev<.y pr) x
+                ... | tri< a ¬b ¬c = {!!} --  already x ∈ chain because of is-max
+                ... | tri≈ ¬a b ¬c = {!!} --  x ≡ z ∈ chain
+                ... | tri> ¬a ¬b x<z = record { chain = zc5 ; chain⊆A =  ⊆-zc5    ---   
+                    ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x  = case1 {!!} ; is-max = {!!} } where
+                --   extend with x ≡ f z where cahin ∋ z 
                     zc5 : HOD
-                    zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f y) } ; odmax = & A ; <odmax = {!!} }
+                    zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} }
                     ⊆-zc5 : zc5 ⊆ A 
                     ⊆-zc5 = record { incl = λ {y} lt → zc15 lt } where
-                        zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f y) ) → odef A z
+                        zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f x) ) → odef A z
                         zc15 {z} (case1 zz) = subst (λ k → odef A k ) &iso ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain  k ) (sym &iso) zz ) )
-                        zc15 (case2 refl) = proj2 ( mf y (subst (λ k → odef A k ) &iso {!!} ) )
+                        zc15 (case2 refl) = proj2 ( mf x (subst (λ k → odef A k ) &iso {!!} ) )
                     IPO = ⊆-IsPartialOrderSet  ⊆-zc5 PO
                     zc8 : { A B x : HOD } → (ax : A ∋ x ) → (P : Prev< A B ax f ) → * (f (& (* (Prev<.y P)))) ≡ x
                     zc8 {A} {B} {x} ax P = subst₂ (λ j k → * ( f j ) ≡ k ) (sym &iso) *iso (sym (cong (*) ( Prev<.x=fy P)))
@@ -399,19 +388,18 @@
                          zc10 : * y ≡ b
                          zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ay {!!} ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) 
                          zc11 : * (f y) ≡ a
-                         zc11 = subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym fx))
+                         zc11 = subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym {!!} ))
                          zc12 : odef chain y
                          zc12 = subst (λ k → odef chain k ) (subst (λ k → & b ≡ k ) &iso (sym (cong (&) zc10)))  c 
                     ... | tri> ¬a ¬b c₁ = {!!}
                     zc6 : IsTotalOrderSet zc5
                     zc6 =  record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}
                         ; compare = cmp }
-          ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) ))
-          ... | case1 pr = {!!} -- x is sup
-          ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
+          ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) ))
+          ... | case1 x=sup = {!!} -- x is sup
+          ... | case2 ¬x=sup = 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
-     ... | no noapx = {!!} -- we have previous ordinal but ¬ A ∋ op
-     ind f mf x prev ya | no ¬ox with trio< (& A) x   --- limit ordinal case
+     ... | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = {!!} where
           zc0 = prev (& A) a
      ... | tri≈ ¬a b ¬c = {!!}