# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650957030 -32400
# Node ID 3826221c61a65f1ed42025073101e8f32e7be36f
# Parent  f3e2cbd07e7c4af8ad0d46ae02cc37a9d776b1ba
...

diff -r f3e2cbd07e7c -r 3826221c61a6 src/zorn.agda
--- a/src/zorn.agda	Mon Apr 25 17:51:24 2022 +0900
+++ b/src/zorn.agda	Tue Apr 26 16:10:30 2022 +0900
@@ -199,7 +199,7 @@
       chain⊆A : chain ⊆ A
       chain∋x : odef chain x
       f-total : IsTotalOrderSet chain 
-      f-next : {a : Ordinal } → odef chain a → odef chain (f a)
+      f-next : {a : Ordinal } → odef chain a → a o< z  → odef chain (f a)
       f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
       is-max :  {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) → a o< z
           → Prev< A chain ba f
@@ -281,7 +281,7 @@
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12))) (me z12 )
+           z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 {!!} ))) (me z12 )
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
@@ -290,7 +290,7 @@
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
                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) )
+               z15  = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso)  (ZChain.f-next zc z12 {!!} ) )
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
@@ -324,7 +324,7 @@
           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 ; f-immediate = {!!}
+          zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!} ; f-immediate = {!!}
              ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }
      ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
@@ -335,37 +335,62 @@
           --   x has no y which y < x 
           zc4 : ZChain A sa f mf supO x
           zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f )
-          ... | case1 y = zc7 where
+          ... | case1 y = zc7 where -- we have previous <
                 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 = ZChain.f-next zc0 
+                ... | 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
                 ... | 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
-                --   extend with f x
+                --   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 = {!!} }
                     ⊆-zc5 : zc5 ⊆ A 
                     ⊆-zc5 = record { incl = λ lt → {!!} }
                     IPO = ⊆-IsPartialOrderSet  ⊆-zc5 PO
-                    fx>zc : ( z : Ordinal ) → odef (ZChain.chain zc0) z → * z < * ( f x )
-                    fx>zc = {!!}
+                    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)))
+                    fx=zc :  odef (ZChain.chain zc0) x → Tri  (* (f x) < * x ) (* (f x) ≡ * x) (* x < * (f x) )
+                    fx=zc  c with mf x (subst (λ k → odef A k) &iso  ax )
+                    ... | ⟪ case1 x=fx , afx ⟫ = tri≈ {!!} zc13 {!!} where
+                        zc13 : * (f x) ≡ * x
+                        zc13 = subst (λ k → k ≡ * x ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso))) (sym ( x=fx ))
+                    ... | ⟪ case2 x<fx , afx ⟫ = tri> {!!} {!!} zc14 where
+                        zc14 : * x < * (f x)
+                        zc14 = subst₂ (λ j k → j < k ) {!!} (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso ))) x<fx
                     cmp : Trichotomous _ _ 
                     cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } with aa | ab
                     ... | case1 x | case1 x₁ = IsStrictTotalOrder.compare (ZChain.f-total zc0) (me x) (me x₁)
-                    ... | case1 c | case2 fx = {!!}
-                    ... | case2 x | case1 x₁ = {!!}
-                    ... | case2 x | case2 x₁ = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) x) (sym (cong (*) x₁ ) ))) {!!}
+                    ... | case2 fx | case2 fx₁ = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) fx) (sym (cong (*) fx₁ ) ))) {!!}
+                    ... | case1 c | case2 fx = {!!} -- subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx>zc (subst (λ k → odef chain k) {!!} c ))
+                    ... | case2 fx | case1 c with ODC.p∨¬p O ( Prev< A chain (incl (ZChain.chain⊆A zc0) c) f )
+                    ... | case2 n = {!!}
+                    ... | case1 fb with IsStrictTotalOrder.compare (ZChain.f-total zc0) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay y))) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay fb)))
+                    ... | tri< a₁ ¬b ¬c = {!!}
+                    ... | tri≈ ¬a b₁ ¬c = subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx=zc (subst (λ k → odef chain k) {!!} c )) where
+                         zc11 : & a ≡ f x
+                         zc11 = fx 
+                         zc10 : * x ≡ b
+                         zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ax y ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) 
+                         zc12 : Tri (a < b) (a ≡ b) (b < a)
+                         zc12 with mf x (subst (λ k → odef A k) &iso  ax )
+                         ... | ⟪ case1 x=fx , afx ⟫ = tri≈ {!!} zc13 {!!} where
+                             zc13 : a ≡ b
+                             zc13 = subst₂ (λ j k → j ≡ k ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym zc11))) zc10 (sym ( x=fx ))
+                         ... | ⟪ case2 x<fx , afx ⟫ = tri> {!!} {!!} zc14 where
+                             zc14 : b < a
+                             zc14 = subst₂ (λ j k → j < k ) zc10 (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym zc11))) x<fx
+                    ... | 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 y = {!!}
-          ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 
+          ... | case1 y = {!!} -- x is sup
+          ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
                      ; f-immediate = {!!} ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }  -- no extention
      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
+     ... | tri< a ¬b ¬c = 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 = {!!} } where
           zc0 = prev (& A) a
      ... | tri≈ ¬a b ¬c = {!!}