# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665050384 -32400
# Node ID 37ddab37e189bb1238d4f47550fb106265941a07
# Parent  f52c610cca068ea2d255477d88c1fb726636c349
...

diff -r f52c610cca06 -r 37ddab37e189 src/zorn.agda
--- a/src/zorn.agda	Thu Oct 06 18:44:18 2022 +0900
+++ b/src/zorn.agda	Thu Oct 06 18:59:44 2022 +0900
@@ -676,6 +676,10 @@
               ... | case2 lt = lt
               ... | case1 eq = ⊥-elim ( <-irr (case1 (sym m11)) m12 ) where 
                     ---    supf b ≡ supf x     * ( supf x ) ≤ * a < * b , * (supf x) ≡ * (supf b) ≡ * b
+                    ---    xchain = UnionCF A f mf ay supf x
+                    ---       {y : Ordinal} → odef xchain y → (y ≡ b ) ∨ (y < * b )
+                    ---     supf x ∈ xchian → ok
+                    ---   ¬ supf x ∈ xchian → ⊥ 
                     m10 : {a : Ordinal} → odef  (UnionCF A f mf ay supf x) a  → * ( supf x ) ≤ * a
                     m10 {a} ⟪ ua , ch-init fc ⟫ = ?
                     m10 {a} ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?