# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655129468 -32400
# Node ID 96f377d87427e9cbf014e9cd3930c0421f2d7d88
# Parent  4af13e0001282953185d9dc3888afe18883fb143
...

diff -r 4af13e000128 -r 96f377d87427 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 13 16:14:55 2022 +0900
+++ b/src/zorn.agda	Mon Jun 13 23:11:08 2022 +0900
@@ -248,7 +248,7 @@
 
 data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where
       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
+      Fc  :  {p x : Ordinal} → p o< x → 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
@@ -264,6 +264,7 @@
           → * a < * b  → odef chain b
       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
       maximal : HOD
@@ -593,29 +594,22 @@
             uind a previ a<b za zb {i} zai = um01 where
                 FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i 
                 FC = fc∨sup za zai 
+                FCb : Fc∨sup A (chain⊆A zb (chain∋x zb)) f i 
+                FCb =  {!!}
                 um01 : odef (chain zb) i
                 um01 with FC
                 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
-                ... | Fc {p} {i} pFC fc with initial za zai
+                ... | Fc {p} {i} p<i 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 with FChain.fc∨sup fc 
-                ... | case1 fci  = um10 i p y<i fci where
-                     um10 : (i p : Ordinal) → y << i → FClosure A f p i → odef (chain zb) i
-                     um10 i p y<i (init {q} ap q=p) = um02 where
-                        q<a : q o< a
-                        q<a = {!!}
-                        um03 : odef (chain (prev q (ordtrans q<a (ordtrans a<b b<x)) ay)) q
-                        um03 = ?
-                        um02 : odef (chain zb) q
-                        um02 = previ a {!!} {!!} za zb ?
-                     um10 i p y<i (fsuc j pfci) = f-next zb (um10 j p y<j pfci)  where
-                        y<j : y << j
-                        y<j = {!!}
-                ... | case2 supi = um06 supi where
-                        um05 : FChain A f p i
-                        um05 = fc 
-                        um06 : ((z : Ordinal) → FClosure A f p z → (z ≡ i) ∨ (z << i) ) → odef (chain zb) i
-                        um06 supi = {!!}
+                ... | case2 y<i with (FChain.fc∨sup fc) 
+                ... | case1 fc = um02 i fc where
+                     um02 : (i : Ordinal) → FClosure A f p i → odef (chain zb) i
+                     um02 i (init ap i=p ) = {!!}
+                     um02 i (fsuc j fc) = f-next zb ( um02 j fc )
+                ... | case2 sup = {!!}
+                -- is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} y<i where
+                --     pFC0 : Fc∨sup A (chain⊆A za (chain∋x za)) f p
+                --     pFC0 = pFC
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux