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

comparison src/OrdUtil.agda @ 715:e4587714c376

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, 15 Jul 2022 14:14:53 +0900
parents 92275389e623
children ddeb107b6f71
comparison
equal deleted inserted replaced
714:e1ef5e6961ce 715:e4587714c376
44 44
45 ¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) ) 45 ¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) )
46 ¬p<x<op {p} {b} P with osuc-≡< (proj2 P) 46 ¬p<x<op {p} {b} P with osuc-≡< (proj2 P)
47 ... | case1 eq = o<¬≡ (sym eq) (proj1 P) 47 ... | case1 eq = o<¬≡ (sym eq) (proj1 P)
48 ... | case2 lt = o<> lt (proj1 P) 48 ... | case2 lt = o<> lt (proj1 P)
49
50 b<x→0<x : { p b : Ordinal } → p o< b → o∅ o< b
51 b<x→0<x {p} {b} p<b with trio< o∅ b
52 ... | tri< a ¬b ¬c = a
53 ... | tri≈ ¬a 0=b ¬c = ⊥-elim ( ¬x<0 ( subst (λ k → p o< k) (sym 0=b) p<b ) )
54 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
49 55
50 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox 56 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox
51 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox 57 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
52 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc 58 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
53 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc 59 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc