# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664694812 -32400
# Node ID d1a850b5d8e4813d74800d5bcbc0144e5a494dda
# Parent  36a50c66a00dbb4682e049fc6d8ac946440c39ae
...

diff -r 36a50c66a00d -r d1a850b5d8e4 src/zorn.agda
--- a/src/zorn.agda	Sun Oct 02 10:19:31 2022 +0900
+++ b/src/zorn.agda	Sun Oct 02 16:13:32 2022 +0900
@@ -906,48 +906,6 @@
                  ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b))
                  ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c )
 
-                 ch1x=pchainpx : UnionCF A f mf ay supf1  x ≡ pchainpx
-                 ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where
-                      fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z 
-                      fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc
-                      fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z 
-                      fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc
-                      zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
-                      zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
-                      zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with trio< u px
-                      ... | tri< a ¬b ¬c = case1 ⟪ az , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } fc ⟫ where
-                          zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
-                          zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
-                      ... | tri≈ ¬a b ¬c = case2 fc 
-                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x  ⟫ )
-                      zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
-                      zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
-                      zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = ⟪ az , ch-is-sup u 
-                          (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) 
-                              record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 (o<→≤  u<x)) (ChainP.supu=u is-sup) } (fcpu fc (o<→≤  u<x)) ⟫  where
-                          zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
-                          zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤  u<x))) ( ChainP.fcy<sup is-sup fc )
-                      zc12 {z} (case2 fc) = ⟪  A∋fc px f mf fc , ch-is-sup px (pxo<x op) record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px)  } 
-                          (subst (λ k → FClosure A f k z ) (trans sfpx=px (sym (zc16 o≤-refl ))) fc) ⟫ where
-                          zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
-                          zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
-
-                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
-                     field
-                         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 (zc16 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a))  } where
-                    m = ZChain.minsup zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
-                    m = ZChain.minsup zc (o≤-refl0 b)
-                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } 
-
                  supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
                  supf-mono1 {z} {w} z≤w with trio< w px 
                  ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w )
@@ -1020,6 +978,68 @@
                               zc23 eq = ⊥-elim (o<¬≡  eq sz0<sz1 )
                         ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl sz0<sz1 )
 
+                 ch1x=pchainpx : UnionCF A f mf ay supf1  x ≡ pchainpx
+                 ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where
+                      fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z 
+                      fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc
+                      fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z 
+                      fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc
+                      zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
+                      zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
+                      zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc21 fc where
+                          zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
+                          zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                          ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
+                          ... | case2 fc = case2 ? 
+                          zc21 (init asp refl ) with trio< u px | inspect supf1 u
+                          ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } ? ⟫ where
+                               zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
+                               zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
+                          ... | tri≈ ¬a b ¬c | _ = case2 ?
+                          ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x  ⟫ )
+                      zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
+                      zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
+                      zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where
+                          zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1
+                          zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
+                          zc21 (init asp refl ) with trio< u px | inspect supf1 u
+                          ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u 
+                               (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) 
+                                  record {fcy<sup = zc13 ; order = ? ; supu=u = trans ? (ChainP.supu=u is-sup) } ? ⟫  where
+                              zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
+                              zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤  u<x))) ( ChainP.fcy<sup is-sup fc )
+                          ... | tri≈ ¬a b ¬c | _ = ?
+                          ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ?  ⟫ )
+
+                      zc12 {z} (case2 fc) = zc21 fc where
+                          zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1
+                          zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
+                          zc21 (init asp refl ) = ⟪ asp , ch-is-sup px (pxo<x op) 
+                                     record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px)  } (init ? ? ) ⟫ where
+                              zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
+                              zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
+
+                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
+                     field
+                         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 (zc16 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a))  } where
+                    m = ZChain.minsup zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
+                    m = ZChain.minsup zc (o≤-refl0 b)
+                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1  
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } 
+
 
                  csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) 
                  csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z