# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664970037 -32400
# Node ID f331c8be2425fa6662eb41b0a9ec50f2663cf921
# Parent  9fb948dac666dc1e3100d77311e470b654477254
x ≤ supf x is no good

diff -r 9fb948dac666 -r f331c8be2425 src/zorn.agda
--- a/src/zorn.agda	Wed Oct 05 13:13:35 2022 +0900
+++ b/src/zorn.agda	Wed Oct 05 20:40:37 2022 +0900
@@ -450,8 +450,8 @@
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u≤z fc with MinSUP.x<sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans ? (sym (supf-is-minsup u≤z ) ) ))
-   ... | case2 lt = case2 ? -- (subst (λ k → * w < k ) ? )-- (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-minsup u≤z ))) ) lt )
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
+   ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
 
    -- ordering is not proved here but in ZChain1 
 
@@ -642,12 +642,12 @@
         order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
         order {b} {s} {z1} b<z ss<sb fc = zc04 where
           zc00 : ( z1  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
-          zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) ? -- (csupf-fc (o<→≤ b<z) ss<sb fc )
+          zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc (o<→≤ b<z) ss<sb fc ))
           -- supf (supf b) ≡ supf b
           zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
           zc04 with zc00
-          ... | case1 eq = ? -- case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) (cong (&) eq) )
-          ... | case2 lt = ? -- case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) ) )))  lt )
+          ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
+          ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
@@ -662,15 +662,20 @@
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab P a<b | case2 is-sup 
-             = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+             = ⟪ ab , ch-is-sup b b<sfx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
+              b<sfx : b o< ZChain.supf zc x
+              b<sfx with trio< x (& A)
+              ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a))
+              ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b))
+              ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ b<A ( ZChain.x≤supfx zc (o≤-refl)))
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
-              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 ? (HasPrev.ay  nhp) 
+              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? uz )  }  , m04 ⟫
+                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) uz )  }  , m04 ⟫
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -687,22 +692,25 @@
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-           ... | case2 y<b = ⟪ ab , ch-is-sup b m10 m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b b<sfx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-              m10 : b o< ZChain.supf zc x
-              m10 = ordtrans<-≤ b<x ( ZChain.x≤supfx zc ? )
+              b<sfx : b o< ZChain.supf zc x
+              b<sfx with trio< x (& A)
+              ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a))
+              ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b))
+              ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ m09 ( ZChain.x≤supfx zc (o≤-refl)))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
               m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m08 {s} {z1} s<b fc = order m09 s<b fc
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
-              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 ? (HasPrev.ay  nhp) 
+              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? lt )} , m04 ⟫    -- ZChain on x
+                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) lt )} , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -720,9 +728,6 @@
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z21 : & (SUP.sup sp1) o< & A
            z21 = c<→o< ( SUP.as sp1)
-           --  ZChain.supf zc (& A) o≤ & (SUP.sup sp1)  ( minimality )
-           z11 : & (SUP.sup sp1) o< ZChain.supf zc (& A)
-           z11 = ? -- c<→o< ( SUP.as sp1)
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
@@ -839,7 +844,7 @@
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
           zc4 : ZChain A f mf ay x
-          zc4 with osuc-≡< (ZChain.x≤supfx zc ? )
+          zc4 with osuc-≡< (ZChain.x≤supfx zc o≤-refl )
           ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
               ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ?    }  where
 
@@ -864,10 +869,9 @@
                     zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb ))
                     ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
                     ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
-                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) 
-                             ? -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 ? k) (sym &iso) ca )
-                    ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 ? )-- (cong (&) eq))
-                    ... | case2 lt = case2 (subst (λ k → (* a) < k ) ? ? ) -- (trans (sym *iso) (cong (*) zc06)) lt)
+                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca )
+                    ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
+                    ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) 
 
                  ptotal : IsTotalOrderSet pchainpx
                  ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso 
@@ -929,9 +933,9 @@
                  supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
                  ... | tri< a ¬b ¬c = zc19 where
                        zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
-                       zc21 = ZChain.minsup zc ? -- (o<→≤ a)
+                       zc21 = ZChain.minsup zc (o<→≤ a)
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux))
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc (o<→≤ a))  ux))
                        zc19 : supf0 z o≤ sp1 
                        zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
@@ -944,7 +948,7 @@
                          supf0 px ≡⟨ sym sfpx=px ⟩
                          px ∎ where open ≡-Reasoning
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux))
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc (o≤-refl0 b)) ux))
                        zc18 : px o≤ sp1 -- supf0 z ≡ px 
                        zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
@@ -1009,7 +1013,7 @@
                               zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup 
                                  (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where
                                     zc19 : u o≤ px
-                                    zc19 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? --  u<x
+                                    zc19 = o<→≤ a
                                     zc18 : s o≤ px
                                     zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19
                               zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
@@ -1085,21 +1089,21 @@
                                   -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
                                   csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
                                   csupf17 (init as refl ) = ZChain.csupf zc sf<px 
-                                  csupf17 (fsuc x fc) = ? -- ZChain.f-next zc ? -- (csupf17 fc)
+                                  csupf17 (fsuc x fc) = ZChain.f-next zc ? -- (csupf17 fc)
 
                  x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z
                  x≤supfx1 {z} z≤x with trio< z (supf1 z) --  supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px
                  ... | tri< a ¬b ¬c = o<→≤ a
                  ... | tri≈ ¬a b ¬c = o≤-refl0 b
                  ... | tri> ¬a ¬b c with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.x≤supfx zc ?
+                 ... | tri< a ¬b ¬c = ZChain.x≤supfx zc (o<→≤ a)
                  ... | tri≈ ¬a b ¬c = subst (λ k → k o< osuc px) (sym b) <-osuc
                  ... | tri> ¬a ¬b lt = ⊥-elim ( o≤> sf04 c ) where --   c : sp1 o< z, lt : px o< z --  supf1 z ≡ sp1 -- supf1 z o< z
                        z=x : z ≡ x 
                        z=x with trio< z x
                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ lt , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) a ⟫ )
                        ... | tri≈ ¬a b ¬c = b
-                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x ? )
+                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x c )
                        sf01 : supf1 x ≡ sp1
                        sf01 with trio< x px
                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬c (pxo<x op ))
@@ -1111,10 +1115,11 @@
                        sf00 = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) sf01 sf02
                        sf04 : z o≤ sp1
                        sf04 with osuc-≡< sf00
-                       ... | case1 eq = ? --   sup of U px ≡ supf1 px ≡ supf1 x ≡ sp1 ≡ sup of U x
-                           --   px ≡ supf0 px
-                           --   px ≡ supf1 x
-                           --   supf1 x ≡ x ?
+                       ... | case1 eq = ? where
+                             sf05 : px ≡ sp1 -- z o< osuc x -- z ≡ x
+                             sf05 = eq
+                             sf06 : z ≡ osuc sp1 -- z o< osuc x -- z ≡ x
+                             sf06 = trans z=x (trans (sym (Oprev.oprev=x op)) (cong osuc sf05 ))
                        ... | case2 lt = subst (λ k → k o≤ sp1 ) (trans (Oprev.oprev=x op) (sym z=x)) (osucc lt )
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
@@ -1140,7 +1145,7 @@
                         z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
                  ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
                       z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px 
-                      z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 ? ) ))
+                      z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) ))
                       zc20 : supf0 px ≡ supf1 z1 
                       zc20 = begin
                         supf0 px  ≡⟨ sym sfpx=px ⟩
@@ -1151,7 +1156,7 @@
                       zc21 : px o< z1
                       zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c  )
                       zc22 : z1 o< x -- c : px o< supf0 z1
-                      zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 ? ) )
+                      zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) )
                      -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
 
           ... | case2 px<spfx = ? where