# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668170918 -32400
# Node ID 6101b9bfbe57f85f70b11565877f1cae61ddd8c4
# Parent  6d29911a9d00ead2b9e7e7c67ecdf2e39e533c33
...

diff -r 6d29911a9d00 -r 6101b9bfbe57 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 11 19:27:15 2022 +0900
+++ b/src/zorn.agda	Fri Nov 11 21:48:38 2022 +0900
@@ -267,7 +267,7 @@
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u )
-      order    : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+      order    : {s z1 : Ordinal} → (lt : s o< u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
       supu=u   : supf u ≡ u
 
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
@@ -320,7 +320,7 @@
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
-     ... | tri< a₁ ¬b ¬c with ChainP.order supb  (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁)  fca
+     ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ fca -- (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁)  fca
      ... | case1 eq with s≤fc (supf ub) f mf fcb
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -337,7 +337,7 @@
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c
          = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa c fcb -- (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb
      ... | case1 eq with s≤fc (supf ua) f mf fca
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -490,7 +490,7 @@
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b)
           → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
-      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 : Ordinal} → b o< & A → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -645,10 +645,10 @@
                 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
                 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫
-        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 : Ordinal} → b o< & A → s o< 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) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc 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 b<z ? fc ))
           -- supf (supf b) ≡ supf b
           zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
           zc04 with zc00
@@ -682,9 +682,9 @@
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {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
-              m09 {s} {z} s<b fcz = order b<A s<b fcz
+              m09 {s} {z} s<b fcz = order b<A ?  fcz
               m06 : ChainP A f mf ay supf b
-              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
+              m06 = record {  fcy<sup = m08  ; order = ? ; supu=u = m05 }
         ... | no lim = record { is-max = is-max ; order = order }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
@@ -703,7 +703,7 @@
               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
+              m08 {s} {z1} s<b fc = order m09 ? fc
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                       chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
@@ -711,7 +711,7 @@
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b
-              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
+              m06 = record { fcy<sup = m07 ;  order = ? ; supu=u = m05 }
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -1396,18 +1396,6 @@
           sz<<c : {z : Ordinal } → z o< & A → supf z <= mc
           sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
 
-          z511 : {u y mc : Ordinal} (u<x : u o< mc ) (is-sup1 : ChainP A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) u)
-                (fc  : FClosure A (cf nmx) (ZChain.supf zc u) y) (x=fy : mc ≡ cf nmx y) → 
-                   ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
-          z511 {u} {y} {mc} u<x is-sup fc x=fy with osuc-≡< (ZChain.supf-mono zc (o<→≤ u<x))
-          ... | case2 lt = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) ? lt (fsuc _ ( fsuc  _ fc )))
-          ... | case1 eq = ?
-               --    u ≡ supf u ≡ supf mc ≡ supf (cf nmx y) 
-               --    supf u << cf nmx (cf nmx ( ... (supf u )) <= spuf mc ≡ u
-               --    y ≡ supf u
-               --    y ≡ cf nmx (supf u)
-               --    y ≡ cf nmx (cf nmx (supf u))
-
           sc=c : supf mc ≡ mc
           sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
               not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc
@@ -1425,7 +1413,7 @@
                    z32 : * (supf mc) < * (cf nmx (cf nmx y))
                    z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
                    z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
-                   z48 = z511 u<x is-sup1 fc x=fy
+                   z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A ? (fsuc _ ( fsuc  _ fc )))
               is-sup :  IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc)  (MinSUP.asm msp1)
               is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) }
 
@@ -1458,9 +1446,9 @@
                         z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
                         z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt
                 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
-                z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc  _ fc ))
+                z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A ? (fsuc _ ( fsuc  _ fc ))
                 z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) )
-                z50 = ≤to<= ( z511 u<x is-sup1 fc x=fy )
+                z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A ? (fsuc _ ( fsuc  _ fc ))
                 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
                     → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1
                     →  * (cf nmx (cf nmx y)) < * d1
@@ -1503,7 +1491,8 @@
                     z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57
                     z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d )
                     z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A
-                        (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1))  u<smc)  fc ) smc<<d )
+                        ?  fc ) smc<<d )
+                        -- (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1))  u<smc)  fc ) smc<<d )
                     z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d )
                     z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) )
                     -- u<x    : ZChain.supf zc u o< ZChain.supf zc d