Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1087:2fa98e3c0fa3
order may come from supf-idem
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 18 Dec 2022 10:32:29 +0900 |
parents | 7ec55b1bdfc2 |
children | 125605b5bf47 |
comparison
equal
deleted
inserted
replaced
1086:9e8cb06f0aff | 1087:2fa98e3c0fa3 |
---|---|
340 | 340 |
341 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) | 341 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) |
342 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where | 342 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where |
343 field | 343 field |
344 supf : Ordinal → Ordinal | 344 supf : Ordinal → Ordinal |
345 | |
346 cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w | |
347 order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b | |
348 | |
349 asupf : {x : Ordinal } → odef A (supf x) | 345 asupf : {x : Ordinal } → odef A (supf x) |
346 | |
350 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y | 347 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y |
351 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x | 348 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x |
352 | |
353 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) | 349 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) |
350 cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w | |
351 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b | |
354 | 352 |
355 chain : HOD | 353 chain : HOD |
356 chain = UnionCF A f ay supf z | 354 chain = UnionCF A f ay supf z |
357 chain⊆A : chain ⊆' A | 355 chain⊆A : chain ⊆' A |
358 chain⊆A = λ lt → proj1 lt | 356 chain⊆A = λ lt → proj1 lt |
397 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) | 395 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) |
398 | 396 |
399 initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x → y ≤ x | 397 initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x → y ≤ x |
400 initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc | 398 initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc |
401 initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc) | 399 initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc) |
400 | |
401 supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b | |
402 supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b) | |
403 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( | |
404 IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) | |
405 ... | tri≈ ¬a b ¬c = b | |
406 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( | |
407 IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) | |
408 | |
409 union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b | |
410 union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where | |
411 z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w | |
412 z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
413 z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where | |
414 u<b : u o< b | |
415 u<b = ordtrans u<a (supf-inject sa<sb ) | |
416 z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w | |
417 z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
418 z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where | |
419 u<a : u o< a | |
420 u<a = supf-inject ( osucprev (begin | |
421 osuc (supf u) ≡⟨ cong osuc su=u ⟩ | |
422 osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ | |
423 z ≤⟨ z≤sa ⟩ | |
424 supf a ∎ )) where open o≤-Reasoning O | |
425 | |
426 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z | |
427 → IsSUP A (UnionCF A f ay supf b) b → supf b ≡ b | |
428 sup=u {b} ab b≤z is-sup = z50 where | |
429 z48 : supf b o≤ b | |
430 z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux ) | |
431 z50 : supf b ≡ b | |
432 z50 with trio< (supf b) b | |
433 ... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where | |
434 z47 : b o≤ supf b | |
435 z47 = zo≤sz b≤z | |
436 ... | tri≈ ¬a b ¬c = b | |
437 ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) | |
438 | |
439 x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x | |
440 x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x | |
441 ... | case2 le = le | |
442 ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where | |
443 z46 : odef (UnionCF A f ay supf x) (f (supf x)) | |
444 z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where | |
445 z47 : supf (supf x) ≡ supf x | |
446 z47 = supf-idem x≤z sx≤z | |
447 z45 : f (supf x) ≤ supf x | |
448 z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 | |
449 | |
450 order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b | |
451 order {a} {b} {w} b≤z sa<sb fc with x<y∨y≤x (supf a) z | |
452 ... | case2 z≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where | |
453 z27 : supf a ≡ supf b | |
454 z27 = supfeq (OrdTrans (o<→≤ (supf-inject sa<sb)) b≤z) b≤z ( union-max z≤sa b≤z sa<sb) | |
455 ... | case1 sa<z = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where | |
456 sa<b : supf a o< b | |
457 sa<b with x<y∨y≤x (supf a) b | |
458 ... | case1 lt = lt | |
459 ... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin | |
460 osuc (supf (supf a)) ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) (o<→≤ sa<z)) ⟩ | |
461 osuc (supf a) ≤⟨ osucc sa<sb ⟩ | |
462 supf b ∎ )))) where open o≤-Reasoning O | |
463 | |
464 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b | |
465 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) | |
466 ... | case2 lt = lt | |
467 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) | |
402 | 468 |
403 f-total : IsTotalOrderSet chain | 469 f-total : IsTotalOrderSet chain |
404 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = | 470 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = |
405 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where | 471 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where |
406 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) | 472 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) |
436 b<a = subst₂ (λ j k → j < k ) *iso *iso lt | 502 b<a = subst₂ (λ j k → j < k ) *iso *iso lt |
437 ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) | 503 ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) |
438 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) | 504 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) |
439 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = | 505 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = |
440 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb ) | 506 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb ) |
441 | |
442 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b | |
443 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) | |
444 ... | case2 lt = lt | |
445 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) | |
446 | |
447 supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b | |
448 supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b) | |
449 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( | |
450 IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) | |
451 ... | tri≈ ¬a b ¬c = b | |
452 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( | |
453 IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) | |
454 | |
455 union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b | |
456 union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where | |
457 z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w | |
458 z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
459 z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where | |
460 u<b : u o< b | |
461 u<b = ordtrans u<a (supf-inject sa<sb ) | |
462 z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w | |
463 z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
464 z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where | |
465 u<a : u o< a | |
466 u<a = supf-inject ( osucprev (begin | |
467 osuc (supf u) ≡⟨ cong osuc su=u ⟩ | |
468 osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ | |
469 z ≤⟨ z≤sa ⟩ | |
470 supf a ∎ )) where open o≤-Reasoning O | |
471 | |
472 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z | |
473 → IsSUP A (UnionCF A f ay supf b) b → supf b ≡ b | |
474 sup=u {b} ab b≤z is-sup = z50 where | |
475 z48 : supf b o≤ b | |
476 z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux ) | |
477 z50 : supf b ≡ b | |
478 z50 with trio< (supf b) b | |
479 ... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where | |
480 z47 : b o≤ supf b | |
481 z47 = zo≤sz b≤z | |
482 ... | tri≈ ¬a b ¬c = b | |
483 ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) | |
484 | |
485 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b | |
486 supf-idem {b} b≤z sfb≤x = z52 where | |
487 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) | |
488 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc | |
489 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z (subst (λ k → k o< supf b) (sym su=u) u<x) fc where | |
490 u<b : u o< b | |
491 u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) | |
492 z52 : supf (supf b) ≡ supf b | |
493 z52 = sup=u asupf sfb≤x record { ax = asupf ; x≤sup = z54 } | |
494 | |
495 x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x | |
496 x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x | |
497 ... | case2 le = le | |
498 ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where | |
499 z46 : odef (UnionCF A f ay supf x) (f (supf x)) | |
500 z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where | |
501 z47 : supf (supf x) ≡ supf x | |
502 z47 = supf-idem x≤z sx≤z | |
503 z45 : f (supf x) ≤ supf x | |
504 z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 | |
505 | |
506 order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b | |
507 order0 {a} {b} {w} b≤z sa<sb sa≤z fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where | |
508 sa<b : supf a o< b | |
509 sa<b with x<y∨y≤x (supf a) b | |
510 ... | case1 lt = lt | |
511 ... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin | |
512 osuc (supf (supf a)) ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) sa≤z) ⟩ | |
513 osuc (supf a) ≤⟨ osucc sa<sb ⟩ | |
514 supf b ∎ )))) where open o≤-Reasoning O | |
515 | 507 |
516 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) | 508 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) |
517 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where | 509 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where |
518 supf = ZChain.supf zc | 510 supf = ZChain.supf zc |
519 field | 511 field |
1116 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x | 1108 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x |
1117 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where | 1109 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where |
1118 u≤px : u o≤ px | 1110 u≤px : u o≤ px |
1119 u≤px = ordtrans u<x z≤px | 1111 u≤px = ordtrans u<x z≤px |
1120 | 1112 |
1121 supfeq1 : {a b : Ordinal } → a o≤ x → b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b | |
1122 supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b) | |
1123 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( | |
1124 IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) | |
1125 ... | tri≈ ¬a b ¬c = b | |
1126 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( | |
1127 IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) | |
1128 | |
1129 union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b | |
1130 union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where | |
1131 z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w | |
1132 z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
1133 z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where | |
1134 u<b : u o< b | |
1135 u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb ) | |
1136 z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w | |
1137 z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
1138 z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where | |
1139 u<a : u o< a | |
1140 u<a = supf-inject0 supf1-mono ( osucprev (begin | |
1141 osuc (supf1 u) ≡⟨ cong osuc su=u ⟩ | |
1142 osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ | |
1143 x ≤⟨ z≤sa ⟩ | |
1144 supf1 a ∎ )) where open o≤-Reasoning O | |
1145 | |
1146 | |
1147 zo≤sz : {z : Ordinal} → z o≤ x → z o≤ supf1 z | 1113 zo≤sz : {z : Ordinal} → z o≤ x → z o≤ supf1 z |
1148 zo≤sz {z} z≤x with osuc-≡< z≤x | 1114 zo≤sz {z} z≤x with osuc-≡< z≤x |
1149 ... | case2 z<x = subst (λ k → z o≤ k) (sym (sf1=sf0 (zc-b<x _ z<x ))) (ZChain.zo≤sz zc (zc-b<x _ z<x )) | 1115 ... | case2 z<x = subst (λ k → z o≤ k) (sym (sf1=sf0 (zc-b<x _ z<x ))) (ZChain.zo≤sz zc (zc-b<x _ z<x )) |
1150 ... | case1 refl with osuc-≡< (supf1-mono (o<→≤ (px<x))) -- px o≤ supf1 px o≤ supf1 x ≡ sp1 → x o≤ sp1 | 1116 ... | case1 refl with osuc-≡< (supf1-mono (o<→≤ (px<x))) -- px o≤ supf1 px o≤ supf1 x ≡ sp1 → x o≤ sp1 |
1151 ... | case2 lt = begin | 1117 ... | case2 lt = begin |
1172 sp1 ∎ where open ≡-Reasoning | 1138 sp1 ∎ where open ≡-Reasoning |
1173 zc40 : f (supf0 px) ≤ supf0 px | 1139 zc40 : f (supf0 px) ≤ supf0 px |
1174 zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) | 1140 zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) |
1175 ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫ )) | 1141 ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫ )) |
1176 | 1142 |
1177 order : {a b : Ordinal} {w : Ordinal} → | |
1178 b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b | |
1179 order {a} {b} {w} b≤x sa<sb fc = z20 where | |
1180 a<b : a o< b | |
1181 a<b = supf-inject0 supf1-mono sa<sb | |
1182 a≤px : a o≤ px | |
1183 a≤px with trio< a px | |
1184 ... | tri< a ¬b ¬c = o<→≤ a | |
1185 ... | tri≈ ¬a b ¬c = o≤-refl0 b | |
1186 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op)) | |
1187 ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x | |
1188 z20 : w ≤ supf1 b | |
1189 z20 with trio< b px | |
1190 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) | |
1191 (fcup fc (o<→≤ (ordtrans a<b b<px))) | |
1192 ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where | |
1193 a≤x : a o≤ x | |
1194 a≤x = o<→≤ (ordtrans ( subst (λ k → a o< k ) b=px a<b ) px<x ) | |
1195 z26 : odef ( UnionCF A f ay supf0 b ) w | |
1196 z26 with x<y∨y≤x (supf1 a) b | |
1197 ... | case2 b≤sa = z27 where | |
1198 z27 : odef (UnionCF A f ay supf0 b) w | |
1199 z27 with osuc-≡< b≤sa | |
1200 ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x | |
1201 ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px))) sa<sb) )) | |
1202 (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where | |
1203 x≤sa : x o≤ supf1 a | |
1204 x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa ) | |
1205 ... | case1 b=sa = ⊥-elim (o<¬≡ sa=sb sa<sb) where | |
1206 sa=sb : supf1 a ≡ supf0 b | |
1207 sa=sb = begin | |
1208 supf1 a ≡⟨ sf1=sf0 a≤px ⟩ | |
1209 supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px (o≤-refl0 (sym (trans (sym b=px) (trans b=sa (sf1=sf0 a≤px) ))))) ⟩ | |
1210 supf0 (supf0 a) ≡⟨ cong supf0 (sym (sf1=sf0 a≤px )) ⟩ | |
1211 supf0 (supf1 a) ≡⟨ cong supf0 (sym b=sa) ⟩ | |
1212 supf0 b ∎ where open ≡-Reasoning | |
1213 ... | case1 sa<b with cfcs a<b b≤x sa<b fc | |
1214 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ | |
1215 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px)) su=u) (fcup fc u≤px) ⟫ where | |
1216 u≤px : u o≤ px | |
1217 u≤px = o<→≤ ( subst (λ k → u o< k ) b=px u<x ) | |
1218 ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b | |
1219 ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) | |
1220 ... | case2 b≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x=b x o≤ sa UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥ | |
1221 b=x : b ≡ x | |
1222 b=x with trio< b x | |
1223 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ a ⟫ ) -- px o< b o< x | |
1224 ... | tri≈ ¬a b ¬c = b | |
1225 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b ≤ x | |
1226 a≤x : a o≤ x | |
1227 a≤x = o<→≤ ( subst (λ k → a o< k ) b=x a<b ) | |
1228 sf1b=sp1 : supf1 b ≡ sp1 | |
1229 sf1b=sp1 = sf1=sp1 (subst (λ k → px o< k) (trans (Oprev.oprev=x op) (sym b=x)) <-osuc) | |
1230 z27 : supf1 a ≡ sp1 | |
1231 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) | |
1232 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1 | |
1233 | |
1234 ... | no lim with trio< x o∅ | 1143 ... | no lim with trio< x o∅ |
1235 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 1144 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1236 ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) | 1145 ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) |
1237 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) | 1146 ; supf-mono = λ _ → o≤-refl |
1238 ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0))) } where | 1147 ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0))) } where |
1239 mf : ≤-monotonic-f A f | 1148 mf : ≤-monotonic-f A f |
1240 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where | 1149 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where |
1241 mf00 : * x < * (f x) | 1150 mf00 : * x < * (f x) |
1242 mf00 = proj1 ( mf< x ax ) | 1151 mf00 = proj1 ( mf< x ax ) |
1643 z50 = o≤-refl0 z49 | 1552 z50 = o≤-refl0 z49 |
1644 z48 : odef pchainU (f spu) | 1553 z48 : odef pchainU (f spu) |
1645 z48 = ⟪ proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50 | 1554 z48 = ⟪ proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50 |
1646 (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫ | 1555 (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫ |
1647 | 1556 |
1648 supfeq1 : {a b : Ordinal } → a o≤ x → b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b | |
1649 supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b) | |
1650 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( | |
1651 IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) | |
1652 ... | tri≈ ¬a b ¬c = b | |
1653 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( | |
1654 IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) | |
1655 | |
1656 union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b | |
1657 union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where | |
1658 z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w | |
1659 z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
1660 z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where | |
1661 u<b : u o< b | |
1662 u<b = ordtrans u<a (supf-inject0 supf-mono sa<sb ) | |
1663 z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w | |
1664 z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
1665 z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where | |
1666 u<a : u o< a | |
1667 u<a = supf-inject0 supf-mono ( osucprev (begin | |
1668 osuc (supf1 u) ≡⟨ cong osuc su=u ⟩ | |
1669 osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ | |
1670 x ≤⟨ z≤sa ⟩ | |
1671 supf1 a ∎ )) where open o≤-Reasoning O | |
1672 | |
1673 order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b | |
1674 order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x | |
1675 ... | case2 b<x = subst (λ k → w ≤ k ) (sym (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )))) ( | |
1676 ZChain.order (pzc b<x) o≤-refl | |
1677 (subst₂ (λ j k → j o< k ) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc))) | |
1678 (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl))) sa<sb) | |
1679 (subst (λ k → FClosure A f k w) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc)) ) fc ) ) where | |
1680 a<b : a o< b | |
1681 a<b = supf-inject0 supf-mono sa<sb | |
1682 a<x : a o< x | |
1683 a<x = ordtrans<-≤ a<b b≤x | |
1684 ... | case1 refl = subst (λ k → w ≤ k ) (sym (sf1=spu refl)) ( zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb) | |
1685 (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc )) where | |
1686 a<x : a o< x | |
1687 a<x = supf-inject0 supf-mono sa<sb | |
1688 zc40 : ZChain.supf (pzc (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc (ob<x lim a<x )) a) w → w ≤ spu | |
1689 zc40 sa<sp fc with x<y∨y≤x (supfz a<x) x | |
1690 ... | case1 sa<x = z29 where | |
1691 z28 : odef (UnionCF A f ay supf1 b) w | |
1692 z28 = cfcs a<x o≤-refl (subst (λ k → k o< x) (sym (sf1=sf a<x)) sa<x) (subst (λ k → FClosure A f k w ) (sym (sf1=sf a<x)) fc ) | |
1693 z29 : w ≤ spu | |
1694 z29 with z28 | |
1695 ... | ⟪ aw , ch-init fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-init fc ⟫ | |
1696 ... | ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-isup u u<b z30 | |
1697 (subst (λ k → FClosure A f k w) (sf1=sf u<b) fc) ⟫ where | |
1698 z30 : supfz u<b o≤ u | |
1699 z30 = o≤-refl0 ( trans (sym (sf1=sf u<b)) su=u ) | |
1700 ... | case2 x≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where | |
1701 z27 : supf1 a ≡ supf1 b | |
1702 z27 = begin | |
1703 supf1 a ≡⟨ ( supfeq1 (o<→≤ a<x) o≤-refl ( union-max1 (subst (λ k → x o≤ k ) (sym (sf1=sf a<x)) x≤sa ) b≤x sa<sb) ) ⟩ | |
1704 supf1 x ∎ where open ≡-Reasoning | |
1705 | |
1706 --- | 1557 --- |
1707 --- the maximum chain has fix point of any ≤-monotonic function | 1558 --- the maximum chain has fix point of any ≤-monotonic function |
1708 --- | 1559 --- |
1709 | 1560 |
1710 SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x | 1561 SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x |