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

comparison src/OrdUtil.agda @ 789:a08c456d49d0

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 Wed, 03 Aug 2022 01:49:34 +0900
parents d92ad9e365b6
children 171123c92007
comparison
equal deleted inserted replaced
788:c164f4f7cfd1 789:a08c456d49d0
82 ordtrans<-≤ : {ox oy oz : Ordinal } → ox o< oy → oy o< osuc oz → ox o< oz 82 ordtrans<-≤ : {ox oy oz : Ordinal } → ox o< oy → oy o< osuc oz → ox o< oz
83 ordtrans<-≤ {ox} {oy} {oz} x<y y≤z with osuc-≡< y≤z 83 ordtrans<-≤ {ox} {oy} {oz} x<y y≤z with osuc-≡< y≤z
84 ... | case1 x=y = subst ( λ k → ox o< k ) (x=y) x<y 84 ... | case1 x=y = subst ( λ k → ox o< k ) (x=y) x<y
85 ... | case2 y<z = ordtrans x<y y<z 85 ... | case2 y<z = ordtrans x<y y<z
86 86
87 open _∧_ 87 o∅≤z : {z : Ordinal } → o∅ o< (osuc z)
88 o∅≤z {z} = b<x→0<x ( <-osuc )
88 89
89 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) 90 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
90 proj2 (osuc2 x y) lt = osucc lt 91 proj2 (osuc2 x y) lt = osucc lt
91 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy 92 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
92 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy 93 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy