# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658192519 -32400
# Node ID 753780183ddf18c3db234d277aca7b234389e0d1
# Parent  15f3bcc4ae3f7a5f312a7f22465675299b41b78f
...

diff -r 15f3bcc4ae3f -r 753780183ddf src/zorn.agda
--- a/src/zorn.agda	Tue Jul 19 09:36:02 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 10:01:59 2022 +0900
@@ -435,21 +435,23 @@
      SZ1 :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
      SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
+        chain-mono2 : (x : Ordinal) {a b c : Ordinal} → a o≤ b → b o≤ x →
+            odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
+        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c fc } ⟫ = 
+                ⟪ ua , record { u = _ ; u<x = case2 refl  ; uchain = ch-init c fc } ⟫ 
+        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
+                ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫ 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
-        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 } where
+        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x } where
            px = Oprev.oprev op
-           chain-mono2 :  {a b c : Ordinal} → a o≤ b → b o≤ x →
-                odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
-           chain-mono2 {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c x } ⟫ = 
-                    ⟪ ua , record { u = _ ; u<x = case2 refl  ; uchain = ch-init c x } ⟫ 
-           chain-mono2 {a} {b} {c} a≤b b≤x ⟪ ua , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
-                    ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫ 
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-           is-max {a} {b} ua b<x ab (case1 has-prev) a<b = {!!}
+           is-max {a} {b} ua b<x ab (case1 has-prev) a<b = m04 where
+                 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+                 m04 = ?
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
            ... | case1 has-prev = m04 where
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
@@ -463,7 +465,7 @@
                      ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } = 
                           ch-init (f (HasPrev.y has-prev)) (fsuc _ fc) 
                      ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc) 
-           ... | case2  ¬fy<x  = {!!} where
+           ... | case2  ¬fy<x  = m01 where
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
                  m01 with trio< px b
                  ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px {!!}) {!!} {!!} m04 where
@@ -471,7 +473,14 @@
                     m04 = ZChain1.is-max (prev px {!!}) {!!} {!!} ab {!!} a<b
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
-        ... | no lim = record { is-max = {!!} ; chain-mono2 = {!!} ; chain≤x = {!!} } 
+        ... | no lim = record { is-max = {!!} ; chain-mono2 = chain-mono2 x  }  where
+           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
+              b o< x → (ab : odef A b) →
+              HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
+              * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+           is-max {a} {b} ua b<x ab (case1 has-prev) a<b = ?
+           is-max {a} {b} ua b<x ab (case2 is-sup) a<b = ?
+           --- with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
            --- m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
            --- m04 = ZChain1.is-max (prev (osuc b) {!!} ) {!!} <-osuc ab {!!} a<b