Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/OrdUtil.agda @ 1286:619e68271cf8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 May 2023 19:06:25 +0900 |
| parents | a8d6ac036d88 |
| children |
comparison
equal
deleted
inserted
replaced
| 1285:302cfb533201 | 1286:619e68271cf8 |
|---|---|
| 257 nexto∅ {x} with trio< o∅ x | 257 nexto∅ {x} with trio< o∅ x |
| 258 nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx | 258 nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx |
| 259 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx | 259 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx |
| 260 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | 260 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) |
| 261 | 261 |
| 262 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z | |
| 263 next< {x} {y} {z} x<nz y<nx with trio< y (next z) | |
| 264 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a | |
| 265 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx) | |
| 266 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) )))) | |
| 267 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx ) | |
| 268 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) | |
| 269 | |
| 270 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y | 262 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y |
| 271 osuc< {x} {y} refl = <-osuc | 263 osuc< {x} {y} refl = <-osuc |
| 272 | 264 |
| 273 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y | 265 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y |
| 274 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy | 266 nexto=n {x} {y} lt = subst (λ k → x o< k ) (sym nexto≡) lt |
| 275 | |
| 276 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) | |
| 277 nexto≡ {x} with trio< (next x) (next (osuc x) ) | |
| 278 -- next x o< next (osuc x ) -> osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x | |
| 279 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a | |
| 280 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) | |
| 281 nexto≡ {x} | tri≈ ¬a b ¬c = b | |
| 282 -- next (osuc x) o< next x -> osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ... | |
| 283 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c | |
| 284 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) | |
| 285 | 267 |
| 286 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) | 268 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) |
| 287 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where | 269 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where |
| 288 y<nx : y o< next x | 270 y<nx : y o< next x |
| 289 y<nx = osuc< (sym eq) | 271 y<nx = osuc< (sym eq) |
| 290 | 272 |
| 291 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y | 273 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y |
| 292 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx) | 274 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx) |
| 293 | 275 |
| 294 x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y | 276 -- x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y |
| 295 x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y) | 277 -- x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y) |
| 296 x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c = -- x < y < next x < next y ∧ next x = osuc z | 278 -- x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c = -- x < y < next x < next y ∧ next x = osuc z |
| 297 ⊥-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 )))) |
| 298 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 |
| 299 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 |
| 300 ⊥-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 )))) |
| 301 | 283 |
| 302 ≤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 |
| 303 ≤next {x} {y} x≤y with trio< (next x) y | 285 -- ≤next {x} {y} x≤y with trio< (next x) y |
| 304 ≤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 ) |
| 305 ≤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 ) |
| 306 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y | 288 -- ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y |
| 307 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x | 289 -- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x |
| 308 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x | 290 -- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x |
| 309 | 291 |
| 310 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 |
| 311 x<ny→≤next {x} {y} x<ny with trio< x y | 293 -- x<ny→≤next {x} {y} x<ny with trio< x y |
| 312 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc ) | 294 -- x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc ) |
| 313 x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl | 295 -- x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl |
| 314 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny )) | 296 -- x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny )) |
| 315 | 297 |
| 316 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 ) |
| 317 omax<nomax {x} {y} with trio< x y | 299 -- omax<nomax {x} {y} with trio< x y |
| 318 omax<nomax {x} {y} | tri< a ¬b ¬c = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx ) | 300 -- omax<nomax {x} {y} | tri< a ¬b ¬c = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx ) |
| 319 omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) | 301 -- omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) |
| 320 omax<nomax {x} {y} | tri> ¬a ¬b c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) | 302 -- omax<nomax {x} {y} | tri> ¬a ¬b c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) |
| 321 | 303 |
| 322 omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z | 304 omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z |
| 323 omax<nx {x} {y} {z} x<nz y<nz with trio< x y | 305 omax<nx {x} {y} {z} x<nz y<nz with trio< x y |
| 324 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz | 306 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz |
| 325 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz | 307 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz |
| 326 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz | 308 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz |
| 327 | 309 |
| 328 nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny) | 310 -- nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny) |
| 329 nn<omax {x} {nx} {ny} xnx xny with trio< nx ny | 311 -- nn<omax {x} {nx} {ny} xnx xny with trio< nx ny |
| 330 nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny | 312 -- nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny |
| 331 nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny | 313 -- nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny |
| 332 nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx | 314 -- nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx |
| 333 | 315 |
| 334 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where | 316 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where |
| 335 field | 317 field |
| 336 os→ : (x : Ordinal) → x o< maxordinal → Ordinal | 318 os→ : (x : Ordinal) → x o< maxordinal → Ordinal |
| 337 os← : Ordinal → Ordinal | 319 os← : Ordinal → Ordinal |