# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665311441 -32400
# Node ID 49594badc9b42bd47a74e9d8eb0d2ec427caab4e
# Parent  6146d75131f51c55a2cbb89efb654b9a537fd4b7
...

diff -r 6146d75131f5 -r 49594badc9b4 src/zorn.agda
--- a/src/zorn.agda	Sun Oct 09 17:58:41 2022 +0900
+++ b/src/zorn.agda	Sun Oct 09 19:30:41 2022 +0900
@@ -828,20 +828,21 @@
                  --  supf1 x ≡ sp1, which is not included now
 
                  pchainpx : HOD
-                 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
-                      zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A
+                 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) 
+                       ∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
+                      zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A
                       zc00 {z} (case1 lt) = z07 lt 
-                      zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc )
-                 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z
+                      zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc )
+                 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → odef A z
                  zc01 {z} (case1 lt) = proj1 lt 
-                 zc01 {z} (case2 fc) = ( A∋fc px f mf fc )
+                 zc01 {z} (case2 fc) = ( A∋fc (supf0 px) f mf fc )
 
-                 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b
+                 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b
                  zc02 {a} {b} ca fb = zc05 fb where
                     zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
                     zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ?
-                    zc05 : {b : Ordinal } → FClosure A f px b → a <= b
-                    zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb ))
+                    zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b
+                    zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
                     ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
                     ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
                     zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? --
@@ -934,17 +935,21 @@
                          ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } 
 
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
-                 csupf1 {z1} sz1<x with trio< (supf0 z1) px
-                 ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) ? (sym (sf1=sf0 (o<→≤ a) )) (case1 (ZChain.csupf zc a )) where
-                        z1≤px : z1 o≤ px
-                        z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) ? a ))
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc21 , subst (λ k → z1 o< k ) (sym (Oprev.oprev=x op)) zc22 ⟫ ) where
-                      zc21 : px o< z1
-                      zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) ? c  )
-                      zc22 : z1 o< x -- c : px o< supf0 z1
-                      zc22 = ? -- supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )
-                     -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
+                 csupf1 {z1} sz1<x with trio< (supf1 z1) px
+                 ... | tri< a ¬b ¬c = csupf0 where
+                     zc18 : supf1 z1 ≡ supf0 z1
+                     zc18 = sf1=sf0 ?
+                     csupf0 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
+                     csupf0 with ZChain.csupf zc (subst (λ k → k o< px) zc18 a )
+                     ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , ch-init ? ⟫
+                     ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , 
+                          ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ?  ?  ⟫ 
+                 ... | tri≈ ¬a b ¬c = ⟪ asm , ch-is-sup (supf1 z1) sz1<x ? (init asm1 ? ) ⟫ where
+                     asm : odef A (supf1 z1)
+                     asm =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
+                     asm1 : odef A (supf1 (supf1 z1))
+                     asm1 =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫  ) 
 
           zc4 : ZChain A f mf ay x     --- supf px ≤ supf x
           zc4 with trio< x (supf0 px)