# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659777893 -32400
# Node ID 9cf74877efab99c5acaba1b755d16a87c8a3bdd8
# Parent  3a8493e6cd675ee054ee131dde5cee8004cb3c21
...

diff -r 3a8493e6cd67 -r 9cf74877efab src/zorn.agda
--- a/src/zorn.agda	Sat Aug 06 15:06:58 2022 +0900
+++ b/src/zorn.agda	Sat Aug 06 18:24:53 2022 +0900
@@ -228,33 +228,52 @@
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
       supf≤x :{x : Ordinal } → z o≤ x → supf z ≡  supf x
+
+   fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
+   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+       , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
+   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
+
    supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
-   supf-mono {x} {y} x<y = ? where
+   supf-mono {x} {y} x<y = sf<sy where
+      --     supf x <<  supf y →   supf x o< supf y
+      --     x o<  y →   supf x <= supf y
       --   z o≤ x → supf x ≡ supf y ≡ supf z
       --   x o< z → z o< y → supf x ≡ supf y ≡ supf z
       sf<sy : supf x o≤ supf y
       sf<sy with trio< x z
       ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y ) <-osuc ) ) )) 
       ... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y) b (o<→≤ x<y)))) 
-      ... | tri< x<z ¬b ¬c with trio< y z
-      ... | tri> ¬a ¬b c = ?
+      ... | tri< x<z ¬b ¬c with trio< (supf x) (supf y)
+      ... | tri< a ¬b ¬c = o<→≤ a
+      ... | tri≈ ¬a b ¬c = o≤-refl0 b
+      ... | tri> ¬a ¬b sy<sx with trio< z y
+      ... | tri< a ¬b ¬c = ?
       ... | tri≈ ¬a b ¬c = ?
-      ... | tri< y<z ¬b ¬c with csupf (o<→≤ x<z) | csupf (o<→≤ y<z)
-      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫  = ?
-      ... | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫  = ?
-      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
-      ... | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+      ... | tri> ¬a ¬b y<z = ?
+      zc04 : x o< z → y o< z → supf x o≤ supf y
+      zc04 x<z y<z with csupf (o<→≤ x<z) | csupf (o<→≤ y<z) 
+      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy
+      ... | case1 eq = o≤-refl0 (sym eq)
+      ... | case2 lt with fcy<sup y<z fcx
+      ... | case1 eq = o≤-refl0 eq
+      ... | case2 lt1 = ⊥-elim ( <-irr (case2 lt) lt1 )
+      zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy
+      ... | case1 eq = o≤-refl0 (sym eq)
+      ... | case2 lt with ChainP.fcy<sup is-sup-x fcy 
+      ... | case1 eq with s≤fc (supf ux) f mf fcx 
+      ... | case1 eq1 = o≤-refl0 ( trans ( subst₂ (λ j k → j ≡ k ) &iso &iso (sym (cong (&) eq1))) (sym eq) )
+      ... | case2 lt1 = ?    --  ux << sx, sy << sx
+      zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ | case2 lt1 = ? -- sy << sx
+      zc04 x<z y<z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ? 
+      zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
       -- ... | tri< a ¬b ¬c = csupf (o<→≤ a)
       -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b)
       -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay supf x) k ) ? (csupf ? )
       -- csy : odef (UnionCF A f mf ay supf y) (supf y) 
       -- csy = csupf ?
        
-   fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
-   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
-       , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
    order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z sf<sb fc = zc04 where
       zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1