# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665130421 -32400
# Node ID ac4daa43ef2a8447a0010b860b7cb608ed6ee028
# Parent  37a09244cebd748b94ae4f867cbcf8b37684e015
roll back to u<x

diff -r 37a09244cebd -r ac4daa43ef2a src/zorn.agda
--- a/src/zorn.agda	Fri Oct 07 08:28:49 2022 +0900
+++ b/src/zorn.agda	Fri Oct 07 17:13:41 2022 +0900
@@ -262,7 +262,7 @@
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : supf u o≤ supf x) ( is-sup : ChainP A f mf ay supf u ) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : u o< x) ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 --
@@ -571,12 +571,12 @@
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
      chain-mono :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 
-       {a b c : Ordinal} → supf a o≤ supf b
+       {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
      chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
      chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua (OrdTrans ua<x a≤b ) is-sup fc  ⟫ 
+            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫ 
 
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
@@ -586,7 +586,6 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
-
      --
      -- Second TransFinite Pass for maximality
      --
@@ -594,7 +593,7 @@
      SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
      SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
-        chain-mono1 :  {a b c : Ordinal} → (ZChain.supf zc a) o≤ (ZChain.supf zc b)
+        chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
@@ -619,7 +618,7 @@
                 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 (o<→≤ zc08) is-sup fc ⟫ where
+                ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where
                     zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
                     zc07 = fc
                     zc06 : supf u ≡ u
@@ -642,7 +641,7 @@
           ... | 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
+        zc1 x prev with Oprev-p x  -- prev is not used now....
         ... | yes op = record { is-max = is-max } where
            px = Oprev.oprev op
            zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
@@ -654,18 +653,23 @@
            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 sb≤sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+             = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
               sb≤sx : supf b o≤ supf x
               sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 
+              sb<sx : supf b o< supf x
+              sb<sx with osuc-≡< sb≤sx
+              ... | case2 lt = lt
+              ... | case1 sb=sx = ? where
+                  -- b ≡ x
+                  -- b o< px → a < * b → odef (UnionCF A f mf ay supf px) b
               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 sb≤sx  (HasPrev.ay  nhp) 
-                 ; x=fy = HasPrev.x=fy nhp } )
+                    chain-mono1 (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 sb≤sx uz) }  , m04 ⟫
+                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (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 
@@ -682,9 +686,11 @@
            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 sb≤sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               sb≤sx : supf b o≤ supf x
               sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 
+              sb<sx : supf b o< supf x
+              sb<sx = ?
               m09 : b o< & A
               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
@@ -694,11 +700,11 @@
               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 sb≤sx (HasPrev.ay  nhp) 
+                      chain-mono1 (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 sb≤sx lt )} , m04 ⟫    -- ZChain on x
+                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (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 }
 
@@ -835,13 +841,17 @@
           ... | 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     --- supf px ≤ supf x
-          zc4 with osuc-≡< ?
-          ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
+          zc4 with trio< x (supf0 px)
+          ... | tri> ¬a ¬b c =  record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
-
+          ... | tri≈ ¬a b ¬c =  ? where
+          -- ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
+          --    ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
+  
                  --  we are going to determine (supf x), which is not specified in previous zc
                  --  case1 : supf px ≡ px 
                  --     supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and  FClosure px 
+                 sfpx=px = ?
 
                  pchainpx : HOD
                  pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
@@ -927,7 +937,7 @@
                        zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
                        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 (ZChain.supf-mono zc (o<→≤ a))  ux))
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (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
@@ -940,7 +950,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 (ZChain.supf-mono zc (o≤-refl0 b)) ux))
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? 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
@@ -1120,7 +1130,7 @@
                       zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )
                      -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
 
-          ... | case2 px<spfx = ? where
+          ... | tri< a ¬b ¬c = ? where
 
                  --  case2 : px o< supf px 
                  --     supf px is not MinSUP of previous chain , supf x ≡ supf px