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

changeset 352:e27769992399

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
next-is-limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 11:12:09 +0900
parents 08d94fec239c
children e4b7485b0b17
files Ordinals.agda
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Ordinals.agda	Tue Jul 14 07:59:17 2020 +0900
+++ b/Ordinals.agda	Tue Jul 14 11:12:09 2020 +0900
@@ -251,6 +251,11 @@
         nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
            (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
 
+        next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
+        next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
+            y<nx : y o< next x
+            y<nx = osuc< (sym eq)
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal