Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 973:2a67cae517d8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 07 Nov 2022 17:56:03 +0900
parents 520aff512969
children 9bfe54cd9fb9 94357ced682d
files src/zorn.agda
diffstat 1 files changed, 2 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Nov 07 16:08:29 2022 +0900
+++ b/src/zorn.agda	Mon Nov 07 17:56:03 2022 +0900
@@ -1221,6 +1221,8 @@
                            cs11 : px o< z1 →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
                            cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) 
                               (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 )))  sfpx≤sp1 ) sz1<x) ⟫ )
+                           cs12 : z1 o≤ px →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
+                           cs12 = ?
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?