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

comparison src/OrdUtil.agda @ 796:171123c92007

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 Fri, 05 Aug 2022 17:57:41 +0900
parents a08c456d49d0
children d70f3f0681ea
comparison
equal deleted inserted replaced
795:408e7e8a3797 796:171123c92007
55 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 55 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
56 56
57 ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x 57 ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x
58 ob<x {b} {x} lim b<x with trio< (osuc b) x 58 ob<x {b} {x} lim b<x with trio< (osuc b) x
59 ... | tri< a ¬b ¬c = a 59 ... | tri< a ¬b ¬c = a
60 ... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x } ) 60 ... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x } )
61 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ ) 61 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )
62 62
63 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox 63 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox
64 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox 64 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
65 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc 65 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc