Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 987:c8c60a05b39b
is-max?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 13 Nov 2022 10:23:50 +0900 |
| parents | 557f8145d3c1 |
| children | 9a85233384f7 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 12 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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