# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661770599 -32400
# Node ID 01361e10ad96a9afd7b4f2c83ec9e49c3f41279f
# Parent  52bff0b4cb37e2b1cf1c2aaad5e659f6126a3945
...

diff -r 52bff0b4cb37 -r 01361e10ad96 src/zorn.agda
--- a/src/zorn.agda	Mon Aug 29 10:18:08 2022 +0900
+++ b/src/zorn.agda	Mon Aug 29 19:56:39 2022 +0900
@@ -771,27 +771,65 @@
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } 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 u u≤px is-sup fc ⟫ = zc12 fc where
-                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
+                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc12 fc where
+                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u1) z → odef pchain1 z
                           zc12 (fsuc x fc) with zc12 fc
                           ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
-                          ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
-                          zc12 (init asu su=z ) with trio< u px
-                          ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu  , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) 
-                              record { fcy<sup = ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫ 
-                          ... | tri≈ ¬a b ¬c = ?
-                          ... | tri> ¬a ¬b c = ?
+                          ... | ⟪ 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₁) ⟫ 
+                          zc12 (init asp refl ) with trio< u1 px | inspect supf1 u1
+                          ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x ? ) 
+                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
+                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
+                              order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
+                                (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
+                              order {s} {z2} s<u1 fc with trio< s px 
+                              ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
+                              ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
+                              ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? ))  --  px o< s < u1 < px
+                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x ? ) 
+                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
+                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
+                              order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
+                                (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
+                              order {s} {z2} s<u1 fc with trio< s px 
+                              ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
+                              ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
+                              ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b ? ) ))  --  px o< s < u1 = px
+                          ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x 
+                          ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
+                          ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
+
                      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 u u≤x is-sup fc ⟫ = zc13 fc where
-                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
+                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc13 fc where
+                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u1) z → odef pchain z
                           zc13 (fsuc x fc) with zc13 fc
                           ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                           ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
-                          zc13 (init asu su=z ) with trio< u x
-                          ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (subst (λ k → u o< k) (sym (Oprev.oprev=x op))  a) ? (init ? ? ) ⟫ 
-                          ... | tri≈ ¬a b ¬c = ?
-                          ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c )
+                          zc13 (init asp refl ) with trio< u1 px | inspect supf1 u1
+                          ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (subst (λ k → u1 o< k ) ? a )
+                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans ? (ChainP.supu=u u1-is-sup)   } (init ? ?)  ⟫ where
+                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
+                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
+                              order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 →
+                                (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
+                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
+                              ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? ))  --  px o< s < u1 < px
+                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x ? ) 
+                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ?) (ChainP.supu=u u1-is-sup)   } (init ? ? )  ⟫ where
+                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
+                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
+                              order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 →
+                                (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
+                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
+                              ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? ))  --  px o< s < u1 = px
+                          ... | tri> ¬a ¬b c | _ = ⊥-elim ( o≤> u1≤x ? )
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px | inspect supf1 z
                  ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤   a) 
@@ -827,21 +865,11 @@
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                  sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
                  sis {z} z≤x  = zc40 where
-                      zc40 : supf1 z ≡ & (SUP.sup (sup z≤x))
+                      zc40 : supf1 z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error
                       zc40 with trio< z px | inspect supf1 z | inspect sup z≤x
                       ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
                       ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
                       ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ?
---                 ... | tri< a ¬b ¬c = ? -- jZChain.supf-is-sup zc (o<→≤ a )
---                 ... | tri≈ ¬a b ¬c = ? -- jZChain.supf-is-sup zc (o≤-refl0 b )
---                 ... | tri> ¬a ¬b px<z = ? 
---                 ... | tri< a ¬b ¬c | _ = ? -- jZChain.supf-is-sup zc (o<→≤ a )
---                 ... | tri≈ ¬a b ¬c | _ = ? -- jZChain.supf-is-sup zc (o≤-refl0 b )
---                 ... | tri> ¬a ¬b px<z | record { eq = eq1 } = ? where
---                     zc30 : z ≡ x
---                     zc30 with osuc-≡< z≤x
---                     ... | case1 eq = eq
---                     ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)