# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659264340 -32400
# Node ID 460df9965d631d176dde7f0734764318964a0a74
# Parent  10a036aeb6884266a0e339da9b90b07950957e01
...

diff -r 10a036aeb688 -r 460df9965d63 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 31 17:57:15 2022 +0900
+++ b/src/zorn.agda	Sun Jul 31 19:45:40 2022 +0900
@@ -265,8 +265,6 @@
       sup : HOD
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
-      min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) ) 
-          → (z ≡ sup ) ∨ (sup < z )  
 
 --
 --  sup and its fclosure is in a chain HOD
@@ -314,11 +312,6 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
-      sup : SUP A chain
-      supf=sup : supf z ≡ & (SUP.sup sup)
-
-      supf-mono : { a b : Ordinal } → a o< b → supf a o≤ supf b
-      csupf : (z : Ordinal ) → odef chain (supf z) 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
       order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
@@ -724,16 +717,11 @@
 
           supf0 = ZChain.supf zc
 
-          csupf : (z : Ordinal) → odef (UnionCF A f mf ay supf0 x) (supf0 z)
-          csupf z with ZChain.csupf zc z
-          ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-          ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ 
-
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} ; supf-mono = ZChain.supf-mono zc
+               ; initial = pinit ; chain∋init = pcy  ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
@@ -799,38 +787,30 @@
           order :  {b sup1 z1 : Ordinal} → b o< x →
             psupf sup1 o< psupf b →
             FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b)
-          order {b} {s} {z1}  b<x ps<pb fc = ? where
-                bzc = pzc (osuc b) (ob<x lim b<x)
-                Sb : SUP A ?
-                Sb = ZChain.sup bzc
-                sb = & (SUP.sup (ZChain.sup bzc))
-                zc21 : ZChain.supf bzc (osuc b) ≡ sb
-                zc21 = ZChain.supf=sup bzc
-                zc22 :  {z : HOD} → UnionCF A f mf ay (ZChain.supf bzc) (osuc b) ∋ z 
-                    → (z ≡ SUP.sup (ZChain.sup bzc)) ∨ (z < SUP.sup (ZChain.sup bzc))
-                zc22 = SUP.x<sup (ZChain.sup bzc)
-                zc23 = SUP.min-sup (ZChain.sup bzc)
+          order {b} {s} {z1}  b<x ps<pb fc with trio< b x
+          ... | tri< a ¬b ¬c = ZChain.order uzc <-osuc zc21 zc20 where
+               uzc = pzc (osuc b) (ob<x lim a)
+               zc22 : psupf s ≡ ZChain.supf uzc s 
+               zc22 with trio< s x
+               ... | tri< s<x ¬b ¬c = zc23 where
+                   szc = pzc (osuc s) (ob<x lim s<x)
+                   zc23 :  ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s
+                   zc23 = ?
+               ... | tri≈ ¬a b ¬c = ?
+               ... | tri> ¬a ¬b c = ?
+               zc21 :  ZChain.supf uzc s o< ZChain.supf uzc b
+               zc21 = subst (λ k → k o< _) zc22 ps<pb
+               zc20 : FClosure A f (ZChain.supf uzc s ) z1
+               zc20 = subst (λ k → FClosure A f k z1) zc22 fc
+          ... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x)
+          ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x)
 
-          csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
-          csupf z with trio< z x | inspect psupf z
-          ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
-                ozc = pzc (osuc z) (ob<x lim z<x)
-                zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
-                zc12  = ZChain.csupf ozc z
-                zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) ⟫ where
-                      az : odef A ( ZChain.supf ozc z )
-                      az = proj1 zc12
-                      zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
-                      zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
-                      ... | case1 eq = case1 (trans eq (sym eq1) )
-                      ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
-                      cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
-                      cp1 = record {  fcy<sup = zc20   ; order = order z<x  }
-                     ---  u = supf u = supf z 
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
-                sa = SUP.A∋maximal usup
-          ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
+          fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u)
+          fcy<sup {u} {w} u<x fc with trio< u x 
+          ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
+               uzc = pzc (osuc u) (ob<x lim a)
+          ... | tri≈ ¬a b ¬c = ⊥-elim (¬a u<x)
+          ... | tri> ¬a ¬b c = ⊥-elim (¬a u<x)
 
           pchain : HOD
           pchain = UnionCF A f mf ay psupf x
@@ -864,7 +844,7 @@
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
 
           no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!}
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!} ; order = order ; fcy<sup = fcy<sup
               ; supf-mono = {!!} ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)