Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 420:53422a8ea836
bijection
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 31 Jul 2020 17:42:25 +0900 |
| parents | aa306f5dab9b |
| children | 9984cdd88da3 |
line wrap: on
line diff
--- a/Ordinals.agda Fri Jul 31 12:57:59 2020 +0900 +++ b/Ordinals.agda Fri Jul 31 17:42:25 2020 +0900 @@ -313,6 +313,12 @@ omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz + nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny) + nn<omax {x} {nx} {ny} xnx xny with trio< nx ny + nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny + nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny + nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx + record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where field os→ : (x : Ordinal) → x o< maxordinal → Ordinal