# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664527691 -32400
# Node ID 1a84433ebc1be2795740ce3b23ef12216c80413b
# Parent  3c2ab35da199d04c63e669de3e1ba989a38587a5
...

diff -r 3c2ab35da199 -r 1a84433ebc1b src/zorn.agda
--- a/src/zorn.agda	Fri Sep 30 17:35:37 2022 +0900
+++ b/src/zorn.agda	Fri Sep 30 17:48:11 2022 +0900
@@ -836,8 +836,8 @@
           --           supf0 px ≡ px 
           --           supf0 px ≡ supf0 x 
 
-          no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-          no-extension P with osuc-≡< (ZChain.x≤supfx zc )
+          zc4 : ZChain A f mf ay x
+          zc4 with osuc-≡< (ZChain.x≤supfx zc )
           ... | case1 sfpx=px = ? where
                  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
@@ -1094,7 +1094,7 @@
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc32 = ZChain.sup zc o≤-refl 
                      zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 ne {w} lt with zc11 P ⟪ proj1 lt , ? ⟫
+                     zc34 ne {w} lt with zc11 ? ⟪ proj1 lt , ? ⟫
                      ... | case1 lt = SUP.x<sup zc32 lt 
                      ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
@@ -1113,7 +1113,7 @@
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
                  ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
-                 ... | tri> ¬a ¬b px<b = zc31 P where
+                 ... | tri> ¬a ¬b px<b = zc31 ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
@@ -1129,20 +1129,6 @@
                      ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev 
                                 ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } ) 
 
-          zc4 : ZChain A f mf ay x 
-          zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension (case1 ( λ s → noax (subst (λ k → odef A k ) (sym &iso) (xSUP.ax s) ))) -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f )   
-               -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
-          ... | case1 is-sup = ? -- x is a sup of zc 
-          ... | case2 ¬x=sup =  no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention
-             nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x 
-             nsup s = ¬x=sup z12 where
-                z12 : IsSup A (UnionCF A f mf ay supf0 px) ax
-                z12 = record { x<sup = λ {z} lt → subst (λ k → (z ≡ k) ∨ (z << k )) (sym &iso) ( IsSup.x<sup ( xSUP.is-sup s ) lt ) }
-
      ... | no lim = zc5 where
 
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z