# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687990112 -32400
# Node ID d9eb3ae5fbad91fbc6a2b03da530a7c95a3856d1
# Parent  34f72406fcfd5323bf5302ec560330fddaa5b785
...

diff -r 34f72406fcfd -r d9eb3ae5fbad src/cardinal.agda
--- a/src/cardinal.agda	Thu Jun 29 02:36:06 2023 +0900
+++ b/src/cardinal.agda	Thu Jun 29 07:08:32 2023 +0900
@@ -308,10 +308,16 @@
                           be30 : CN (fba x bx) → ⊥ 
                           be30 = ncn
                           be25 : ¬ CN (g⁻¹ agx be22)  
-                          be25 = ? where
-                             be26 : (i : ℕ) (y : Ordinal) (ay : odef (* a) y)  ( gfi : gfImage i  y ) → ¬ CN (fab y ay )  → ⊥
-                             be26 0 y ay (a-g ax ¬ib) ncy = ?
-                             be26 (suc i) y ay (next-gf record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } gfi) ncy = be26 i y1 ay1 gfi ?
+                          be25 cn = be26 (CN.i cn) _ ? (CN.gfix cn) ?  where
+                             be26 : (i : ℕ) (y : Ordinal) (ay : odef (* a) y)  ( gfi : gfImage i  y ) → ¬ CN y  → ⊥
+                             be26 0 y ay (a-g ax ¬ib) ncy = ⊥-elim ( ncy record { i = 0 ; gfix = a-g ax ¬ib } )
+                             be26 (suc i) y ay (next-gf record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } gfi) ncy = be26 i y1 ay1 gfi be27 where
+                                 be27 : ¬ (CN y1)
+                                 be27 cn with CN.i cn | CN.gfix cn
+                                 ... | 0 | t @ (a-g ax ¬ib) = ncy record { i = suc 0 
+                                    ; gfix = next-gf record { y = y1 ; ay = ax ; x=fy = trans x=fy1 (fba-eq (fab-eq refl)) }  t }
+                                 ... | suc i | t @ (next-gf ix t1) = ncy record { i = suc (suc i) 
+                                    ; gfix = next-gf record { y = y1 ; ay = a∋gfImage _ t ; x=fy = trans x=fy1 (fba-eq (fab-eq refl)) } t }
                           be23 : ¬ CN (g⁻¹ agx be22)  -- g⁻¹ (g x ) -- ¬ CN x
                           be23 cng with CN.i cng | CN.gfix cng
                           ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = ? ; ay = ? ; x=fy = ? } )