Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1402:d9eb3ae5fbad
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Jun 2023 07:08:32 +0900 |
| parents | 34f72406fcfd |
| children | 5476e93726e3 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 10 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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 = ? } )