# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665506789 -32400
# Node ID fec6064b44befbb846bf6c14cedf6b52196e4c50
# Parent  d917831fb60744870f2a92c4104db2f2fce266ac
...

diff -r d917831fb607 -r fec6064b44be src/zorn.agda
--- a/src/zorn.agda	Tue Oct 11 22:47:13 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 01:46:29 2022 +0900
@@ -456,22 +456,6 @@
 
    -- ordering is not proved here but in ZChain1 
 
-   supf-¬hp : {x : Ordinal } → x o≤ z → odef (UnionCF A f mf ay supf x) (supf x)
-       → ( supf x ≡ f (supf x) ) ∨  ( ¬  HasPrev A chain (supf x) f )
-   supf-¬hp {x} x≤z usx with proj1 ( mf (supf x) asupf )
-   ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) eq)) 
-   ... | case2 s<fs = case2 sh00 where
-       sh00 : ( ¬  HasPrev A chain (supf x) f )
-       sh00 hp = <-irr (<=to≤ sh01) s<fs where
-          sh01 : ( f ( supf x ) ≡  supf x ) ∨  ( f ( supf x ) <<  supf x )
-          sh01 = subst (λ k → ( f ( supf x ) ≡  k ) ∨  ( f ( supf x ) << k )) (sym (supf-is-minsup x≤z)) 
-              ( MinSUP.x<sup ( minsup x≤z ) (f-next usx )) 
-
-   supf-idem : {x : Ordinal } → supf x o< z  → supf (supf x) ≡ supf x
-   supf-idem {x} sf<z with csupf sf<z
-   ... | ⟪ au , ch-init fc ⟫ = ? 
-   ... | ⟪ au , ch-is-sup u u<z is-sup fc ⟫ = ?
-
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
@@ -1093,6 +1077,8 @@
                      --  z1 ≡ px , supf0 px ≡  px
                      psz1≤px :  supf1 z1 o≤ px
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
+                     cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px)
+                     cs01 spx<px = ZChain.csupf zc spx<px
                      cs00 : supf1 (supf1 px) ≡ supf1 px
                      cs00 = ?
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
@@ -1103,28 +1089,20 @@
                           -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
                           supu=u = ? -- ZChain.sup=u zc ? ? ?
-                     ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
-                     ... | ⟪ 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))  ⟫  where
-                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
-                          supu=u = ? -- ZChain.sup=u zc ? ? ?
-                     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
-                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
-                          supu=u = ?
+                     ... | case2 lt  = zc12 (case1 cs03)  where
+                           cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
+                           cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
+                     csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
                      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
+                          --  supf1 z1 ≡ sp1, px o< z1, sp1 o< x
                           asm : odef A (supf1 z1)
                           asm =  subst (λ k → odef A k ) (sym (sf1=sp1 c)) ( MinSUP.asm sup1) 
                           sp1=px : sp1 ≡ px
                           sp1=px with trio< sp1 px
-                          ... | tri> ¬a ¬b c = ?
-                          ... | tri≈ ¬a b ¬c = b
-                          ... | tri< a ¬b ¬c = ?
+                          ... | tri< a ¬b ¬c = ? --  sp1 o< px, supf0 sp1 ≡  supf0 px
+                          ... | tri≈ ¬a b ¬c = b 
+                          ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
                           supu=u = ?