Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 826:da99e787cb7a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 18 Aug 2022 18:20:54 +0900 |
| parents | eec82adba99b |
| children | 685f7ae1b821 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 11 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Aug 18 18:09:15 2022 +0900 +++ b/src/zorn.agda Thu Aug 18 18:20:54 2022 +0900 @@ -321,16 +321,20 @@ ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where zc06 : supf u ≡ u zc06 = ChainP.supu=u is-sup - u≤b : u o≤ supf s → u o≤ b - u≤b u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s) - ... | case1 su=ss = o<→≤ (supf-inject zc08 ) where + zc09 : u o≤ supf s → ( u o≤ b ) ∨ ( supf u ≡ supf b ) + zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s) + ... | case1 su=ss = zc08 where zc07 : supf u o≤ supf b zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono (o<→≤ s<b) ) - zc08 : supf u o< supf b + zc08 : ( u o≤ b ) ∨ ( supf u ≡ supf b ) zc08 with osuc-≡< zc07 - ... | case1 su=sb = ? - ... | case2 lt = lt - ... | case2 lt = o<→≤ (ordtrans (supf-inject lt) s<b) + ... | case1 su=sb = case2 su=sb + ... | case2 lt = case1 ( o<→≤ (supf-inject lt )) + ... | case2 lt = case1 ( o<→≤ (ordtrans (supf-inject lt) s<b) ) + zc10 : odef (UnionCF A f mf ay supf b) (supf s) + zc10 with zc09 u≤x + ... | case1 lt = ⟪ as , ch-is-sup u lt is-sup fc ⟫ + ... | case2 eq = ⟪ as , ch-is-sup u ? is-sup ? ⟫ zc03 : odef (UnionCF A f mf ay supf b) (supf s) zc03 with csupf (o<→≤ s<z) ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫