Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 127:870fe02c7a07
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jul 2019 16:03:15 +0900 |
| parents | 5f97ebaeb89b |
| children | 2a5519dcc167 |
line wrap: on
line diff
--- a/ordinal.agda Mon Jul 01 01:27:25 2019 +0900 +++ b/ordinal.agda Mon Jul 01 16:03:15 2019 +0900 @@ -170,6 +170,12 @@ maxαd x y | tri≈ ¬a b ¬c = x maxαd x y | tri> ¬a ¬b c = x +minαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx +minαd x y with triOrdd x y +minαd x y | tri< a ¬b ¬c = x +minαd x y | tri≈ ¬a b ¬c = y +minαd x y | tri> ¬a ¬b c = x + _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) a o≤ b = (a ≡ b) ∨ ( a o< b ) @@ -212,10 +218,15 @@ maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal maxα x y with <-cmp (lv x) (lv y) -maxα x y | tri< a ¬b ¬c = x -maxα x y | tri> ¬a ¬b c = y +maxα x y | tri< a ¬b ¬c = y +maxα x y | tri> ¬a ¬b c = x maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } +minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal +minα x y with <-cmp (lv x) (lv y) +minα x y | tri< a ¬b ¬c = x +minα x y | tri> ¬a ¬b c = y +minα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = minαd (ord x) (ord y) } -- -- max ( osuc x , osuc y ) --