# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662560249 -32400
# Node ID bba4ce6d276687c83710477774fdaa2f8a955225
# Parent  266e0b9027cd6a9e695336404826816f003b8d8e
...

diff -r 266e0b9027cd -r bba4ce6d2766 src/zorn.agda
--- a/src/zorn.agda	Wed Sep 07 21:28:30 2022 +0900
+++ b/src/zorn.agda	Wed Sep 07 23:17:29 2022 +0900
@@ -787,22 +787,23 @@
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
 
-          no-extension : ¬ xSUP (UnionCF A f mf ay supf0 px) x → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max
+          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 = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
                  pchain0=1 : pchain ≡ pchain1
-                 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
+                 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 P } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                      zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                      zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) u1-is-sup  fc  ⟫
-                     zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
-                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x
+                     zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
+                        → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
+                     zc11 P {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc11 P {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x
                      ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px u1-is-sup fc  ⟫ where
                                 u1≤px : u1 o≤ px  
                                 u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt)
-                     ... | case1 eq = ⊥-elim (¬sp=x zcsup) where
+                     zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | case1 eq = ⊥-elim (¬sp=x zcsup) where
                              s1u=x : supf0 u1 ≡ x
                              s1u=x = trans (ChainP.supu=u u1-is-sup) eq
                              zc13 : osuc px o< osuc u1
@@ -825,6 +826,21 @@
                              zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                              zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) 
                                  ; is-sup = record { x<sup = x<sup } }
+                     zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | case1 eq = zc20 fc where
+                        zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
+                        zc20 {z} (init asu su=z ) = zc13 where
+                          zc14 : x ≡ z
+                          zc14 = begin
+                             x ≡⟨ sym eq ⟩
+                             u1 ≡⟨  sym (ChainP.supu=u u1-is-sup ) ⟩
+                             supf0 u1 ≡⟨ su=z ⟩
+                             z ∎ where open ≡-Reasoning
+                          zc13 : odef pchain z
+                          zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) )
+                        zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc)
+
+                     -- zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup (init asu su=z ) ⟫ | case1 eq = zc13 where
+                     --zc11 (case2 hp) {.(f w)} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup (fsuc w fc) ⟫ | case1 eq = ?
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
                          tsup : SUP A (UnionCF A f mf ay supf0 z)
@@ -849,15 +865,18 @@
                  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 is-sup lt } 
                  ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup lt } 
-                 ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
+                 ... | tri> ¬a ¬b px<b = zc31 P where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
-                     zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
-                     zcsup with zc30
-                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
-                        IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
+                     zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → supf0 b ≡ b
+                     zc31 (case1 ¬sp=x) = ⊥-elim (¬sp=x zcsup ) where
+                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
+                         zcsup with zc30
+                         ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
+                            IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
+                     zc31 (case2 hasPrev ) = ?
 
                  zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
                  zc04 {b} b≤x with trio< b px