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

diff -r f48c9f4bafdb -r 5f329a1c1d09 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 13 09:22:14 2022 +0900
+++ b/src/zorn.agda	Mon Jun 13 10:47:53 2022 +0900
@@ -243,18 +243,12 @@
 record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p : Ordinal)   ( x : Ordinal ) : Set n where
    field
       ax : odef A x
-      fc∨sup :  FClosure A f p x ∨ ((a : Ordinal) → FClosure A f p a → a << x )
-      -- f-min : (x1 : Ordinal) → ( (a : Ordinal) → FClosure A f p a → a << x1 ) → x o≤ x1
-
-FCSet :  (A : HOD) → ( f : Ordinal → Ordinal ) → (sup : Ordinal) → HOD
-FCSet A f sup = record { od = record { def = λ x → FChain A f sup x } ; odmax = & A ; <odmax = fcs00 }
-   where
-     fcs00 :   {y : Ordinal} →  FChain A f sup y → y o< & A
-     fcs00  {y} fc = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (FChain.ax fc )))
+      fc∨sup :  FClosure A f p x ∨ ((a : Ordinal) → FClosure A f p a → (a ≡ x) ∨ (a << x) )
+      f-min : (x1 : Ordinal) → ( (a : Ordinal) → FClosure A f p a → (a ≡ x1 ) ∨ (a << x1) ) → FClosure A f p x1 ∨ ( x o≤ x1 )
 
 data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where
-      Finit :  {z : Ordinal} → z ≡ (& (* y , * y))  → Fc∨sup A ay f z
-      Fc  :  {x : Ordinal} → (fc : Fc∨sup A ay f x ) →  Fc∨sup A ay f (& (FCSet A f x))
+      Finit :  {z : Ordinal} → z ≡ y  → Fc∨sup A ay f z
+      Fc  :  {p x : Ordinal} → Fc∨sup A ay f p  → FChain A f p x →  Fc∨sup A ay f x
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -268,7 +262,7 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      fc∨sup :  {s c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A ca) f s ∧ odef (* s) c
+      fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f c 
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -597,11 +591,31 @@
                  → ((c : Ordinal) → c o< a →  c o< b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
                  → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb
             uind a previ a<b za zb {i} zai = um01 where
-                FC : Fc∨sup A (chain⊆A za zai) f i ∧ odef {!!} i
+                FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i 
                 FC = fc∨sup za zai 
                 um01 : odef (chain zb) i
                 um01 with FC
-                ... | t = {!!}
+                ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
+                ... | Fc {p} {x1} pFC fc with initial za zai
+                ... | case1 y=i = subst (λ k → odef (chain zb) k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=i)) ( chain∋x zb )
+                ... | case2 y<i = is-max zb {y} {i} (chain∋x zb) i<b (chain⊆A za zai) um05 y<i
+                  where
+                    i<b : i o< osuc b
+                    i<b = {!!}
+                    um05 : HasPrev A (chain zb) (chain⊆A za zai) f ∨ IsSup A (chain zb) (chain⊆A za zai)
+                    um05 with FChain.fc∨sup fc
+                    ... | case1 (init {p} ap i=p) = case2 {!!}
+                    ... | case1 (fsuc p pfci) = case1 record { y = p ; ay = um07 ; x=fy = refl }  where
+                        -- p should be the top of fc
+                        p<a : p o< a
+                        p<a = {!!}
+                        um08 : odef (chain (prev p {!!} ay)) p
+                        um08 = {!!}
+                        um07 : odef (chain zb) p
+                        um07 = previ p p<a {!!} (prev p {!!} ay )  zb um08 
+                    ... | case2 supi = case2 record { x<sup = um06 supi } where
+                        um06 : ((z : Ordinal) → FClosure A f p z → (z ≡ i) ∨ (z << i) ) → {w : Ordinal} → odef (chain zb) w → (w ≡ i) ∨ (w << i)
+                        um06 supi = {!!}
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux