# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668302630 -32400
# Node ID c8c60a05b39b72ead721dd83d8297c9c13c6c40b
# Parent  557f8145d3c110b21648cbea02a1595b7d72d555
is-max?

diff -r 557f8145d3c1 -r c8c60a05b39b src/zorn.agda
--- a/src/zorn.agda	Sat Nov 12 18:11:14 2022 +0900
+++ b/src/zorn.agda	Sun Nov 13 10:23:50 2022 +0900
@@ -1433,11 +1433,19 @@
           ... | case1 sc=sa = ⊥-elim (  nmx record { maximal = * d ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm spd) 
                 ; ¬maximal<x = λ {x} ax → subst₂ (λ j k → ¬ ( j < k)) refl *iso (zc10 sc=sa ax) } ) where 
              zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x  → ¬ ( d << x )
-             zc10 = ? --    supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c
+             zc10 = ? where 
+                  zc11 : {z : Ordinal } →  odef (ZChain.chain zc) z → supf z o< supf (& A) 
+                  zc11 = ?
+                  sc≤c : c o≤ supf c 
+                  sc≤c = MinSUP.minsup msp1 ? ?
+                  sc=c : supf c ≡ c
+                  sc=c = ?
+                  d≤c : c o≤ d
+                  d≤c = MinSUP.minsup msp1 ? ?
+                    --    supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c
                     --      c << x → x is sup of chain or x = f ( .. ( f c ))
-                    --      c << x → x is not in chain
-                    --      supf c o≤ x (minimulity)
-                    --  odef chain z → supf z o< supf (& A) ≡ supf c → minimulity  c o≤ supf c 
+                    --      c o≤ x (by minimulity)
+                    --  odef chain z → supf z o< supf (& A) ≡ supf c → supf c is sup of chain, by minimulity  c o≤ supf c 
                     --   supf c o≤ supf (supf c) o≤ supf x o≤ supf (& A)
                     --   supf c ≡ supf (supf c) ≡ supf x  ≡ supf (& A)  means supf of FClosure of (supf c) is Maximal