Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 411:6eaab908130e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 Jul 2020 21:51:00 +0900 |
| parents | 6dcea4c7cba1 |
| children | aa306f5dab9b |
line wrap: on
line diff
--- a/Ordinals.agda Wed Jul 29 12:42:05 2020 +0900 +++ b/Ordinals.agda Wed Jul 29 21:51:00 2020 +0900 @@ -172,6 +172,14 @@ omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) + omax≤ : ( x y : Ordinal ) → x o≤ y → osuc y ≡ omax x y + omax≤ x y le with trio< x y + omax≤ x y le | tri< a ¬b ¬c = refl + omax≤ x y le | tri≈ ¬a refl ¬c = refl + omax≤ x y le | tri> ¬a ¬b c with osuc-≡< le + omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq) + omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y) + omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y omax≡ x y eq with trio< x y omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) @@ -273,15 +281,17 @@ x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c = -- x < y < next y < next x ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) - ≤next : {x y : Ordinal} → x o< y → next x o≤ next y - ≤next {x} {y} x<y with trio< (next x) y - ≤next {x} {y} x<y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc ) - ≤next {x} {y} x<y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc ) - ≤next {x} {y} x<y | tri> ¬a ¬b c = o≤-refl (x<ny→≡next x<y c) + ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y + ≤next {x} {y} x≤y with trio< (next x) y + ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc ) + ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc ) + ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y + ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl -- x = y < next x + ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y x<ny→≤next {x} {y} x<ny with trio< x y - x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next a + x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc ) x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl refl x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))