# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660813755 -32400
# Node ID eec82adba99bc063302ef7c5ca102a1d73e7b962
# Parent  8a06fe74721bb7c8f56b11a9264dfc1c2cd53bb7
...

diff -r 8a06fe74721b -r eec82adba99b src/zorn.agda
--- a/src/zorn.agda	Thu Aug 18 14:11:58 2022 +0900
+++ b/src/zorn.agda	Thu Aug 18 18:09:15 2022 +0900
@@ -286,7 +286,18 @@
       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-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
+      --  supf b ≡ b → csupf0 → csupf
+   csupf0 : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b) ) (supf b) 
+   csupf0 {b}  b≤z = ?
+   supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y 
+   supf-inject {x} {y} sx<sy with trio< x y
+   ... | tri< a ¬b ¬c = a
+   ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
+   ... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) )
+   ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
+   ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
    -- ordering is proved here for totality and sup
 
@@ -295,13 +306,31 @@
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
-       
+
    order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z s<b fc = zc04 where
       zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
       zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
             s<z : s o< z
             s<z = ordtrans s<b b<z
+            zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
+            zc04 = ?
+            zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
+            zc05 with zc04
+            ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
+            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where
+                zc06 : supf u ≡ u
+                zc06 = ChainP.supu=u is-sup
+                u≤b : u o≤ supf s  → u o≤ b
+                u≤b u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s)
+                ... | case1 su=ss = o<→≤ (supf-inject zc08 ) where
+                    zc07 : supf u o≤ supf b   
+                    zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono  (o<→≤ s<b)  )
+                    zc08 : supf u o< supf b   
+                    zc08 with osuc-≡< zc07
+                    ... | case1 su=sb = ?
+                    ... | case2 lt = lt
+                ... | case2 lt = o<→≤ (ordtrans (supf-inject lt) s<b)
             zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
             zc03 with csupf (o<→≤ s<z) 
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
@@ -515,9 +544,9 @@
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz )  }  )
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
-              m09 : {sup1 z1 : Ordinal} → sup1 o< b 
-                           → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
-              m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
+              m09 : {s z1 : Ordinal} → s o< b 
+                           → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
+              m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz    
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } }  
@@ -535,9 +564,9 @@
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
               m07 {z} fc = ZChain.fcy<sup zc  m09 fc
-              m08 : {sup1 z1 : Ordinal} → sup1 o< b 
-                       → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
-              m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
+              m08 : {s z1 : Ordinal} → s o< b 
+                       → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
+              m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab (o<→≤  m09)
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} )   -- ZChain on x
@@ -702,9 +731,9 @@
                ax : odef A x
                is-sup : IsSup A (UnionCF A f mf ay supf0 px) ax
 
-          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o≤ px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
-          UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
+          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o< px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
+          UnionCF⊆ {z0} {z1} z0≤1 z0<px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF⊆ {z0} {z1} z0≤1 z0<px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
               zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w
               zc60 (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 z0≤1 ) 
@@ -727,7 +756,7 @@
                   ... | 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)
+              ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x (o<→≤ z0<px))
               ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
               ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
               zc60 (fsuc w1 fc) with zc60 fc
@@ -783,7 +812,7 @@
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     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<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl  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 px<b = ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
@@ -792,10 +821,10 @@
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                      zcsup : xSUP
                      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) } } 
+                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) ? 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 (o<→≤ a)  )
+                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ( ZChain.csupf zc (o<→≤ a)  )
                  ... | tri≈ ¬a refl ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? --  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
                  sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))