Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/OrdUtil.agda @ 796:171123c92007
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 05 Aug 2022 17:57:41 +0900 |
parents | a08c456d49d0 |
children | d70f3f0681ea |
line wrap: on
line diff
--- a/src/OrdUtil.agda Fri Aug 05 16:21:46 2022 +0900 +++ b/src/OrdUtil.agda Fri Aug 05 17:57:41 2022 +0900 @@ -57,7 +57,7 @@ ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x ob<x {b} {x} lim b<x with trio< (osuc b) x ... | tri< a ¬b ¬c = a -... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x } ) +... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x } ) ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ ) osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox