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

diff -r 379bd9b4610c -r 5ad7a31df4f4 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 27 23:21:21 2022 +0900
+++ b/src/zorn.agda	Thu Apr 28 10:29:47 2022 +0900
@@ -200,7 +200,7 @@
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → 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 ) →  a o< z  → (ba : odef A b) 
+      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< z  → (ba : odef A b) 
           → Prev< A chain ba f
                ∨  (sup (& chain) (subst (λ k → k  ⊆ A) (sym *iso) chain⊆A)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b )
           → * a < * b  → odef chain b
@@ -277,7 +277,7 @@
      z03 f mf zc = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → a o< & A → (ab : odef A b ) 
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
               →  Prev< A chain ab f
                    ∨  (supO (& chain) (subst (λ k → k  ⊆ A) (sym *iso) (ZChain.chain⊆A zc))  (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b )
               → * a < * b  → odef chain b
@@ -287,7 +287,7 @@
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) s<A (SUP.A∋maximal sp1)  (case2 refl ) z13 where
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) z11 (SUP.A∋maximal sp1)  (case2 refl ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc ))
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
@@ -315,13 +315,14 @@
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
-     premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 :  ZChain A sa f mf supO y ) 
-        → {a b : Ordinal} (ca : odef (ZChain.chain zc0) a) → (ab : odef A b) → a o< y
-        →  Prev< A (ZChain.chain zc0) ab f ∨ (supO (& (ZChain.chain zc0))
-             (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
-             (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b)
-       → * a < * b → odef (ZChain.chain zc0) b
-     premax {x} {y} y<x  f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca a<y ab P a<b -- ca ab y P a<b
+
+     3cases : {x y : Ordinal} → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )
+        → (ax : odef A x )→ (ay : odef A y )
+        → (zc0 :  ZChain A ay f mf supO x ) 
+        →  Prev< A (ZChain.chain zc0) ax f
+           ∨  (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ x)
+           ∨ ( ( z : Ordinal) → odef (ZChain.chain zc0) z → ¬ ( * z < * x ))
+     3cases {x} {y} f mf ax ay zc0 = {!!}
      -- Union of ZFChain
      UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) 
             → ( (z : Ordinal) → z o< B → {y : Ordinal} →  (ya : odef A y) → ZChain A ya f mf supO z ) → HOD
@@ -331,32 +332,28 @@
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
             ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → { y : Ordinal } → (ya : odef A y) → ZChain A ya f mf supO x
      ind f mf x prev {y} ay with Oprev-p x
-     ... | yes op with ODC.∋-p O A (* (Oprev.oprev op))
-     ... | yes apx = zc4 where -- we have previous ordinal and A ∋ op
+     ... | yes op = zc4 where
           px = Oprev.oprev op
-          apx0 = subst (λ k → odef A k ) &iso apx 
           zc0 : ZChain A ay f mf supO (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
-          zc1 : {y : Ordinal } → (ay : odef A y ) → ZChain A ay f mf supO (Oprev.oprev op)
-          zc1 {y} ay = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
-          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))))
-          --   x is in the previous chain, use the same
-          --   x has some y which y < x ∧ f y ≡ x
-          --   x has no y which y < x 
           zc4 : ZChain A ay f mf supO x 
-          zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ay f )
+          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 <
+                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 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  =  {!!} -- ZChain.chain∋x zc0
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = z22
                          ; is-max = {!!} }  where -- no extention
-                    z22 : {a : Ordinal} → x o< osuc a → ¬ odef (ZChain.chain zc0) a
-                    z22 {a} x<oa = {!!}
+                    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