# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665650839 -32400
# Node ID f0b98f57ec650186dd9c10bb37a45be5ff39c2f5
# Parent  8695050933a78205864357a277972a8b06a53054
...

diff -r 8695050933a7 -r f0b98f57ec65 src/zorn.agda
--- a/src/zorn.agda	Wed Oct 12 20:49:21 2022 +0900
+++ b/src/zorn.agda	Thu Oct 13 17:47:19 2022 +0900
@@ -456,14 +456,6 @@
 
    -- ordering is not proved here but in ZChain1 
 
-   csupf< : {a b : Ordinal } → a o≤ b → odef (UnionCF A f mf ay supf z) (supf b) → odef (UnionCF A f mf ay supf z) (supf a) 
-   csupf< {a} {b} a≤b ⟪ as , ch-init fc ⟫ = ⟪ ? , ch-init ?  ⟫ 
-   csupf< {a} {b} a≤b ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? , ch-is-sup (supf a) uz01 ? ? ⟫ where
-       a≤u : ?
-       a≤u = ?
-       uz01 : supf a o< z
-       uz01 = ordtrans≤-< (subst (λ k → supf a o< k) (cong osuc (ChainP.supu=u is-sup)) (supf-mono a≤u )) u<x
-
 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
@@ -1103,24 +1095,38 @@
                              supf1 px ≡⟨ sym sfz=sfpx ⟩
                              supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a)  ⟩
                              supf0 z1 ∎ where open ≡-Reasoning
-                     ... | case2 sfz<sfpx =  ? ---   supf0 z1 o< supf0 px
+                     ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫  )  where
+                            --- supf1 z1 ≡ px , z1 o< px ,  px ≡ supf0 z1 o< supf0 px o< x
+                           cs05 : px o< supf0 px
+                           cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
+                           cs06 : supf0 px o< osuc px
+                           cs06 = subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x 
                      csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
-                     csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 }  with trio< sp1 px
-                     ... | tri< sp1<px ¬b ¬c = ? --  sp1 o< px, supf0 sp1 ≡  supf0 px, sp1 o< z1
-                     ... | tri≈ ¬a sp1=px ¬c = ⟪ 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, sp1 o< x  -- sp1 o< z1
-                          --  supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1
-                          asm : odef A (supf1 z1)
-                          asm =  subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) 
-                          cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) 
-                          cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin
-                             supf0 px ≡⟨ sym (sf1=sf0 o≤-refl )  ⟩
-                             supf1 px ≡⟨ cong supf1 (sym sp1=px)  ⟩
-                             supf1 sp1 ∎  ))) where open ≡-Reasoning
-                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
-                          supu=u = ?
-                     ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
+                     csupf2 | tri> ¬a ¬b px<z1 | 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 
+                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
+                           supu=u = ?
+                           sp1≤px : sp1 o≤ px
+                           sp1≤px with trio< sp1 px
+                           ... | tri< a ¬b ¬c = o<→≤ a
+                           ... | tri≈ ¬a b ¬c = o≤-refl0 b
+                           ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
+
+                     -- with trio< sp1 px
+                     -- ... | tri< sp1<px ¬b ¬c = ? --  supf1 z1 = sp1 o< px o< z1 
+                     -- ... | tri≈ ¬a sp1=px ¬c = ⟪ 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, sp1 o< x  -- sp1 o< z1
+                     --      --  supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1
+                     --      asm : odef A (supf1 z1)
+                     --      asm =  subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) 
+                     --      cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) 
+                     --      cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin
+                     --         supf0 px ≡⟨ sym (sf1=sf0 o≤-refl )  ⟩
+                     --        supf1 px ≡⟨ cong supf1 (sym sp1=px)  ⟩
+                     --       supf1 sp1 ∎  ))) where open ≡-Reasoning
+                     --... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)