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

changeset 659:b8dca06b6372

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Jul 2022 22:44:13 +0900
parents a7a0df28086d
children fe6e36ea0254
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Jul 02 18:50:11 2022 +0900
+++ b/src/zorn.agda	Sat Jul 02 22:44:13 2022 +0900
@@ -612,7 +612,9 @@
               {λ x → z o≤ x → { cx : HOD } → (Cx : Chain A f ay x cx )  → cx ⊆' cz } (u-mono-ind z Cz) x z≤x Cx 
          u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
          u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
-         ... | s | t = ?
+         ... | tri< a ¬b ¬c | t = ?
+         ... | tri≈ ¬a b ¬c | t = ?
+         ... | tri> ¬a ¬b c | t = ?
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay   z  } (λ x → ind f mf ay x ) (& A)