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

comparison src/zorn.agda @ 1058:12ce8d0224d2

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 Sat, 10 Dec 2022 09:56:32 +0900
parents cd3237120dec
children bd2a258f309c
comparison
equal deleted inserted replaced
1057:cd3237120dec 1058:12ce8d0224d2
339 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 339 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
340 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z 340 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
341 341
342 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) 342 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
343 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z 343 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
344 → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b 344 → IsSUP A (UnionCF A f ay supf b) b → supf b ≡ b
345 345
346 chain : HOD 346 chain : HOD
347 chain = UnionCF A f ay supf z 347 chain = UnionCF A f ay supf z
348 chain⊆A : chain ⊆' A 348 chain⊆A : chain ⊆' A
349 chain⊆A = λ lt → proj1 lt 349 chain⊆A = λ lt → proj1 lt
350 350
351 chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y 351 chain∋init : {x : Ordinal } → odef (UnionCF A f ay supf x) y
352 chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl) ⟫ 352 chain∋init {x} = ⟪ ay , ch-init (init ay refl) ⟫
353 353
354 mf : ≤-monotonic-f A f 354 mf : ≤-monotonic-f A f
355 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where 355 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
356 mf00 : * x < * (f x) 356 mf00 : * x < * (f x)
357 mf00 = proj1 ( mf< x ax ) 357 mf00 = proj1 ( mf< x ax )
428 ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) 428 ft00 : Tri ( a < b) ( a ≡ b) ( b < a )
429 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) 429 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
430 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = 430 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
431 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb ) 431 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb )
432 432
433 IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
434 → ({y : Ordinal} → odef (UnionCF A f ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
435 → ( {a : Ordinal } → odef A a → a << f a )
436 → ¬ ( HasPrev A (UnionCF A f ay supf x) f sp )
437 IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<<-irr fsp≤sp sp<fsp ) where
438 sp<fsp : sp << f sp
439 sp<fsp = <-mono-f asp
440 pr = HasPrev.y hp
441 im00 : f (f pr) ≤ sp
442 im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
443 fsp≤sp : f sp ≤ sp
444 fsp≤sp = subst (λ k → f k ≤ sp ) (sym (HasPrev.x=fy hp)) im00
445
446 supf-¬hp : {x : Ordinal } → x o≤ z
447 → ( {a : Ordinal } → odef A a → a << f a )
448 → ¬ ( HasPrev A (UnionCF A f ay supf x) f (supf x) )
449 supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw →
450 (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
451
452 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b 433 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b
453 supf-idem {b} b≤z sfb≤x = z52 where 434 supf-idem {b} b≤z sfb≤x = z52 where
454 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) 435 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
455 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc 436 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
456 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 437 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
457 u<b : u o< b 438 u<b : u o< b
458 u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) 439 u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
459 z52 : supf (supf b) ≡ supf b 440 z52 : supf (supf b) ≡ supf b
460 z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 441 z52 = sup=u asupf sfb≤x record { ax = asupf ; x≤sup = z54 }
461 442
462 x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x 443 x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x
463 x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x 444 x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
464 ... | case2 le = le 445 ... | case2 le = le
465 ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where 446 ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where
467 z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where 448 z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where
468 z47 : supf (supf x) ≡ supf x 449 z47 : supf (supf x) ≡ supf x
469 z47 = supf-idem x≤z sx≤z 450 z47 = supf-idem x≤z sx≤z
470 z45 : f (supf x) ≤ supf x 451 z45 : f (supf x) ≤ supf x
471 z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 452 z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
453
454 sup=u0 : {b : Ordinal} → (ab : odef A b) → b o≤ z
455 → IsSUP A (UnionCF A f ay supf b) b → supf b ≡ b
456 sup=u0 {b} ab b≤z is-sup with trio< (supf b) b
457 ... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where
458 z47 : b o≤ supf b
459 z47 = x≤supfx b≤z ?
460 ... | tri≈ ¬a b ¬c = b
461 ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) where
462 z48 : supf b o≤ b
463 z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux )
472 464
473 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b 465 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
474 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) 466 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl)
475 ... | case2 lt = lt 467 ... | case2 lt = lt
476 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) 468 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
706 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 698 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
707 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) 699 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
708 ... | case2 sb<sx = m10 where 700 ... | case2 sb<sx = m10 where
709 b<A : b o< & A 701 b<A : b o< & A
710 b<A = z09 ab 702 b<A = z09 ab
711 m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
712 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
713 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } )
714 m05 : ZChain.supf zc b ≡ b 703 m05 : ZChain.supf zc b ≡ b
715 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ 704 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz }
716 m10 : odef (UnionCF A f ay supf x) b 705 m10 : odef (UnionCF A f ay supf x) b
717 m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) 706 m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
718 ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where 707 ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
719 m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x ) 708 m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
720 m17 = ZChain.minsup zc x≤A 709 m17 = ZChain.minsup zc x≤A
726 m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where 715 m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
727 m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b 716 m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
728 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 717 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
729 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) 718 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } )
730 m05 : ZChain.supf zc b ≡ b 719 m05 : ZChain.supf zc b ≡ b
731 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ 720 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz }
732 m14 : ZChain.supf zc b o< x 721 m14 : ZChain.supf zc b o< x
733 m14 = subst (λ k → k o< x ) (sym m05) b<x 722 m14 = subst (λ k → k o< x ) (sym m05) b<x
734 m13 : odef (UnionCF A f ay supf x) z 723 m13 : odef (UnionCF A f ay supf x) z
735 m13 = ZChain.cfcs zc b<x x≤A m14 fc 724 m13 = ZChain.cfcs zc b<x x≤A m14 fc
736 725
739 b o< x → (ab : odef A b) → 728 b o< x → (ab : odef A b) →
740 HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) b → 729 HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) b →
741 * a < * b → odef (UnionCF A f ay supf x) b 730 * a < * b → odef (UnionCF A f ay supf x) b
742 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P 731 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
743 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 732 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
744 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc (ordtrans b<x x≤A) ) 733 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc )
745 ... | 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 )) ⟫ 734 ... | 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 )) ⟫
746 ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) 735 ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
747 ... | case2 sb<sx = m10 where 736 ... | case2 sb<sx = m10 where
748 m09 : b o< & A 737 m09 : b o< & A
749 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) 738 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
750 m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
751 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
752 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp)
753 ; x=fy = HasPrev.x=fy nhp } )
754 m05 : ZChain.supf zc b ≡ b 739 m05 : ZChain.supf zc b ≡ b
755 m05 = ZChain.sup=u zc ab (o<→≤ m09) ⟪ record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫ -- ZChain on x 740 m05 = ZChain.sup=u zc ab (o<→≤ m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt }
756 m10 : odef (UnionCF A f ay supf x) b 741 m10 : odef (UnionCF A f ay supf x) b
757 m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) 742 m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
758 ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where 743 ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
759 m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x ) 744 m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
760 m17 = ZChain.minsup zc x≤A 745 m17 = ZChain.minsup zc x≤A
762 m18 = ZChain.supf-is-minsup zc x≤A 747 m18 = ZChain.supf-is-minsup zc x≤A
763 m10 : f (supf b) ≡ supf b 748 m10 : f (supf b) ≡ supf b
764 m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where 749 m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
765 m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x) 750 m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
766 m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where 751 m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
767 m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b 752 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz }
768 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
769 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } )
770 m05 : ZChain.supf zc b ≡ b
771 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫
772 m14 : ZChain.supf zc b o< x 753 m14 : ZChain.supf zc b o< x
773 m14 = subst (λ k → k o< x ) (sym m05) b<x 754 m14 = subst (λ k → k o< x ) (sym m05) b<x
774 m13 : odef (UnionCF A f ay supf x) z 755 m13 : odef (UnionCF A f ay supf x) z
775 m13 = ZChain.cfcs zc b<x x≤A m14 fc 756 m13 = ZChain.cfcs zc b<x x≤A m14 fc
776 757
1135 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where 1116 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where
1136 u≤px : u o≤ px 1117 u≤px : u o≤ px
1137 u≤px = ordtrans u<x z≤px 1118 u≤px = ordtrans u<x z≤px
1138 1119
1139 sup=u : {b : Ordinal} (ab : odef A b) → 1120 sup=u : {b : Ordinal} (ab : odef A b) →
1140 b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b 1121 b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b → supf1 b ≡ b
1141 sup=u {b} ab b≤x is-sup with trio< b px 1122 sup=u {b} ab b≤x is-sup with trio< b px
1142 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ zc40 , ZChain.IsMinSUP→NotHasPrev zc ab zc42 (λ ax → proj1 (mf< _ ax)) ⟫ where 1123 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) zc40 where
1143 zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b 1124 zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
1144 zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-init fc ⟫ 1125 zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup is-sup ⟪ ua , ch-init fc ⟫
1145 zc42 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , 1126 zc42 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = IsSUP.x≤sup is-sup ⟪ ua ,
1146 ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44) ⟫ where 1127 ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44) ⟫ where
1147 zc44 : u o≤ px 1128 zc44 : u o≤ px
1148 zc44 = ordtrans u<x (o<→≤ a) 1129 zc44 = ordtrans u<x (o<→≤ a)
1149 zc40 : IsSUP A (UnionCF A f ay supf0 b) b 1130 zc40 : IsSUP A (UnionCF A f ay supf0 b) b
1150 zc40 = record { ax = ab ; x≤sup = zc42 } 1131 zc40 = record { ax = ab ; x≤sup = zc42 }
1151 ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px) ⟪ record { ax = ab ; x≤sup = zc42 } , 1132 ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px) record { ax = ab ; x≤sup = zc42 } where
1152 ZChain.IsMinSUP→NotHasPrev zc ab zc42 (λ ax → proj1 (mf< _ ax)) ⟫ where
1153 zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b 1133 zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
1154 zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-init fc ⟫ 1134 zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup is-sup ⟪ ua , ch-init fc ⟫
1155 zc42 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , 1135 zc42 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = IsSUP.x≤sup is-sup ⟪ ua ,
1156 ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44) ⟫ where 1136 ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44) ⟫ where
1157 zc44 : u o≤ px 1137 zc44 : u o≤ px
1158 zc44 = o<→≤ ( subst (λ k → u o< k ) b=px u<x ) 1138 zc44 = o<→≤ ( subst (λ k → u o< k ) b=px u<x )
1159 ... | tri> ¬a ¬b px<b = trans zc36 x=b where 1139 ... | tri> ¬a ¬b px<b = trans zc36 x=b where
1160 x=b : x ≡ b 1140 x=b : x ≡ b
1162 ... | case1 eq = sym (eq) 1142 ... | case1 eq = sym (eq)
1163 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 1143 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
1164 zc31 : sp1 o≤ b 1144 zc31 : sp1 o≤ b
1165 zc31 = MinSUP.minsup sup1 ab zc32 where 1145 zc31 = MinSUP.minsup sup1 ab zc32 where
1166 zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) 1146 zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
1167 zc32 {w} (case1 ⟪ ua , ch-init fc ⟫ ) = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-init fc ⟫ 1147 zc32 {w} (case1 ⟪ ua , ch-init fc ⟫ ) = IsSUP.x≤sup is-sup ⟪ ua , ch-init fc ⟫
1168 zc32 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫ ) = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-is-sup u z01 z02 z03 ⟫ where 1148 zc32 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫ ) = IsSUP.x≤sup is-sup ⟪ ua , ch-is-sup u z01 z02 z03 ⟫ where
1169 z01 : u o< b 1149 z01 : u o< b
1170 z01 = ordtrans u<x (subst (λ k → px o< k ) x=b px<x ) 1150 z01 = ordtrans u<x (subst (λ k → px o< k ) x=b px<x )
1171 z02 : supf1 u ≡ u 1151 z02 : supf1 u ≡ u
1172 z02 = trans (sf1=sf0 (o<→≤ u<x)) su=u 1152 z02 = trans (sf1=sf0 (o<→≤ u<x)) su=u
1173 z03 : FClosure A f (supf1 u) w 1153 z03 : FClosure A f (supf1 u) w
1174 z03 = fcpu fc (o<→≤ u<x) 1154 z03 = fcpu fc (o<→≤ u<x)
1175 zc32 {w} (case2 fc) = IsSUP.x≤sup (proj1 is-sup) ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where 1155 zc32 {w} (case2 fc) = IsSUP.x≤sup is-sup ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where
1176 su=u : supf1 (supf0 px) ≡ supf0 px 1156 su=u : supf1 (supf0 px) ≡ supf0 px
1177 su=u = trans (sf1=sf0 (zc-b<x _ (proj2 fc))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (proj2 fc)) ) 1157 su=u = trans (sf1=sf0 (zc-b<x _ (proj2 fc))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (proj2 fc)) )
1178 fc1 : FClosure A f (supf1 (supf0 px)) w 1158 fc1 : FClosure A f (supf1 (supf0 px)) w
1179 fc1 = subst (λ k → FClosure A f k w ) (sym su=u) (proj1 fc) 1159 fc1 = subst (λ k → FClosure A f k w ) (sym su=u) (proj1 fc)
1180 sa<x : supf0 px o< b 1160 sa<x : supf0 px o< b
1303 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) 1283 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa)
1304 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1 1284 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1
1305 1285
1306 ... | no lim with trio< x o∅ 1286 ... | no lim with trio< x o∅
1307 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 1287 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
1308 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ? 1288 ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; sup=u = ? ; asupf = MinSUP.as (ysup f mf ay)
1309 ; supfmax = ? ; is-minsup = ? ; cfcs = ? } 1289 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
1290 ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where
1291 mf : ≤-monotonic-f A f
1292 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
1293 mf00 : * x < * (f x)
1294 mf00 = proj1 ( mf< x ax )
1310 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ? 1295 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
1311 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where 1296 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where
1312 1297
1313 -- mf : ≤-monotonic-f A f 1298 -- mf : ≤-monotonic-f A f
1314 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust 1299 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust
1469 fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc 1454 fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
1470 zcm : odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim m<x))) (osuc (omax a sa))) w 1455 zcm : odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim m<x))) (osuc (omax a sa))) w
1471 zcm = ZChain.cfcs (pzc (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm 1456 zcm = ZChain.cfcs (pzc (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
1472 zc40 : odef (UnionCF A f ay supf1 b) w 1457 zc40 : odef (UnionCF A f ay supf1 b) w
1473 zc40 with ZChain.cfcs (pzc (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm 1458 zc40 with ZChain.cfcs (pzc (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
1474 ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ 1459 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
1460 ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ? ⟫
1475 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) 1461 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
1476 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) 1462 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
1477 cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where 1463 cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
1478 supfb = ZChain.supf (pzc (ob<x lim b<x)) 1464 supfb = ZChain.supf (pzc (ob<x lim b<x))
1479 sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a 1465 sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a
1483 -- supfb a o< b assures it is in Union b 1469 -- supfb a o< b assures it is in Union b
1484 zcb : odef (UnionCF A f ay supfb b) w 1470 zcb : odef (UnionCF A f ay supfb b) w
1485 zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb 1471 zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
1486 zc40 : odef (UnionCF A f ay supf1 b) w 1472 zc40 : odef (UnionCF A f ay supf1 b) w
1487 zc40 with zcb 1473 zc40 with zcb
1488 ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ 1474 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
1475 ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ? ⟫
1489 1476
1490 sup=u : {b : Ordinal} (ab : odef A b) → 1477 sup=u : {b : Ordinal} (ab : odef A b) →
1491 b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b 1478 b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b → supf1 b ≡ b
1492 sup=u {b} ab b≤x is-sup with osuc-≡< b≤x 1479 sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
1493 ... | case1 b=x = ? where 1480 ... | case1 b=x = ? where
1494 zc31 : spu o≤ b 1481 zc31 : spu o≤ b
1495 zc31 = MinSUP.minsup usup ab zc32 where 1482 zc31 = MinSUP.minsup usup ab zc32 where
1496 zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b) 1483 zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b)
1525 z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl ) 1512 z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
1526 z22 : sp o< & A 1513 z22 : sp o< & A
1527 z22 = z09 asp 1514 z22 = z09 asp
1528 z12 : odef chain sp 1515 z12 : odef chain sp
1529 z12 with o≡? (& s) sp 1516 z12 with o≡? (& s) sp
1530 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ? ) 1517 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
1531 ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ? ) (z09 asp) asp (case2 z19 ) z13 where 1518 ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
1532 z13 : * (& s) < * sp 1519 z13 : * (& s) < * sp
1533 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ? ) 1520 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
1534 ... | case1 eq = ⊥-elim ( ne eq ) 1521 ... | case1 eq = ⊥-elim ( ne eq )
1535 ... | case2 lt = lt 1522 ... | case2 lt = lt
1536 z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp 1523 z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp
1537 z19 = record { ax = ? ; x≤sup = z20 } where 1524 z19 = record { ax = ? ; x≤sup = z20 } where
1538 z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) 1525 z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)