# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659458974 -32400
# Node ID a08c456d49d0ab4f6eae0c0ea6b7710a1591e09d
# Parent  c164f4f7cfd1e1fc34dd8c3884521b63db11cb42
...

diff -r c164f4f7cfd1 -r a08c456d49d0 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Tue Aug 02 16:09:00 2022 +0900
+++ b/src/OrdUtil.agda	Wed Aug 03 01:49:34 2022 +0900
@@ -84,7 +84,8 @@
 ... | case1 x=y = subst ( λ k → ox o< k ) (x=y) x<y
 ... | case2 y<z = ordtrans x<y y<z
 
-open _∧_
+o∅≤z : {z : Ordinal } → o∅ o< (osuc z)
+o∅≤z {z} = b<x→0<x ( <-osuc )
 
 osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
 proj2 (osuc2 x y) lt = osucc lt
diff -r c164f4f7cfd1 -r a08c456d49d0 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 02 16:09:00 2022 +0900
+++ b/src/zorn.agda	Wed Aug 03 01:49:34 2022 +0900
@@ -284,7 +284,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 : u o< 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
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -334,7 +334,7 @@
             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  ⟫ 
-            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u<x s<b) is-sup fc ⟫ 
+            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u<x (osucc s<b)) is-sup fc ⟫ 
         zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
@@ -506,15 +506,7 @@
         chain-mono1 x {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
         chain-mono1 x {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  ⟫ 
-        chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
-        chain<ZA {x} ux with proj2 ux
-        ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
-        ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ch-is-sup u u<x is-sup fc ⟫  where
-            u<A : (& ( * ( ZChain.supf zc u)))  o< & A
-            u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
-            u<x :  u o< & A
-            u<x = subst (λ k → k o< & A ) (trans &iso ?) u<A
+            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (osucc a≤b )) is-sup fc  ⟫ 
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
             b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → 
@@ -528,8 +520,8 @@
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max } where
            px = Oprev.oprev op
-           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
-           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+           zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
+           zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
@@ -543,23 +535,22 @@
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
-                 ... | tri< b<px ¬b ¬c = chain-mono1 x (ordtrans px<x ? ) m04 where
+                 ... | tri< b<px ¬b ¬c = chain-mono1 x (ordtrans px<x <-osuc ) m04 where
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u u<x is-sup fc with trio< u px
-                    ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u a is-sup fc ⟫
-                    ... | tri≈ ¬a u=px ¬c = ?   ---    supf u < a < b , 
-                    ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
+                    ... | ch-is-sup u u≤x is-sup fc with osuc-≡< u≤x
+                    ... | case1 u=x = ?    -- u is sup of chain px, b is also a sup becasue it has no prev , so a = b
+                    ... | case2 u<x = ⟪ proj1 ua , ch-is-sup u (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x) is-sup fc ⟫
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
-                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x ? lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
+                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x (ordtrans px<x <-osuc) lt)  } ) a<b
+                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
                     b<A : b o< & A
                     b<A = z09 ab
                     m05 : b ≡ ZChain.supf zc b
                     m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x ? uz )  }  )
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x (osucc 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} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
@@ -574,9 +565,8 @@
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
-           ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA {x} (chain-mono1 (osuc x) ? ua )) )
-                       (subst (λ k → * a < * k ) (sym b=y) a<b ) )
-           ... | case2 y<b = chain-mono1 x ? m04 where
+           ... | 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 = chain-mono1 x (osucc b<x) m04 where
                  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
@@ -586,11 +576,11 @@
                  m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u zc ab m09
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x ? lt )} )   -- ZChain on x
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b 
                  m06 = record { fcy<sup = m07 ;  order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , ch-is-sup b ?  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
+                 m04 = ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -698,7 +688,7 @@
           mono : {x : Ordinal} {z : Ordinal} → x o< z → isupf x o≤ isupf z 
           mono {x} {z} x<z = o≤-refl
           csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z)
-          csupf {z} z≤0 = ⟪ asi , ch-is-sup spi ? uz02 (init asi refl) ⟫ where
+          csupf {z} z≤0 = ⟪ asi , ch-is-sup o∅ o∅≤z uz02 (init asi refl) ⟫ where
                uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi)
                uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
                ... | case1 eq = case1 ( begin
@@ -708,7 +698,7 @@
                ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
                uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
                uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
-               uz02 :  ChainP A f mf ay isupf spi 
+               uz02 :  ChainP A f mf ay isupf o∅
                uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
 
 
@@ -755,6 +745,7 @@
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
+          --  (¬ odef (UnionCF A f mf ay supf0 z) (supf0 px)) ∨ (supf0 px is sup of UnionCF px )
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0 ; supf-mono = ZChain.supf-mono zc ; sup = sup
                ; initial = pinit ; chain∋init = pcy  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
@@ -768,9 +759,11 @@
                      zc9 = supP pchain  pchain⊆A ptotal
                      zc8 : odef (UnionCF A f mf ay supf0 z) (supf0 px)
                      zc8 = subst (λ k → odef (UnionCF A f mf ay supf0 z) k ) (cong supf0 b)  (ZChain.csupf zc (subst (λ k → z o≤ k) b o≤-refl ))
+                     x<sup' :  {w : HOD} → UnionCF A f mf ay supf0 x ∋ w → (w ≡  (SUP.sup zc9) ) ∨ (w < (SUP.sup zc9) )
+                     x<sup' {q} uw = SUP.x<sup zc9 uw
                      x<sup :  {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ * (supf0 px) ) ∨ (w < * (supf0 px) )
                      x<sup {w} ⟪ aw , ch-init fc ⟫ = ?
-                     x<sup {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = ?
+                     x<sup {w} ⟪ aw , ch-is-sup u u≤z is-sup fc ⟫ = ?
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
@@ -841,7 +834,7 @@
                 zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
                 zc12  = ?
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 = ⟪ az , ch-is-sup z z<x cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
+                zc11 = ⟪ az , ch-is-sup z ? cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
                       az : odef A ( ZChain.supf ozc z )
                       az = proj1 zc12
                       zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
@@ -896,6 +889,7 @@
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!} 
                ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension -- ¬ A ∋ p, just skip