# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667709585 -32400
# Node ID 9a8041a7f3c92254adcd9698bd806d896491e57e
# Parent  cd0ef83189c5e73bc0f8db70a21eb1e94f549bc6
...

diff -r cd0ef83189c5 -r 9a8041a7f3c9 src/zorn.agda
--- a/src/zorn.agda	Sat Nov 05 18:29:21 2022 +0900
+++ b/src/zorn.agda	Sun Nov 06 13:39:45 2022 +0900
@@ -884,8 +884,8 @@
           zc43 = ?
           
           zc41 : ZChain A f mf ay x
-          zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
-          zc41 | (case2 sfpx<sp1) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
+          zc41 with zc43
+          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
                  --  supf0 px is included by the chain of sp1
                  --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
@@ -909,6 +909,9 @@
                  ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z )
                  ... | tri> ¬a ¬b c = refl
 
+                 sf=eq :  { z : Ordinal } → z o< x → supf0 z ≡ supf1 z
+                 sf=eq {z} z<x = sym (sf1=sf0 (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ))
+
                  asupf1 : {z : Ordinal } → odef A (supf1 z)
                  asupf1 {z} with trio< z px
                  ... | tri< a ¬b ¬c = ZChain.asupf zc
@@ -938,6 +941,13 @@
                        zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
 
+                 sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
+                 sf≤ {z} x≤z with trio< z px
+                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
+                 ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c) 
+                     (supf1-mono (o<→≤ c ))
+                      --  px o<z → spuf0 x ≡ supf0 px ≡ supf1 px o≤ supf1 z
 
                  fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
                  fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
@@ -1122,7 +1132,7 @@
                      -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
 
 
-          zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
+          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
 
                  --  supf0 px not is included by the chain
@@ -1131,7 +1141,7 @@
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px
                  ... | tri< a ¬b ¬c = supf0 z
-                 ... | tri≈ ¬a b ¬c = supf0 px
+                 ... | tri≈ ¬a b ¬c = supf0 z
                  ... | tri> ¬a ¬b c = supf0 px
 
                  sf1=sf0 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z
@@ -1140,6 +1150,17 @@
                  ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
 
+                 sf=eq :  { z : Ordinal } → z o< x → supf0 z ≡ supf1 z
+                 sf=eq {z} z<x with trio< z px
+                 ... | tri< a ¬b ¬c = refl
+                 ... | tri≈ ¬a b ¬c = refl 
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op))  z<x ⟫ )
+                 sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
+                 sf≤ {z} x≤z with trio< z px
+                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
+                 ... | tri> ¬a ¬b c = o≤-refl0 ( ZChain.supfmax zc px<x )
+
                  zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
                  zc17 = ? -- px o< z, px o< supf0 px
 
@@ -1152,7 +1173,7 @@
                  ... | tri> ¬a ¬b c = o≤-refl
                  supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
                  ... | tri< a ¬b ¬c = zc17
-                 ... | tri≈ ¬a b ¬c = o≤-refl
+                 ... | tri≈ ¬a b ¬c = o≤-refl0 ?
                  ... | tri> ¬a ¬b c = o≤-refl
 
                  pchain1 : HOD