# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660718417 -32400
# Node ID d395f1827e6aa30d283fdce311e08e16da2e76ca
# Parent  89c4e8f06ce183035e03eaaff61afe3a9cf91191
another spuf1

diff -r 89c4e8f06ce1 -r d395f1827e6a src/zorn.agda
--- a/src/zorn.agda	Wed Aug 17 14:32:33 2022 +0900
+++ b/src/zorn.agda	Wed Aug 17 15:40:17 2022 +0900
@@ -285,7 +285,7 @@
 
       sup : {x : Ordinal } → x o< z  → SUP A (UnionCF A f mf ay supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b 
-      supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) )
+      supf-is-sup : {x : Ordinal } → (x<z : x o< z) → supf x ≡ & (SUP.sup (sup x<z) )
       csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) 
 
    -- ordering is proved here for totality and sup
@@ -672,7 +672,7 @@
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z px
           ... | tri< a ¬b ¬c = ZChain.supf zc z
-          ... | tri≈ ¬a b ¬c = ZChain.supf zc z
+          ... | tri≈ ¬a b ¬c = sp1
           ... | tri> ¬a ¬b c = sp1
 
           pchain1 : HOD
@@ -715,17 +715,17 @@
                     (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 s<u1 fc )
-                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri≈ ¬a b ¬c = ? -- subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
                   ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                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
+                record { fcy<sup = fcy<sup ; order = order ; supu=u = trans 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 )
+                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ? -- ( ChainP.fcy<sup u1-is-sup fc )
                   order : {s : Ordinal} {z2 : Ordinal} → s o< 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 s<u1 fc )
-                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
                   ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
               ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px)
               ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
@@ -750,17 +750,17 @@
                             (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) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = ? -- subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
                           ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
                       ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                        record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init asp refl )  ⟫ where
+                        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 )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
+                          fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
                           order : {s : Ordinal} {z2 : Ordinal} → s o< 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) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (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 s<u1 (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 s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? ))
                           ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
                       ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px
                       ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) )
@@ -813,7 +813,7 @@
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
                  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 (UnionCF⊆ o≤-refl (o<→≤ a) lt) } 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
+                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
                  ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -823,8 +823,8 @@
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) o≤-refl lt) } } 
                  csupf : {b : Ordinal} → b o< x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
-                 csupf {b} b≤x with trio< b px | inspect supf1 b
-                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc a  )
+                 csupf {b} b<x with trio< b px | inspect supf1 b
+                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc  a  )
                  ... | tri≈ ¬a b ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc ? )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } =  
                     ⟪ SUP.as sup1  , ch-is-sup ?  ? ? (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl))  ⟫