Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 982:6d29911a9d00
... order supf o< supf is bad?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 11 Nov 2022 19:27:15 +0900 |
parents | 6b67e43733ca |
children | 6101b9bfbe57 |
comparison
equal
deleted
inserted
replaced
981:6b67e43733ca | 982:6d29911a9d00 |
---|---|
271 supu=u : supf u ≡ u | 271 supu=u : supf u ≡ u |
272 | 272 |
273 data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) | 273 data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) |
274 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where | 274 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where |
275 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z | 275 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z |
276 ch-is-sup : (u : Ordinal) {z : Ordinal } (u≤x : supf u o≤ supf x) ( is-sup : ChainP A f mf ay supf u ) | 276 ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) |
277 ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z | 277 ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z |
278 | 278 |
279 -- | 279 -- |
280 -- f (f ( ... (sup y))) f (f ( ... (sup z1))) | 280 -- f (f ( ... (sup y))) f (f ( ... (sup z1))) |
281 -- / | / | | 281 -- / | / | |
287 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) | 287 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) |
288 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) | 288 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) |
289 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where | 289 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where |
290 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) | 290 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) |
291 ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb | 291 ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb |
292 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca | 292 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca |
293 ... | case1 eq with s≤fc (supf ub) f mf fcb | 293 ... | case1 eq with s≤fc (supf ub) f mf fcb |
294 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where | 294 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where |
295 ct00 : * a ≡ * b | 295 ct00 : * a ≡ * b |
296 ct00 = trans (cong (*) eq) eq1 | 296 ct00 = trans (cong (*) eq) eq1 |
297 ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where | 297 ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where |
298 ct01 : * a < * b | 298 ct01 : * a < * b |
299 ct01 = subst (λ k → * k < * b ) (sym eq) lt | 299 ct01 = subst (λ k → * k < * b ) (sym eq) lt |
300 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where | 300 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where |
301 ct00 : * a < * (supf ub) | 301 ct00 : * a < * (supf ub) |
302 ct00 = lt | 302 ct00 = lt |
303 ct01 : * a < * b | 303 ct01 : * a < * b |
304 ct01 with s≤fc (supf ub) f mf fcb | 304 ct01 with s≤fc (supf ub) f mf fcb |
305 ... | case1 eq = subst (λ k → * a < k ) eq ct00 | 305 ... | case1 eq = subst (λ k → * a < k ) eq ct00 |
306 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt | 306 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt |
307 ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb | 307 ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb |
308 ... | case1 eq with s≤fc (supf ua) f mf fca | 308 ... | case1 eq with s≤fc (supf ua) f mf fca |
309 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where | 309 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where |
310 ct00 : * a ≡ * b | 310 ct00 : * a ≡ * b |
311 ct00 = sym (trans (cong (*) eq) eq1 ) | 311 ct00 = sym (trans (cong (*) eq) eq1 ) |
312 ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where | 312 ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where |
313 ct01 : * b < * a | 313 ct01 : * b < * a |
314 ct01 = subst (λ k → * k < * a ) (sym eq) lt | 314 ct01 = subst (λ k → * k < * a ) (sym eq) lt |
315 ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where | 315 ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where |
316 ct00 : * b < * (supf ua) | 316 ct00 : * b < * (supf ua) |
317 ct00 = lt | 317 ct00 = lt |
318 ct01 : * b < * a | 318 ct01 : * b < * a |
319 ct01 with s≤fc (supf ua) f mf fca | 319 ct01 with s≤fc (supf ua) f mf fca |
320 ... | case1 eq = subst (λ k → * b < k ) eq ct00 | 320 ... | case1 eq = subst (λ k → * b < k ) eq ct00 |
399 chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) | 399 chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) |
400 (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b | 400 (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b |
401 → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c | 401 → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c |
402 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = | 402 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = |
403 ⟪ ua , ch-init fc ⟫ | 403 ⟪ ua , ch-init fc ⟫ |
404 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua≤x is-sup fc ⟫ = | 404 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = |
405 ⟪ uaa , ch-is-sup ua (OrdTrans ua≤x (supf-mono a≤b) ) is-sup fc ⟫ | 405 ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b) is-sup fc ⟫ |
406 | 406 |
407 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) | 407 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) |
408 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where | 408 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where |
409 field | 409 field |
410 supf : Ordinal → Ordinal | 410 supf : Ordinal → Ordinal |
433 | 433 |
434 chain∋init : odef chain y | 434 chain∋init : odef chain y |
435 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ | 435 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ |
436 f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) | 436 f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) |
437 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ | 437 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ |
438 f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫ | 438 f-next {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x is-sup (fsuc _ fc ) ⟫ |
439 initial : {z : Ordinal } → odef chain z → * y ≤ * z | 439 initial : {z : Ordinal } → odef chain z → * y ≤ * z |
440 initial {a} ⟪ aa , ua ⟫ with ua | 440 initial {a} ⟪ aa , ua ⟫ with ua |
441 ... | ch-init fc = s≤fc y f mf fc | 441 ... | ch-init fc = s≤fc y f mf fc |
442 ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where | 442 ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where |
443 zc7 : y <= supf u | 443 zc7 : y <= supf u |
444 zc7 = ChainP.fcy<sup is-sup (init ay refl) | 444 zc7 = ChainP.fcy<sup is-sup (init ay refl) |
445 f-total : IsTotalOrderSet chain | 445 f-total : IsTotalOrderSet chain |
446 f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where | 446 f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where |
447 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) | 447 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) |
615 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) | 615 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) |
616 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b | 616 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b |
617 → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b | 617 → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b |
618 is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev | 618 is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev |
619 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ | 619 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ |
620 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) | 620 ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) |
621 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ | 621 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ |
622 | 622 |
623 supf = ZChain.supf zc | 623 supf = ZChain.supf zc |
624 | 624 |
625 csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 | 625 csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 |
626 csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where | 626 csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where |
631 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) | 631 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) |
632 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) | 632 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) |
633 zc05 : odef (UnionCF A f mf ay supf b) (supf s) | 633 zc05 : odef (UnionCF A f mf ay supf b) (supf s) |
634 zc05 with zc04 | 634 zc05 with zc04 |
635 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ | 635 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ |
636 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (o<→≤ zc08) is-sup fc ⟫ where | 636 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where |
637 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s | 637 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s |
638 zc07 = fc | 638 zc07 = fc |
639 zc06 : supf u ≡ u | 639 zc06 : supf u ≡ u |
640 zc06 = ChainP.supu=u is-sup | 640 zc06 = ChainP.supu=u is-sup |
641 zc08 : supf u o< supf b | 641 zc08 : supf u o< supf b |
642 zc08 = ordtrans≤-< (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc ))) ss<sb | 642 zc08 = ordtrans≤-< (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc ))) ss<sb |
643 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where | 643 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where |
644 zc04 : odef (UnionCF A f mf ay supf b) (f x) | 644 zc04 : odef (UnionCF A f mf ay supf b) (f x) |
645 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) | 645 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) |
646 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ | 646 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ |
647 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ | 647 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫ |
648 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) | 648 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) |
649 order {b} {s} {z1} b<z ss<sb fc = zc04 where | 649 order {b} {s} {z1} b<z ss<sb fc = zc04 where |
650 zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) | 650 zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) |
651 zc00 = MinSUP.x≤sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc )) | 651 zc00 = MinSUP.x≤sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc )) |
652 -- supf (supf b) ≡ supf b | 652 -- supf (supf b) ≡ supf b |
666 HasPrev A (UnionCF A f mf ay supf x) f b ∨ IsSUP A (UnionCF A f mf ay supf b) ab → | 666 HasPrev A (UnionCF A f mf ay supf x) f b ∨ IsSUP A (UnionCF A f mf ay supf b) ab → |
667 * a < * b → odef (UnionCF A f mf ay supf x) b | 667 * a < * b → odef (UnionCF A f mf ay supf x) b |
668 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P | 668 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P |
669 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b | 669 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b |
670 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup | 670 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup |
671 = ⟪ ab , ch-is-sup b (ZChain.supf-mono zc (o<→≤ b<x)) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where | 671 = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where |
672 b<A : b o< & A | 672 b<A : b o< & A |
673 b<A = z09 ab | 673 b<A = z09 ab |
674 b<x : b o< x | 674 b<x : b o< x |
675 b<x = ZChain.supf-inject zc sb<sx | 675 b<x = ZChain.supf-inject zc sb<sx |
676 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b | 676 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b |
692 * a < * b → odef (UnionCF A f mf ay supf x) b | 692 * a < * b → odef (UnionCF A f mf ay supf x) b |
693 is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P | 693 is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P |
694 is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b | 694 is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b |
695 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay ) | 695 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay ) |
696 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ | 696 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ |
697 ... | case2 y<b = ⟪ ab , ch-is-sup b (ZChain.supf-mono zc (o<→≤ b<x)) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where | 697 ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where |
698 m09 : b o< & A | 698 m09 : b o< & A |
699 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) | 699 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) |
700 b<x : b o< x | 700 b<x : b o< x |
701 b<x = ZChain.supf-inject zc sb<sx | 701 b<x = ZChain.supf-inject zc sb<sx |
702 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b | 702 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b |
1049 s1u=x = trans ? eq | 1049 s1u=x = trans ? eq |
1050 zc13 : osuc px o< osuc u1 | 1050 zc13 : osuc px o< osuc u1 |
1051 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) | 1051 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) |
1052 x≤sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) | 1052 x≤sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) |
1053 x≤sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? | 1053 x≤sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? |
1054 x≤sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? )) | 1054 x≤sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? )) |
1055 ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where | 1055 ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where |
1056 zc14 : u ≡ osuc px | 1056 zc14 : u ≡ osuc px |
1057 zc14 = begin | 1057 zc14 = begin |
1058 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ | 1058 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ |
1059 supf0 u ≡⟨ ? ⟩ | 1059 supf0 u ≡⟨ ? ⟩ |
1173 b o< x → (ab : odef A b) → | 1173 b o< x → (ab : odef A b) → |
1174 HasPrev A (UnionCF A f mf ay supf x) f b → | 1174 HasPrev A (UnionCF A f mf ay supf x) f b → |
1175 * a < * b → odef (UnionCF A f mf ay supf x) b | 1175 * a < * b → odef (UnionCF A f mf ay supf x) b |
1176 is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev | 1176 is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev |
1177 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ | 1177 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ |
1178 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ? -- ⟪ ab , | 1178 ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab , |
1179 -- subst (λ k → UChain A f mf ay supf x k ) | 1179 -- subst (λ k → UChain A f mf ay supf x k ) |
1180 -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ | 1180 -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ |
1181 | 1181 |
1182 zc70 : HasPrev A pchain f x → ¬ xSUP pchain f x | 1182 zc70 : HasPrev A pchain f x → ¬ xSUP pchain f x |
1183 zc70 pr xsup = ? | 1183 zc70 pr xsup = ? |
1184 | 1184 |
1185 no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) supf0 x ) → ZChain A f mf ay x | 1185 no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) supf0 x ) → ZChain A f mf ay x |
1189 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z | 1189 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z |
1190 pchain0=1 : pchain ≡ pchain1 | 1190 pchain0=1 : pchain ≡ pchain1 |
1191 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where | 1191 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where |
1192 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z | 1192 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z |
1193 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ | 1193 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ |
1194 zc10 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc12 fc where | 1194 zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where |
1195 zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z | 1195 zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z |
1196 zc12 (fsuc x fc) with zc12 fc | 1196 zc12 (fsuc x fc) with zc12 fc |
1197 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ | 1197 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ |
1198 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ | 1198 ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ |
1199 zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫ | 1199 zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫ |
1200 zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z | 1200 zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z |
1201 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ | 1201 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ |
1202 zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where | 1202 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where |
1203 zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z | 1203 zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z |
1204 zc13 (fsuc x fc) with zc13 fc | 1204 zc13 (fsuc x fc) with zc13 fc |
1205 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ | 1205 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ |
1206 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ | 1206 ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ |
1207 zc13 (init asu su=z ) with trio< u x | 1207 zc13 (init asu su=z ) with trio< u x |
1208 ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫ | 1208 ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫ |
1209 ... | tri≈ ¬a b ¬c = ? | 1209 ... | tri≈ ¬a b ¬c = ? |
1210 ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u≤x c ) | 1210 ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c ) |
1211 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) | 1211 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) |
1212 sup {z} z≤x with trio< z x | 1212 sup {z} z≤x with trio< z x |
1213 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} ) | 1213 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} ) |
1214 ... | tri≈ ¬a b ¬c = {!!} | 1214 ... | tri≈ ¬a b ¬c = {!!} |
1215 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) | 1215 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) |
1394 smc<<d = sc<<d asc spd | 1394 smc<<d = sc<<d asc spd |
1395 | 1395 |
1396 sz<<c : {z : Ordinal } → z o< & A → supf z <= mc | 1396 sz<<c : {z : Ordinal } → z o< & A → supf z <= mc |
1397 sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) | 1397 sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) |
1398 | 1398 |
1399 z511 : {u y mc : Ordinal} (u<x : u o< mc ) (is-sup1 : ChainP A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) u) | |
1400 (fc : FClosure A (cf nmx) (ZChain.supf zc u) y) (x=fy : mc ≡ cf nmx y) → | |
1401 ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) | |
1402 z511 {u} {y} {mc} u<x is-sup fc x=fy with osuc-≡< (ZChain.supf-mono zc (o<→≤ u<x)) | |
1403 ... | case2 lt = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) ? lt (fsuc _ ( fsuc _ fc ))) | |
1404 ... | case1 eq = ? | |
1405 -- u ≡ supf u ≡ supf mc ≡ supf (cf nmx y) | |
1406 -- supf u << cf nmx (cf nmx ( ... (supf u )) <= spuf mc ≡ u | |
1407 -- y ≡ supf u | |
1408 -- y ≡ cf nmx (supf u) | |
1409 -- y ≡ cf nmx (cf nmx (supf u)) | |
1410 | |
1399 sc=c : supf mc ≡ mc | 1411 sc=c : supf mc ≡ mc |
1400 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where | 1412 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where |
1401 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc | 1413 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc |
1402 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where | 1414 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where |
1403 z30 : * mc < * (cf nmx mc) | 1415 z30 : * mc < * (cf nmx mc) |
1404 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) | 1416 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) |
1405 z31 : ( * (cf nmx mc) ≡ * mc ) ∨ ( * (cf nmx mc) < * mc ) | 1417 z31 : ( * (cf nmx mc) ≡ * mc ) ∨ ( * (cf nmx mc) < * mc ) |
1406 z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k → odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) | 1418 z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k → odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) |
1407 ⟪ proj2 (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc)) ⟫ )) | 1419 ⟪ proj2 (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc)) ⟫ )) |
1408 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u≤x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where | 1420 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where |
1409 z30 : * mc < * (cf nmx mc) | 1421 z30 : * mc < * (cf nmx mc) |
1410 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) | 1422 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) |
1411 z31 : ( supf mc ≡ mc ) ∨ ( * (supf mc) < * mc ) | 1423 z31 : ( supf mc ≡ mc ) ∨ ( * (supf mc) < * mc ) |
1412 z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) | 1424 z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) |
1413 z32 : * (supf mc) < * (cf nmx (cf nmx y)) | 1425 z32 : * (supf mc) < * (cf nmx (cf nmx y)) |
1414 z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 ) | 1426 z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 ) |
1415 z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) | 1427 z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) |
1416 z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A ? (fsuc _ ( fsuc _ fc ))) | 1428 z48 = z511 u<x is-sup1 fc x=fy |
1417 is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) | 1429 is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) |
1418 is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) } | 1430 is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) } |
1419 | 1431 |
1420 | 1432 |
1421 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d | 1433 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d |
1424 z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) | 1436 z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) |
1425 z32 : ( cf nmx (cf nmx y) ≡ supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) ) | 1437 z32 : ( cf nmx (cf nmx y) ≡ supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) ) |
1426 z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc)) | 1438 z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc)) |
1427 z31 : ( * (cf nmx d) ≡ * d ) ∨ ( * (cf nmx d) < * d ) | 1439 z31 : ( * (cf nmx d) ≡ * d ) ∨ ( * (cf nmx d) < * d ) |
1428 z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) | 1440 z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) |
1429 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u≤x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where | 1441 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where |
1430 z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) | 1442 z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) |
1431 z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p | 1443 z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p |
1432 z48 : supf mc << d | 1444 z48 : supf mc << d |
1433 z48 = sc<<d {mc} asc spd | 1445 z48 = sc<<d {mc} asc spd |
1434 z53 : supf u o≤ supf (& A) | 1446 z53 : supf u o≤ supf (& A) |
1435 z53 = OrdTrans u≤x ? | 1447 z53 = ZChain.supf-mono zc (o<→≤ (z09 (subst (λ k → odef A k) (ChainP.supu=u is-sup1) (ZChain.asupf zc) ))) -- OrdTrans u<x ? |
1436 z52 : ( u ≡ mc ) ∨ ( u << mc ) | 1448 z52 : ( u ≡ mc ) ∨ ( u << mc ) |
1437 z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) | 1449 z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) |
1438 , ch-is-sup u ? is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ | 1450 , ch-is-sup u (z09 (subst (λ k → odef A k) (ChainP.supu=u is-sup1) (ZChain.asupf zc) )) |
1451 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ | |
1439 z51 : supf u o≤ supf mc | 1452 z51 : supf u o≤ supf mc |
1440 z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where | 1453 z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where |
1441 z56 : u ≡ mc → supf u ≡ supf mc | 1454 z56 : u ≡ mc → supf u ≡ supf mc |
1442 z56 eq = cong supf eq | 1455 z56 eq = cong supf eq |
1443 z57 : u << mc → supf u o≤ supf mc | 1456 z57 : u << mc → supf u o≤ supf mc |
1445 z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d | 1458 z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d |
1446 z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c) lt | 1459 z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c) lt |
1447 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) | 1460 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) |
1448 z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc )) | 1461 z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc )) |
1449 z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) ) | 1462 z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) ) |
1450 z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A ? (fsuc _ ( fsuc _ fc )) | 1463 z50 = ≤to<= ( z511 u<x is-sup1 fc x=fy ) |
1451 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) | 1464 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) |
1452 → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1 | 1465 → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1 |
1453 → * (cf nmx (cf nmx y)) < * d1 | 1466 → * (cf nmx (cf nmx y)) < * d1 |
1454 z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq)) smc<d | 1467 z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq)) smc<d |
1455 z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d | 1468 z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d |
1472 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → | 1485 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → |
1473 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) | 1486 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) |
1474 z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where | 1487 z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where |
1475 z32 : ( a ≡ supf mc ) ∨ ( * a < * (supf mc) ) | 1488 z32 : ( a ≡ supf mc ) ∨ ( * a < * (supf mc) ) |
1476 z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc | 1489 z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc |
1477 z22 {a} ⟪ aa , ch-is-sup u u≤x is-sup1 fc ⟫ = tri u (supf mc) | 1490 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc) |
1478 z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where | 1491 z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where |
1479 z53 : supf u o< supf (& A) | |
1480 z53 = ordtrans<-≤ u≤x ? | |
1481 z52 : ( u ≡ mc ) ∨ ( u << mc ) | 1492 z52 : ( u ≡ mc ) ∨ ( u << mc ) |
1482 z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) | 1493 z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) |
1483 , ch-is-sup u ? is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ | 1494 , ch-is-sup u (z09 (subst (λ k → odef A k) (ChainP.supu=u is-sup1) (ZChain.asupf zc) )) |
1495 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ | |
1484 z56 : u ≡ mc → supf u ≡ supf mc | 1496 z56 : u ≡ mc → supf u ≡ supf mc |
1485 z56 eq = cong supf eq | 1497 z56 eq = cong supf eq |
1486 z57 : u << mc → supf u o≤ supf mc | 1498 z57 : u << mc → supf u o≤ supf mc |
1487 z57 lt = ZChain.supf-<= zc (case2 z58) where | 1499 z57 lt = ZChain.supf-<= zc (case2 z58) where |
1488 z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d | 1500 z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d |
1492 z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d ) | 1504 z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d ) |
1493 z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A | 1505 z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A |
1494 (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1)) u<smc) fc ) smc<<d ) | 1506 (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1)) u<smc) fc ) smc<<d ) |
1495 z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d ) | 1507 z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d ) |
1496 z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) ) | 1508 z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) ) |
1497 -- u≤x : ZChain.supf zc u o< ZChain.supf zc d | 1509 -- u<x : ZChain.supf zc u o< ZChain.supf zc d |
1498 -- supf u o< supf c → order | 1510 -- supf u o< supf c → order |
1499 | 1511 |
1500 sd=d : supf d ≡ d | 1512 sd=d : supf d ≡ d |
1501 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ | 1513 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ |
1502 | 1514 |