Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
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 |