Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1029:07ffcf16a3d4
ChainP removal
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 28 Nov 2022 07:13:19 +0900 |
| parents | d1eecfc6cdfa |
| children | 40532b0ed230 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 144 insertions(+), 400 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Nov 27 20:19:18 2022 +0900 +++ b/src/zorn.agda Mon Nov 28 07:13:19 2022 +0900 @@ -265,23 +265,6 @@ x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive -- --- sup and its fclosure is in a chain HOD --- chain HOD is sorted by sup as Ordinal and <-ordered --- whole chain is a union of separated Chain --- minimum index is sup of y not ϕ --- - -record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where - field - fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) - order : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) - supu=u : supf u ≡ u - -data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) - (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where - ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z - ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) - ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z -- -- f (f ( ... (supf y))) f (f ( ... (supf z1))) @@ -301,91 +284,34 @@ fc00 : * b ≤ * (f b) fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa )) --- --- data UChain is total - -chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) - {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 ) -chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where - 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) - ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca - ... | case1 eq with s≤fc (supf ub) f mf fcb - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * a ≡ * b - ct00 = trans (cong (*) eq) eq1 - ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where - ct01 : * a < * b - ct01 = subst (λ k → * k < * b ) (sym eq) lt - 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 - ct00 : * a < * (supf ub) - ct00 = lt - ct01 : * a < * b - ct01 with s≤fc (supf ub) f mf fcb - ... | case1 eq = subst (λ k → * a < k ) eq ct00 - ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt - ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb - ... | case1 eq with s≤fc (supf ua) f mf fca - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where +fc-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) (supf : Ordinal → Ordinal ) + (order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y) + {s s1 a b : Ordinal } ( fa : FClosure A f (supf s) a )( fb : FClosure A f (supf s1) b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) +fc-total A f mf supf order {xa} {xb} {a} {b} ca cb with trio< xa xb +... | tri< a₁ ¬b ¬c with order a₁ ? +... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b - ct00 = sym (trans (cong (*) eq) eq1 ) - ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where - ct01 : * b < * a - ct01 = subst (λ k → * k < * a ) (sym eq) lt - 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 - ct00 : * b < * (supf ua) - ct00 = lt - ct01 : * b < * a - ct01 with s≤fc (supf ua) f mf fca - ... | case1 eq = subst (λ k → * b < k ) eq ct00 - ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub - ... | tri< a₁ ¬b ¬c with ChainP.order supb (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁) fca - ... | case1 eq with s≤fc (supf ub) f mf fcb - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * a ≡ * b - ct00 = trans (cong (*) eq) eq1 - ... | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where + ct00 = ? -- trans (cong (*) eq) eq1 +... | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where ct02 : * a < * b - ct02 = subst (λ k → * k < * b ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where - ct03 : * a < * (supf ub) - ct03 = lt - ct02 : * a < * b - ct02 with s≤fc (supf ub) f mf fcb - ... | case1 eq = subst (λ k → * a < k ) eq ct03 - ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri≈ ¬a eq ¬c - = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb ) - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb - ... | case1 eq with s≤fc (supf ua) f mf fca - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * a ≡ * b - ct00 = sym (trans (cong (*) eq) eq1) - ... | case2 lt = tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02 where - ct02 : * b < * a - ct02 = subst (λ k → * k < * a ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04 where - ct05 : * b < * (supf ua) - ct05 = lt - ct04 : * b < * a - ct04 with s≤fc (supf ua) f mf fca - ... | case1 eq = subst (λ k → * b < k ) eq ct05 - ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt + ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt +fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri< a₁ ¬b ¬c = ? + ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) -- Union of supf z which o< x -- -UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) - ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD -UnionCF A f mf ay supf x - = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } +-- UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) +-- ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD +-- UnionCF A f supf x +-- = record { od = record { def = λ z → odef A z ∧ UChain A f supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } -UnionCF' : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) - ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD -UnionCF' A f mf ay supf x +-- order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y +-- +UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD +UnionCF A f supf x = record { od = record { def = λ z → odef A z ∧ ( { s : Ordinal} → s o< x → FClosure A f (supf s) z ) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } @@ -412,12 +338,12 @@ M→S : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} {y : Ordinal} {ay : odef A y} { x : Ordinal } → (supf : Ordinal → Ordinal ) - → MinSUP A (UnionCF A f mf ay supf x) - → SUP A (UnionCF A f mf ay supf x) + → MinSUP A (UnionCF A f supf x) + → SUP A (UnionCF A f supf x) M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms) ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm ms) ; x≤sup = ms00 } where msup = MinSUP.sup ms - ms00 : {z : HOD} → UnionCF A f mf ay supf x ∋ z → (z ≡ * msup) ∨ (z < * msup) + ms00 : {z : HOD} → UnionCF A f supf x ∋ z → (z ≡ * msup) ∨ (z < * msup) ms00 {z} uz with MinSUP.x≤sup ms uz ... | case1 eq = case1 (subst (λ k → k ≡ _) *iso ( cong (*) eq)) ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso refl lt ) @@ -425,11 +351,8 @@ chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b - → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c -chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = - ⟪ ua , ch-init fc ⟫ -chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = - ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b) is-sup fc ⟫ + → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c +chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ⟫ = ? record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where @@ -437,44 +360,39 @@ supf : Ordinal → Ordinal sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z - → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b + → IsSUP A (UnionCF A f supf b) ab ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b cfcs : (mf< : <-monotonic-f A f) - {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w + {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f supf b) w order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z - minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) + minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f supf x) supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) chain : HOD - chain = UnionCF A f mf ay supf z + chain = UnionCF A f supf z chain⊆A : chain ⊆' A chain⊆A = λ lt → proj1 lt - sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) + sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f supf x) sup {x} x≤z = M→S supf (minsup x≤z) s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z) s=ms {x} x≤z = &iso chain∋init : odef chain y - chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ - f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) - f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ - 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 ) ⟫ + chain∋init = ⟪ ay , ? ⟫ + f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a) + f-next {a} ⟪ aa , ch-is-sup ⟫ = ? initial : {z : Ordinal } → odef chain z → * y ≤ * z - initial {a} ⟪ aa , ua ⟫ with ua - ... | ch-init fc = s≤fc y f mf fc - ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where - zc7 : y <= supf u - zc7 = ChainP.fcy<sup is-sup (init ay refl) + initial {a} ⟪ aa , ua ⟫ = ? f-total : IsTotalOrderSet chain f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf ay supf ( (proj2 ca)) ( (proj2 cb)) + uz01 = ? -- chain-total A f supf ( (proj2 ca)) ( (proj2 cb)) supf-inject : {x y : Ordinal } → supf x o< supf y → x o< y supf-inject {x} {y} sx<sy with trio< x y @@ -488,21 +406,20 @@ supf<A = z09 asupf csupf : (mf< : <-monotonic-f A f) {b : Ordinal } - → supf b o< supf z → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain + → supf b o< supf z → supf b o< z → odef (UnionCF A f supf z) (supf b) -- supf z is not an element of this chain csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl) fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf - fcy<sup {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) - , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ + fcy<sup {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ? ⟫ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) -- ordering is not proved here but in ZChain1 IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp - → ({y : Ordinal} → odef (UnionCF A f mf ay supf x) y → (y ≡ sp ) ∨ (y << sp )) + → ({y : Ordinal} → odef (UnionCF A f supf x) y → (y ≡ sp ) ∨ (y << sp )) → ( {a : Ordinal } → odef A a → a << f a ) - → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f sp ) + → ¬ ( HasPrev A (UnionCF A f supf x) f sp ) IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr ( <=to≤ fsp≤sp) sp<fsp ) where sp<fsp : sp << f sp sp<fsp = <-mono-f asp @@ -514,32 +431,29 @@ supf-¬hp : {x : Ordinal } → x o≤ z → ( {a : Ordinal } → odef A a → a << f a ) - → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f (supf x) ) + → ¬ ( HasPrev A (UnionCF A f supf x) f (supf x) ) supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → (subst (λ k → w <= k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b supf-idem mf< {b} b≤z sfb≤x = z52 where - z54 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) - z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc - z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) - (sym (supf-is-minsup b≤z)) - (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z (subst (λ k → k o< b) (sym (ChainP.supu=u is-sup)) u<b) fc )) where - u<b : u o< b - u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x ) + z54 : {w : Ordinal} → odef (UnionCF A f supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) + z54 {w} ⟪ aw , fc ⟫ = order ? ? where + u<b : supf b o< b + u<b = ? z52 : supf (supf b) ≡ supf b z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ - -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f mf ay supf (supf b) + -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b) -- the condition of cfcs is satisfied, this is obvious record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc field - is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z → (ab : odef A b) - → HasPrev A (UnionCF A f mf ay supf z) f b ∨ IsSUP A (UnionCF A f mf ay supf b) ab - → * a < * b → odef ((UnionCF A f mf ay supf z)) b + is-max : {a b : Ordinal } → (ca : odef (UnionCF A f supf z) a ) → b o< z → (ab : odef A b) + → HasPrev A (UnionCF A f supf z) f b ∨ IsSUP A (UnionCF A f supf b) ab + → * a < * b → odef ((UnionCF A f supf z)) b record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -548,8 +462,8 @@ ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative init-uchain : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) - { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y -init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl) ⟫ + { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f supf x) y +init-uchain A f mf ay = ⟪ ay , ? ⟫ record IChain (A : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where field @@ -586,25 +500,8 @@ spa ≡⟨ sym sax=spa ⟩ supfa x ∎ ) a ) where open o≤-Reasoning O - z53 : {z : Ordinal } → odef (UnionCF A f mf ay (ZChain.supf zb) x) z → odef (UnionCF A f mf ay (ZChain.supf za) x) z - z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - z53 {z} ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u u<x z54 z55 ⟫ where - ua=ub : supfa u ≡ supfb u - ua=ub = prev u u<x (ordtrans u<x x≤xa ) - order : {s z1 : Ordinal} → ZChain.supf za s o< ZChain.supf za u → FClosure A f (ZChain.supf za s) z1 → - (z1 ≡ ZChain.supf za u) ∨ (z1 << ZChain.supf za u) - order {s} {z1} lt fc = subst (λ k → z1 <= k) (sym ua=ub) - (ChainP.order is-sup (subst₂ ( λ j k → j o< k ) z56 ua=ub lt ) (subst (λ k → FClosure A f k z1 ) z56 fc )) where - s<x : s o< x - s<x = ordtrans (ZChain.supf-inject za lt) u<x - z56 : supfa s ≡ supfb s - z56 = prev s s<x (ordtrans s<x x≤xa) - z54 : ChainP A f mf ay (ZChain.supf za) u - z54 = record { fcy<sup = λ {w} fc → subst (λ k → w <= k ) (sym ua=ub) (ChainP.fcy<sup is-sup fc ) - ; order = order - ; supu=u = trans ua=ub (ChainP.supu=u is-sup) } - z55 : FClosure A f (ZChain.supf za u) z - z55 = subst (λ k → FClosure A f k z ) (sym ua=ub) fc + z53 : {z : Ordinal } → odef (UnionCF A f (ZChain.supf zb) x) z → odef (UnionCF A f (ZChain.supf za) x) z + z53 {z} ⟪ as , cp ⟫ = ⟪ as , ? ⟫ ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin supfa x ≡⟨ sax=spa ⟩ @@ -612,37 +509,18 @@ spb ≡⟨ sym sbx=spb ⟩ supfb x ∎ ) c ) where open o≤-Reasoning O - z53 : {z : Ordinal } → odef (UnionCF A f mf ay (ZChain.supf za) x) z → odef (UnionCF A f mf ay (ZChain.supf zb) x) z - z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - z53 {z} ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u u<x z54 z55 ⟫ where - ub=ua : supfb u ≡ supfa u - ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa )) - order : {s z1 : Ordinal} → ZChain.supf zb s o< ZChain.supf zb u → FClosure A f (ZChain.supf zb s) z1 → - (z1 ≡ ZChain.supf zb u) ∨ (z1 << ZChain.supf zb u) - order {s} {z1} lt fc = subst (λ k → z1 <= k) (sym ub=ua) - (ChainP.order is-sup (subst₂ ( λ j k → j o< k ) z56 ub=ua lt ) (subst (λ k → FClosure A f k z1 ) z56 fc )) where - s<x : s o< x - s<x = ordtrans (ZChain.supf-inject zb lt) u<x - z56 : supfb s ≡ supfa s - z56 = sym (prev s s<x (ordtrans s<x x≤xa)) - z54 : ChainP A f mf ay (ZChain.supf zb) u - z54 = record { fcy<sup = λ {w} fc → subst (λ k → w <= k ) (sym ub=ua) (ChainP.fcy<sup is-sup fc ) - ; order = order - ; supu=u = trans ub=ua (ChainP.supu=u is-sup) } - z55 : FClosure A f (ZChain.supf zb u) z - z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc + z53 : {z : Ordinal } → odef (UnionCF A f (ZChain.supf za) x) z → odef (UnionCF A f (ZChain.supf zb) x) z + z53 {z} ⟪ as , cp ⟫ = ⟪ as , ? ⟫ UChain-eq : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} {z y : Ordinal} {ay : odef A y} { supf0 supf1 : Ordinal → Ordinal } → (seq : {x : Ordinal } → x o< z → supf0 x ≡ supf1 x ) - → UnionCF A f mf ay supf0 z ≡ UnionCF A f mf ay supf1 z + → UnionCF A f supf0 z ≡ UnionCF A f supf1 z UChain-eq {A} {f} {mf} {z} {y} {ay} {supf0} {supf1} seq = ==→o≡ record { eq← = ueq← ; eq→ = ueq→ } where - ueq← : {x : Ordinal} → odef A x ∧ UChain A f mf ay supf1 z x → odef A x ∧ UChain A f mf ay supf0 z x - ueq← {z} ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫ - ueq← {z} ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u u<x ? ? ⟫ - ueq→ : {x : Ordinal} → odef A x ∧ UChain A f mf ay supf0 z x → odef A x ∧ UChain A f mf ay supf1 z x - ueq→ {z} ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫ - ueq→ {z} ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u u<x ? ? ⟫ + ueq← : {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ? + ueq← {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ + ueq→ : {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ? + ueq→ {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ Zorn-lemma : { A : HOD } → o∅ o< & A @@ -755,15 +633,13 @@ {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x SZ1 f mf mf< {y} ay zc x x≤A = zc1 x x≤A where chain-mono1 : {a b c : Ordinal} → a o≤ b - → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c + → odef (UnionCF A f (ZChain.supf zc) a) c → odef (UnionCF A f (ZChain.supf zc) b) c chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b - is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) - → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b - → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b + is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f (ZChain.supf zc) x) a → (ab : odef A b) + → HasPrev A (UnionCF A f (ZChain.supf zc) x) f b + → * a < * b → odef (UnionCF A f (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev - ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) - (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ + ... | ⟪ ab0 , cp ⟫ = ⟪ ab , ? ⟫ supf = ZChain.supf zc @@ -771,25 +647,25 @@ zc1 x x≤A with Oprev-p x ... | yes op = record { is-max = is-max } where px = Oprev.oprev op - is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → + is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f mf ay supf x) f b ∨ IsSUP A (UnionCF A f mf ay supf b) ab → - * a < * b → odef (UnionCF A f mf ay supf x) b + HasPrev A (UnionCF A f supf x) f b ∨ IsSUP A (UnionCF A f supf b) ab → + * a < * b → odef (UnionCF A f supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P 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 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) ... | case2 sb<sx = m10 where b<A : b o< & A b<A = z09 ab - m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b + m04 : ¬ HasPrev A (UnionCF A f supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ - m10 : odef (UnionCF A f mf ay supf x) b + m10 : odef (UnionCF A f supf x) b m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where - m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x ) + m17 : MinSUP A (UnionCF A f supf x) -- supf z o< supf ( supf x ) m17 = ZChain.minsup zc x≤A m18 : supf x ≡ MinSUP.sup m17 m18 = ZChain.supf-is-minsup zc x≤A @@ -797,39 +673,39 @@ m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x) m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where - m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b + m04 : ¬ HasPrev A (UnionCF A f supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x - m13 : odef (UnionCF A f mf ay supf x) z + m13 : odef (UnionCF A f supf x) z m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc ... | no lim = record { is-max = is-max } where - is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → + is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f mf ay supf x) f b ∨ IsSUP A (UnionCF A f mf ay supf b) ab → - * a < * b → odef (UnionCF A f mf ay supf x) b + HasPrev A (UnionCF A f supf x) f b ∨ IsSUP A (UnionCF A f supf b) ab → + * a < * b → odef (UnionCF A f supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P 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 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay ) - ... | 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 )) ⟫ + ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ? ⟫ ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) ... | case2 sb<sx = m10 where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) - m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b + m04 : ¬ HasPrev A (UnionCF A f supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫ -- ZChain on x - m10 : odef (UnionCF A f mf ay supf x) b + m10 : odef (UnionCF A f supf x) b m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where - m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x ) + m17 : MinSUP A (UnionCF A f supf x) -- supf z o< supf ( supf x ) m17 = ZChain.minsup zc x≤A m18 : supf x ≡ MinSUP.sup m17 m18 = ZChain.supf-is-minsup zc x≤A @@ -837,14 +713,14 @@ m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x) m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where - m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b + m04 : ¬ HasPrev A (UnionCF A f supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x - m13 : odef (UnionCF A f mf ay supf x) z + m13 : odef (UnionCF A f supf x) z m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD @@ -895,7 +771,7 @@ supf0 = ZChain.supf zc pchain : HOD - pchain = UnionCF A f mf ay supf0 px + pchain = UnionCF A f supf0 px supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b supf-mono = ZChain.supf-mono zc @@ -913,13 +789,13 @@ -- pchainpx : HOD - pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) + pchainpx = record { od = record { def = λ z → (odef A z ∧ ? ) ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where - zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A + zc00 : {z : Ordinal } → (odef A z ∧ ? ) ∨ FClosure A f (supf0 px) z → z o< & A zc00 {z} (case1 lt) = z07 lt zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc ) - zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b + zc02 : { a b : Ordinal } → odef A a ∧ ? → FClosure A f (supf0 px) b → a <= b zc02 {a} {b} ca fb = zc05 fb where zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl @@ -928,13 +804,13 @@ ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) ... | case2 lt = <=-trans (zc05 fb) (case2 lt) zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) - (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca ) + (subst (λ k → odef A k ∧ ?) (sym &iso) ca ) ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) ptotal : IsTotalOrderSet pchainpx ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso - (chain-total A f mf ay supf0 (proj2 a) (proj2 b)) + ? ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where eq1 : a0 ≡ b0 @@ -1009,18 +885,18 @@ ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (subst (λ k → a o≤ k) b a≤b))) refl ( supf-mono a≤b ) supf1-mono {a} {b} a≤b | tri> ¬a ¬b c with trio< a px ... | tri< a<px ¬b ¬c = zc19 where - zc21 : MinSUP A (UnionCF A f mf ay supf0 a) + zc21 : MinSUP A (UnionCF A f supf0 a) zc21 = ZChain.minsup zc (o<→≤ a<px) - zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) ) zc19 : supf0 a o≤ sp1 zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri≈ ¬a b ¬c = zc18 where - zc21 : MinSUP A (UnionCF A f mf ay supf0 a) + zc21 : MinSUP A (UnionCF A f supf0 a) zc21 = ZChain.minsup zc (o≤-refl0 b) zc20 : MinSUP.sup zc21 ≡ supf0 a zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) - zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) ) zc18 : supf0 a o≤ sp1 zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) @@ -1042,7 +918,7 @@ -- this is a kind of maximality, so we cannot prove this without <-monotonicity -- cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } - → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w + → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f supf1 b) w cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px ... | case2 px≤sa = z50 where a<x : a o< x @@ -1051,9 +927,9 @@ a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x) -- supf0 a ≡ px we cannot use previous cfcs, it is in the chain because -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x - z50 : odef (UnionCF A f mf ay supf1 b) w + z50 : odef (UnionCF A f supf1 b) w z50 with osuc-≡< px≤sa - ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc) ⟫ where + ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ? ⟫ where sa≤px : supf0 a o≤ px sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x spx=sa : supf0 px ≡ supf0 a @@ -1071,7 +947,7 @@ supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ supf1 (supf0 px) ∎ where open ≡-Reasoning - m : MinSUP A (UnionCF A f mf ay supf0 px) + m : MinSUP A (UnionCF A f supf0 px) m = ZChain.minsup zc o≤-refl m=spx : MinSUP.sup m ≡ supf1 (supf0 px) m=spx = begin @@ -1086,11 +962,9 @@ supf1 (supf0 a) ≡⟨ sf1=sf0 sa≤px ⟩ supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩ supf0 px ∎ where open ≡-Reasoning - cp : ChainP A f mf ay supf1 (supf0 px) - cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) - ; order = order - ; supu=u = z53 } where - uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 + cp : ? + cp = ? where + uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f supf0 px) z1 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) (sf1=sf0 (o<→≤ s<px)) fc ) where s<spx : s o< supf0 px @@ -1117,36 +991,12 @@ z53 = ordtrans<-≤ sa<b b≤x ... | case1 sa<px with trio< a px ... | tri< a<px ¬b ¬c = z50 where - z50 : odef (UnionCF A f mf ay supf1 b) w + z50 : odef (UnionCF A f supf1 b) w z50 with osuc-≡< b≤x ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ? - u≤px : u o≤ px - u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x ) - u<x : u o< x - u<x = ordtrans<-≤ u<b b≤x - cp1 : ChainP A f mf ay supf1 u - cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc ) - ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) - (sym (sf=eq u<x)) s<u) - (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc )) - ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) } + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ -- u o< px → u o< b ? z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫ where -- u o< px → u o< b ? - u<b : u o< b - u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc ) - u<x : u o< x - u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc ) - cp1 : ChainP A f mf ay supf1 u - cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc ) - ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) - (sym (sf=eq u<x)) s<u) - (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc )) - ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) } + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ where -- u o< px → u o< b ? ... | tri≈ ¬a a=px ¬c = csupf1 where -- a ≡ px , b ≡ x, sp o≤ x px<b : px o< b @@ -1160,9 +1010,9 @@ z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc z53 : odef A w z53 = A∋fc {A} _ f mf fc - csupf1 : odef (UnionCF A f mf ay supf1 b) w + csupf1 : odef (UnionCF A f supf1 b) w csupf1 with trio< (supf0 px) x - ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫ where + ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ? ⟫ where spx = supf0 px spx≤px : supf0 px o≤ px spx≤px = zc-b<x _ sfpx<x @@ -1185,11 +1035,6 @@ supf1 spx ≡⟨ sf1=sf0 spx≤px ⟩ supf0 spx ≤⟨ ZChain.supf-mono zc spx≤px ⟩ supf0 px ∎ ) where open o≤-Reasoning O - cp1 : ChainP A f mf ay supf1 spx - cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) - ( ZChain.fcy<sup zc spx≤px fc ) - ; order = order - ; supu=u = z52 } ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case m12 : supf0 px ≡ sp1 @@ -1203,37 +1048,17 @@ ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans sfpx≤sp1 sp≤x))) -- x o< supf0 px o≤ sp1 ≤ x ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x - zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z - zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where - u≤px : u o≤ px - u≤px = zc-b<x _ u<x - zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 + zc11 : {z : Ordinal} → odef (UnionCF A f supf1 x) z → odef pchainpx z + zc11 {z} ⟪ az , cp ⟫ = zc21 ? where + zc21 : {z1 : Ordinal } → FClosure A f (supf1 ?) z1 → odef pchainpx z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc - ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ + ... | case1 ⟪ ua1 , cp ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ? ⟫ ... | case2 fc = case2 (fsuc _ fc) - zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px record {fcy<sup = zc13 ; order = zc17 - ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where - u<px : u o< px - u<px = ZChain.supf-inject zc a - asp0 : odef A (supf0 u) - asp0 = ZChain.asupf zc - zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → - FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 u≤px)) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 u≤px)) ss<spx) (fcpu fc zc18) ) where - zc18 : s o≤ px - zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + zc21 (init asp refl ) = ? record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field - tsup : MinSUP A (UnionCF A f mf ay supf1 z) + tsup : MinSUP A (UnionCF A f supf1 z) tsup=sup : supf1 z ≡ MinSUP.sup tsup sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x @@ -1241,27 +1066,26 @@ ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where m = ZChain.minsup zc (o<→≤ a) - ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) - ms00 {w} ⟪ az , ch-init fc ⟫ = MinSUP.x≤sup m ? - ms00 {w} ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = MinSUP.x≤sup m ⟪ az , ch-is-sup u ? ? ? ⟫ + ms00 : {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 {w} ⟪ az , cp ⟫ = MinSUP.x≤sup m ⟪ az , ? ⟫ ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → - odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m us ? ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where m = ZChain.minsup zc (o≤-refl0 b) - ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 : {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) ms00 {x} ux = MinSUP.x≤sup m ? ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → - odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m us ? ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where m = sup1 - ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 : {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) ms00 {x} ux = MinSUP.x≤sup m ? ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → - odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m us ? @@ -1272,7 +1096,7 @@ -- supf1 x ≡ supf0 px because of supfmax cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } - → a o< b → b o≤ x → supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w + → a o< b → b o≤ x → supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f supf0 b) w cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc @@ -1288,8 +1112,8 @@ -- supf a ≡ px -- a o< px → odef U w -- a ≡ px → supf px ≡ px → odef U w - cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w - cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b cp fc1 ⟫ where + cfcs0 : a ≡ px → odef (UnionCF A f supf0 b) w + cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ? ⟫ where spx<b : supf0 px o< b spx<b = subst (λ k → supf0 k o< b) a=px sa<b cs01 : supf0 a ≡ supf0 (supf0 px) @@ -1297,64 +1121,36 @@ (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x)))) fc1 : FClosure A f (supf0 (supf0 px)) w fc1 = subst (λ k → FClosure A f k w) cs01 fc - m : MinSUP A (UnionCF A f mf ay supf0 (supf0 px)) + m : MinSUP A (UnionCF A f supf0 (supf0 px)) m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x)) m=sa : MinSUP.sup m ≡ supf0 (supf0 px) m=sa = begin MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x) )) ⟩ supf0 (supf0 px) ∎ where open ≡-Reasoning - cp : ChainP A f mf ay supf0 (supf0 px) - cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) - ; order = order - ; supu=u = sym (trans (cong supf0 (sym a=px)) cs01) } where - uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 px) → FClosure A f (supf0 s) z1 - → odef (UnionCF A f mf ay supf0 (supf0 px)) z1 - uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<spx spx≤px - (subst (λ k → supf0 s o< k) (sym (trans (cong supf0 (sym a=px)) cs01) ) ss<sp) fc where - s<spx : s o< supf0 px - s<spx = ZChain.supf-inject zc ss<sp - spx≤px : supf0 px o≤ px - spx≤px = zc-b<x _ (ordtrans<-≤ spx<b b≤x) - order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 px) → - FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 px)) ∨ (z1 << supf0 (supf0 px)) - order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) ) - cfcs1 : odef (UnionCF A f mf ay supf0 b) w + cfcs1 : odef (UnionCF A f supf0 b) w cfcs1 with trio< a px ... | tri< a<px ¬b ¬c = cfcs2 where sa<x : supf0 a o< x sa<x = ordtrans<-≤ sa<b b≤x - cfcs2 : odef (UnionCF A f mf ay supf0 b) w + cfcs2 : odef (UnionCF A f supf0 b) w cfcs2 with trio< (supf0 a) px ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x) ⟫ ) ... | tri≈ ¬a sa=px ¬c with trio< a px - ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b cp fc1 ⟫ where + ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ? ⟫ where cs01 : supf0 a ≡ supf0 (supf0 a) cs01 = sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x))) fc1 : FClosure A f (supf0 (supf0 a)) w fc1 = subst (λ k → FClosure A f k w) cs01 fc - m : MinSUP A (UnionCF A f mf ay supf0 (supf0 a)) + m : MinSUP A (UnionCF A f supf0 (supf0 a)) m = ZChain.minsup zc (o≤-refl0 sa=px) m=sa : MinSUP.sup m ≡ supf0 (supf0 a) m=sa = begin MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (o≤-refl0 sa=px) ) ⟩ supf0 (supf0 a) ∎ where open ≡-Reasoning - cp : ChainP A f mf ay supf0 (supf0 a) - cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) - ; order = order - ; supu=u = sym cs01 } where - uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 a) → FClosure A f (supf0 s) z1 - → odef (UnionCF A f mf ay supf0 (supf0 a)) z1 - uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< (ZChain.supf-inject zc ss<sp) - (zc-b<x _ (ordtrans<-≤ sa<b b≤x)) ss<sa fc where - ss<sa : supf0 s o< supf0 a - ss<sa = subst (λ k → supf0 s o< k ) (sym cs01) ss<sp - order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 a) → - FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 a)) ∨ (z1 << supf0 (supf0 a)) - order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) ) ... | tri≈ ¬a a=px ¬c = cfcs0 a=px ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) ) ⟫ ) ... | tri≈ ¬a a=px ¬c = cfcs0 a=px @@ -1368,26 +1164,12 @@ zc177 : supf0 z ≡ supf0 px zc177 = ZChain.supfmax zc px<z -- px o< z, px o< supf0 px - zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) z → odef pchainpx z - zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where - u≤px : u o≤ px - u≤px = zc-b<x _ u<x - zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef pchainpx z1 - zc21 {z1} (fsuc z2 fc ) with zc21 fc - ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ - ... | case2 fc = case2 (fsuc _ fc) - zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf0 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px is-sup (init asp refl ) ⟫ where - u<px : u o< px - u<px = ZChain.supf-inject zc a - ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym b )) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + zc11 : {z : Ordinal} → odef (UnionCF A f supf0 x) z → odef pchainpx z + zc11 {z} ⟪ az , cp ⟫ = ? where record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field - tsup : MinSUP A (UnionCF A f mf ay supf0 z) + tsup : MinSUP A (UnionCF A f supf0 z) tsup=sup : supf0 z ≡ MinSUP.sup tsup sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x @@ -1400,7 +1182,7 @@ ... | case1 eq = eq ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) zc32 = ZChain.sup zc o≤-refl - zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) + zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) zc34 ne {w} lt = ? zc33 : supf0 z ≡ & (SUP.sup zc32) zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl ) @@ -1411,10 +1193,10 @@ ... | tri< a ¬b ¬c = zc36 ¬b ... | tri> ¬a ¬b c = zc36 ¬b ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ? } where - zc37 : MinSUP A (UnionCF A f mf ay supf0 z) + zc37 : MinSUP A (UnionCF A f supf0 z) zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? } sup=u : {b : Ordinal} (ab : odef A b) → - b o≤ x → IsMinSUP A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → supf0 b ≡ b + b o≤ x → IsMinSUP A (UnionCF A f supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f supf0 b) f b ) → supf0 b ≡ b sup=u {b} ab b≤x is-sup with trio< b px ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ @@ -1489,14 +1271,14 @@ ... | tri> ¬a ¬b c = spu pchain : HOD - pchain = UnionCF A f mf ay supf1 x + pchain = UnionCF A f supf1 x -- pchain ⊆ pchainx ptotal : IsTotalOrderSet pchain ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) + uz01 = ? -- chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z sf1=sf {z} z<x with trio< z x @@ -1533,7 +1315,7 @@ ... | tri> ¬a ¬b c = ? cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } - → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w + → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f supf1 b) w cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x ... | case1 b=x with trio< a x ... | tri< a<x ¬b ¬c = zc40 where @@ -1557,37 +1339,11 @@ sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ ) fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc - zcm : odef (UnionCF A f mf ay (ZChain.supf (pzc (ob<x lim m<x))) (osuc (omax a sa))) w + zcm : odef (UnionCF A f (ZChain.supf (pzc (ob<x lim m<x))) (osuc (omax a sa))) w zcm = ZChain.cfcs (pzc (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm - zc40 : odef (UnionCF A f mf ay supf1 b) w + zc40 : odef (UnionCF A f supf1 b) w zc40 with ZChain.cfcs (pzc (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b cp fc2 ⟫ where - zc55 : u o< osuc m - zc55 = u<x - u<b : u o< b - u<b = subst (λ k → u o< k ) (sym b=x) ( ordtrans u<x (ob<x lim m<x)) - fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w - fc1m = fc1 - fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) w - fc1a = fc - fc2 : FClosure A f (supf1 u) w - fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) ) fc1 where - zc57 : osuc u o≤ osuc m - zc57 = osucc u<x - sb=sa : {a : Ordinal } → a o≤ m → supf1 a ≡ ZChain.supf (pzc (ob<x lim m<x)) a - sb=sa {a} a≤m = trans (sf1=sf (ordtrans≤-< a≤m m<x)) (zeq _ _ (osucc a≤m) (o<→≤ <-osuc)) - cp : ChainP A f mf ay supf1 u - cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) (ChainP.fcy<sup is-sup fc ) - ; order = order - ; supu=u = trans (sb=sa u<x ) (ChainP.supu=u is-sup) } where - order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sb=sa s≤m) (sb=sa u<x) s<u) - (subst (λ k → FClosure A f k z) (sb=sa s≤m ) fc )) where - s≤m : s o≤ m - s≤m = ordtrans (supf-inject0 supf-mono s<u ) u<x + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where @@ -1597,26 +1353,14 @@ fcb : FClosure A f (supfb a) w fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc -- supfb a o< b assures it is in Union b - zcb : odef (UnionCF A f mf ay supfb b) w + zcb : odef (UnionCF A f supfb b) w zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb - zc40 : odef (UnionCF A f mf ay supf1 b) w + zc40 : odef (UnionCF A f supf1 b) w zc40 with zcb - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x cp (subst (λ k → FClosure A f k w) (sym (sb=sa u<x)) fc1 ) ⟫ where - cp : ChainP A f mf ay supf1 u - cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) (ChainP.fcy<sup is-sup fc ) - ; order = order - ; supu=u = trans (sb=sa u<x) (ChainP.supu=u is-sup) } where - order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sb=sa s<b) (sb=sa u<x) s<u) - (subst (λ k → FClosure A f k z) (sb=sa s<b ) fc )) where - s<b : s o< b - s<b = ordtrans (supf-inject0 supf-mono s<u ) u<x + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ sup=u : {b : Ordinal} (ab : odef A b) → - b o≤ x → IsMinSUP A (UnionCF A f mf ay supf1 b) supf1 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b + b o≤ x → IsMinSUP A (UnionCF A f supf1 b) supf1 ab ∧ (¬ HasPrev A (UnionCF A f supf1 b) f b ) → supf1 b ≡ b sup=u {b} ab b≤x is-sup with osuc-≡< b≤x ... | case1 b=x = ? where zc31 : spu o≤ b @@ -1633,8 +1377,8 @@ msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → (zc : ZChain A f mf ay x ) - → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x) - msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc) + → MinSUP A (UnionCF A f (ZChain.supf zc) x) + msp0 f mf {x} ay zc = minsupP (UnionCF A f (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc) fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) → (sp1 : MinSUP A (ZChain.chain zc)) @@ -1647,7 +1391,7 @@ asp : odef A sp asp = MinSUP.asm sp1 z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b ) - → HasPrev A chain f b ∨ IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab + → HasPrev A chain f b ∨ IsSUP A (UnionCF A f (ZChain.supf zc) b) ab → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl ) z22 : sp o< & A @@ -1660,9 +1404,9 @@ z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ) ... | case1 eq = ⊥-elim ( ne eq ) ... | case2 lt = lt - z19 : IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp + z19 : IsSUP A (UnionCF A f (ZChain.supf zc) sp) asp z19 = record { x≤sup = z20 } where - z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) + z20 : {y : Ordinal} → odef (UnionCF A f (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) z20 {y} zy with MinSUP.x≤sup sp1 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22) zy )) ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )