# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665452479 -32400
# Node ID a6f075a164fa7e0ff9d39fd1710e538641644a9d
# Parent  02f250be89e25b0fd35f819becc2c558d5810ecf
...

diff -r 02f250be89e2 -r a6f075a164fa src/zorn.agda
--- a/src/zorn.agda	Mon Oct 10 18:25:04 2022 +0900
+++ b/src/zorn.agda	Tue Oct 11 10:41:19 2022 +0900
@@ -1042,19 +1042,35 @@
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
-                         tsup : MinSUP A (UnionCF A f mf ay supf0 z)
+                         tsup : MinSUP A (UnionCF A f mf ay supf1 z)
                          tsup=sup : supf1 z ≡ MinSUP.sup tsup 
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px 
                  ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
+                         ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 {x} ux = MinSUP.x<sup m ?
+                    ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
+                        odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                    ms01 {sup2} us P = MinSUP.minsup m ? ?
                  ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
+                         ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 {x} ux = MinSUP.x<sup m ?
+                    ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
+                        odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                    ms01 {sup2} us P = MinSUP.minsup m ? ?
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } 
+                         ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
+                    m = sup1
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 {x} ux = MinSUP.x<sup m ?
+                    ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
+                        odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                    ms01 {sup2} us P = MinSUP.minsup m ? ?
 
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                  csupf1 {z1} sz1<x = csupf2 where
@@ -1064,19 +1080,32 @@
                      psz1≤px :  supf1 z1 o≤ px
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
-                     csupf2 with  trio< z1 px
-                     csupf2 | tri< a ¬b ¬c  with osuc-≡< psz1≤px
-                     ... | case1 eq = ? -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
+                     csupf2 with  trio< z1 px | inspect supf1 z1
+                     csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
+                     ... | case1 eq =  ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
+                             record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
+                          -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
+                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
+                          supu=u = ?
                      ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
-                     ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) ? ab , ch-init ? ⟫
-                     ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? , 
-                               ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ?  ?  ⟫ 
-                     csupf2 | tri≈ ¬a b ¬c = ? where  -- supf1 z1 ≡ supf0 z1, z1 ≡ px
+                     ... | ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫
+                     ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , 
+                               ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) 
+                                 record { fcy<sup = ? ; order = ? ; supu=u = ?  } (fcpu fc (o<→≤ u<x))  ⟫ 
+                     csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
+                             record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
+                          -- supf1 z1 ≡ supf0 z1, z1 ≡ px
                           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) 
-                     csupf2 | tri> ¬a ¬b c = ?
+                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
+                          supu=u = ?
+                     csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
+                             record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
+                          --  supf1 z1 ≡ sp1, px o< z1
+                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
+                          supu=u = ?
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)