# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656297351 -32400
# Node ID ce4dbd14cf441d7039ab4069a48389f240d0940a
# Parent  3821048a85524735d017e21dd4dd657da8a90447
...

diff -r 3821048a8552 -r ce4dbd14cf44 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 27 11:11:56 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 11:35:51 2022 +0900
@@ -244,6 +244,14 @@
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
 
+record UZFChain ( A : HOD )  ( f : Ordinal → Ordinal ) (x y  : Ordinal) (prev : (z : Ordinal) → z o< x → ZChain A y f z) (z : Ordinal) : Set n where 
+   -- Union of ZFChain from y which has maximality o< x
+   inductive
+   field
+      u : Ordinal
+      u<x : u o< x
+      chain∋z : odef (ZChain.chain (prev u u<x  )) z
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -528,19 +536,13 @@
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
      ... | no ¬ox = record { chain⊆A = Uz⊆A ; f-next = u-next ; chain = Uz
                      ; initial = u-initial ; chain∋x  = u-chain∋x ; is-max = {!!} }   where --- limit ordinal case
-         record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
-            inductive
-            field
-               u : Ordinal
-               u<x : u o< x
-               chain∋z : odef (ZChain.chain (prev u u<x  )) z
-         Uz⊆A : {z : Ordinal} → UZFChain z ∨ FClosure A f y z → odef A z
+         Uz⊆A : {z : Ordinal} → UZFChain A f x y prev z ∨ FClosure A f y z → odef A z
          Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
          Uz⊆A (case2 lt) = A∋fc _ f mf lt 
-         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
+         uzc : {z : Ordinal} → (u : UZFChain A f x y prev z) → ZChain A y f (UZFChain.u u)
          uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) 
          Uz : HOD
-         Uz = record { od = record { def = λ z → UZFChain z ∨ FClosure A f y z } ; odmax = & A
+         Uz = record { od = record { def = λ z → UZFChain A f x y prev z ∨ FClosure A f y z } ; odmax = & A
              ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
          u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
          u-next {z} (case1 u) = case1 record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
@@ -573,9 +575,15 @@
              zc0 = ind f mf ay px (λ w w<px → zc zc1 (o<→≤ w<px) )
              px<x : px o< x
              px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
+             no-extrention1 : ( {a b : Ordinal} → odef (chain zc0) a → b o< osuc x → (ab : odef A b) →
+                     HasPrev A (chain zc0) ab f ∨  IsSup A (chain zc0) ab →
+                             * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 y f x
+             no-extrention1 imx = record { zc = sz00  ; chain-mono = ? ; f-total = ?  } where
+                  sz00 : {z : Ordinal} → z o≤ x → ZChain A y f z 
+                  sz00 {z} z≤x = ?
              sz02 : ZChain1 y f x
              sz02 with ODC.∋-p O A (* x)
-             ... | no noax = record { zc = ? ;  chain-mono = ? ; f-total = ? }
+             ... | no noax = no-extrention1 ?
              ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain zc0) ax f ) 
              ... | case1 pr = record { zc = ? ;  chain-mono = ? ; f-total = ? } where
              ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain zc0) ax )
@@ -597,10 +605,11 @@
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
              ... | case2 ¬x=sup =  ?
-         ... | no  ¬ox  with trio< x y
-         ... | tri< a ¬b ¬c = {!!}
-         ... | tri≈ ¬a b ¬c = {!!}
-         ... | tri> ¬a ¬b y<x = {!!}
+         ... | no  ¬ox  = record { zc = zcu ; chain-mono = sz03 ; f-total = ? } where
+              zcu : { z : Ordinal } → z o≤ x → ZChain A y f z
+              zcu = ?
+              sz03 : {a b : Ordinal} → (a≤b : a o≤ b) → (b≤x : b o≤ x ) →  chain (zcu {a} (OrdTrans a≤b b≤x))  ⊆' chain (zcu b≤x ) 
+              sz03 = ?
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM