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

comparison Ordinals.agda @ 411:6eaab908130e

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, 29 Jul 2020 21:51:00 +0900
parents 6dcea4c7cba1
children aa306f5dab9b
comparison
equal deleted inserted replaced
410:6dcea4c7cba1 411:6eaab908130e
170 omax< x y lt with trio< x y 170 omax< x y lt with trio< x y
171 omax< x y lt | tri< a ¬b ¬c = refl 171 omax< x y lt | tri< a ¬b ¬c = refl
172 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) 172 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
173 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) 173 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
174 174
175 omax≤ : ( x y : Ordinal ) → x o≤ y → osuc y ≡ omax x y
176 omax≤ x y le with trio< x y
177 omax≤ x y le | tri< a ¬b ¬c = refl
178 omax≤ x y le | tri≈ ¬a refl ¬c = refl
179 omax≤ x y le | tri> ¬a ¬b c with osuc-≡< le
180 omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
181 omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y)
182
175 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y 183 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y
176 omax≡ x y eq with trio< x y 184 omax≡ x y eq with trio< x y
177 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) 185 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
178 omax≡ x y eq | tri≈ ¬a refl ¬c = refl 186 omax≡ x y eq | tri≈ ¬a refl ¬c = refl
179 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) 187 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
271 ⊥-elim ( ¬nx<nx y<nx a (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 279 ⊥-elim ( ¬nx<nx y<nx a (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
272 x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b 280 x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
273 x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c = -- x < y < next y < next x 281 x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c = -- x < y < next y < next x
274 ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 282 ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
275 283
276 ≤next : {x y : Ordinal} → x o< y → next x o≤ next y 284 ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
277 ≤next {x} {y} x<y with trio< (next x) y 285 ≤next {x} {y} x≤y with trio< (next x) y
278 ≤next {x} {y} x<y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc ) 286 ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
279 ≤next {x} {y} x<y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc ) 287 ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
280 ≤next {x} {y} x<y | tri> ¬a ¬b c = o≤-refl (x<ny→≡next x<y c) 288 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
289 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl -- x = y < next x
290 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x
281 291
282 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y 292 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
283 x<ny→≤next {x} {y} x<ny with trio< x y 293 x<ny→≤next {x} {y} x<ny with trio< x y
284 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next a 294 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc )
285 x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl refl 295 x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl refl
286 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny )) 296 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))
287 297
288 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y ) 298 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
289 omax<nomax {x} {y} with trio< x y 299 omax<nomax {x} {y} with trio< x y