Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1033:2da8dcbb0825
ch-init again, because ch-is-sup require u<x which is not valid supf o∅
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 01 Dec 2022 11:31:15 +0900 |
| parents | 382680c3e9be |
| children | 84881efe649b |
| files | src/zorn.agda |
| diffstat | 1 files changed, 146 insertions(+), 142 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 30 20:43:01 2022 +0900 +++ b/src/zorn.agda Thu Dec 01 11:31:15 2022 +0900 @@ -286,23 +286,16 @@ ∈∧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 supf x --- = record { od = record { def = λ z → odef A z ∧ UChain A f supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } +-- Union of supf z and FClosure A f y --- order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y --- +data UChain { A : HOD } { f : Ordinal → Ordinal } {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) + (x : Ordinal) : (z : Ordinal) → Set n where + ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z + ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z -data UChain { A : HOD } { f : Ordinal → Ordinal } - {supf : Ordinal → Ordinal} (x : Ordinal) : (z : Ordinal) → Set n where - ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain x z - -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 ∧ UChain {A} {f} {supf} x z } ; +UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD +UnionCF A f ay supf x + = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } @@ -335,11 +328,11 @@ 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 supf x) - → SUP A (UnionCF A f supf x) + → MinSUP A (UnionCF A f ay supf x) + → SUP A (UnionCF A f ay supf x) M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms) ; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.as ms) ; x≤sup = ms00 } } where - ms00 : {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ & (* (MinSUP.sup ms))) ∨ (z << & (* (MinSUP.sup ms))) + ms00 : {z : Ordinal} → odef (UnionCF A f ay supf x) z → (z ≡ & (* (MinSUP.sup ms))) ∨ (z << & (* (MinSUP.sup ms))) ms00 {z} uz with MinSUP.x≤sup ms uz ... | case1 eq = case1 (subst (λ k → z ≡ k) (sym &iso) eq) ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt ) @@ -347,7 +340,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 supf a) c → odef (UnionCF A f supf b) c + → odef (UnionCF A f ay supf a) c → odef (UnionCF A f 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 ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) @@ -355,38 +349,30 @@ field supf : Ordinal → Ordinal + order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y + 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 supf b) w - fcy<sup : {w : Ordinal } → FClosure A f y w → (w ≡ supf o∅ ) ∨ ( w << supf o∅ ) - order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y + {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w 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 - is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f supf x) (supf x) + is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z - → IsSUP A (UnionCF A f supf b) b ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b + → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b chain : HOD - chain = UnionCF A f supf z + chain = UnionCF A f ay supf z chain⊆A : chain ⊆' A chain⊆A = λ lt → proj1 lt - chain∋init : odef chain y - 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 , cp ⟫ = ? - initial : {z : Ordinal } → odef chain z → y ≤ z - 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 with trio< (& a) (& b) - -- ... | tri> ¬a ¬b c = ? - -- ... | tri≈ ¬a b ¬c = ? - -- ... | tri< a ¬b ¬c = ? + chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y + chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl) ⟫ + + f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a) + f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-init (fsuc _ fc) ⟫ + f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-is-sup u su<x su=u (fsuc _ fc) ⟫ supf-inject : {x y : Ordinal } → supf x o< supf y → x o< y supf-inject {x} {y} sx<sy with trio< x y @@ -400,39 +386,56 @@ 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 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 ay 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) - minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f supf x) + minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f ay supf x) minsup {x} x≤z = record { sup = supf x ; isMinSUP = is-minsup x≤z } supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup (minsup x≤z) supf-is-minsup _ = refl - chain-minsup : {x : Ordinal} → IsMinSUP A (UnionCF A f supf x) (supf x) - chain-minsup {x} = record { as = as ; x≤sup = cp1 ; minsup = cpm } where - as : odef A (supf x) - as = asupf - cp1 : {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ supf x) ∨ (z << supf x) - cp1 {z} ⟪ az , ch-is-sup u u<x supu=u fc ⟫ = order u<x fc - cpm : {s : Ordinal} → odef A s → ({z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ s) ∨ (z << s)) → supf x o≤ s - cpm {s} as z≤s with trio< (supf x) s - ... | tri< a ¬b ¬c = o<→≤ a - ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b c = ? where - cp4 : supf (supf s) ≡ supf s - cp4 = ? - cp3 : supf s o< x - cp3 = ? - cp2 : odef (UnionCF A f supf x) (supf s) - cp2 = ⟪ asupf , ch-is-sup (supf s) cp3 cp4 (init asupf cp4) ⟫ --- ... | case1 eq = ? --- ... | case2 lt = ? + -- different from order because y o< supf + fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) + 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 ) ⟫ + ... | 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 ) + + initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x → y ≤ x + initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc + initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc) + + f-total : IsTotalOrderSet chain + f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = + subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fc-total A f mf supf order fca fcb) + f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where + ft01 : (& a) ≤ (& b) → Tri ( a < b) ( a ≡ b) ( b < a ) + ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where + a=b : a ≡ b + a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) + ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) where + a<b : a < b + a<b = subst₂ (λ j k → j < k ) *iso *iso lt + ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) + ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb)) + f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where + ft01 : (& b) ≤ (& a) → Tri ( a < b) ( a ≡ b) ( b < a ) + ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where + a=b : a ≡ b + a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq)) + ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where + b<a : b < a + b<a = subst₂ (λ j k → j < k ) *iso *iso lt + ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) + ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) + f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = + subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb ) IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp - → ({y : Ordinal} → odef (UnionCF A f supf x) y → (y ≡ sp ) ∨ (y << sp )) + → ({y : Ordinal} → odef (UnionCF A f ay supf x) y → (y ≡ sp ) ∨ (y << sp )) → ( {a : Ordinal } → odef A a → a << f a ) - → ¬ ( HasPrev A (UnionCF A f supf x) f sp ) + → ¬ ( HasPrev A (UnionCF A f ay supf x) f sp ) IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<<-irr fsp≤sp sp<fsp ) where sp<fsp : sp << f sp sp<fsp = <-mono-f asp @@ -444,18 +447,19 @@ supf-¬hp : {x : Ordinal } → x o≤ z → ( {a : Ordinal } → odef A a → a << f a ) - → ¬ ( HasPrev A (UnionCF A f supf x) f (supf x) ) + → ¬ ( HasPrev A (UnionCF A f ay 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 supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) + z54 : {w : Ordinal} → odef (UnionCF A f 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 su=u fc ⟫ = order su<b fc where su<b : u o< b su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) z52 : supf (supf b) ≡ supf b - z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ + z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; 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 supf (supf b) -- the condition of cfcs is satisfied, this is obvious @@ -464,9 +468,9 @@ {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 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) b - → * a < * b → odef ((UnionCF A f supf z)) b + is-max : {a b : Ordinal } → (ca : odef (UnionCF A f ay supf z) a ) → b o< z → (ab : odef A b) + → HasPrev A (UnionCF A f ay supf z) f b ∨ IsSUP A (UnionCF A f ay supf b) b + → * a < * b → odef ((UnionCF A f ay supf z)) b record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -474,10 +478,6 @@ as : A ∋ maximal ¬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 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 i : Ordinal @@ -513,7 +513,7 @@ spa ≡⟨ sym sax=spa ⟩ supfa x ∎ ) a ) where open o≤-Reasoning O - z53 : {z : Ordinal } → odef (UnionCF A f (ZChain.supf zb) x) z → odef (UnionCF A f (ZChain.supf za) x) z + z53 : {z : Ordinal } → odef (UnionCF A f ay (ZChain.supf zb) x) z → odef (UnionCF A f ay (ZChain.supf za) x) z z53 {z} ⟪ as , cp ⟫ = ⟪ as , ? ⟫ ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin @@ -522,13 +522,13 @@ spb ≡⟨ sym sbx=spb ⟩ supfb x ∎ ) c ) where open o≤-Reasoning O - z53 : {z : Ordinal } → odef (UnionCF A f (ZChain.supf za) x) z → odef (UnionCF A f (ZChain.supf zb) x) z + z53 : {z : Ordinal } → odef (UnionCF A f ay (ZChain.supf za) x) z → odef (UnionCF A f ay (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 supf0 z ≡ UnionCF A f supf1 z + → UnionCF A f ay supf0 z ≡ UnionCF A f ay 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 ∧ ? → odef A x ∧ ? ueq← {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ @@ -646,11 +646,11 @@ {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 (ZChain.supf zc) a) c → odef (UnionCF A f (ZChain.supf zc) b) c + → odef (UnionCF A f ay (ZChain.supf zc) a) c → odef (UnionCF A f ay (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 (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 : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) x) a → (ab : odef A b) + → HasPrev A (UnionCF A f ay (ZChain.supf zc) x) f b + → * a < * b → odef (UnionCF A f ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , cp ⟫ = ⟪ ab , ? ⟫ @@ -660,25 +660,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 supf x) a → + is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f supf x) f b ∨ IsSUP A (UnionCF A f supf b) ? → - * a < * b → odef (UnionCF A f supf x) b + HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) ? → + * a < * b → odef (UnionCF A f ay 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 supf b) f b + m04 : ¬ HasPrev A (UnionCF A f ay 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 supf x) b + m10 : odef (UnionCF A f ay 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 supf x) -- supf z o< supf ( supf x ) + m17 : MinSUP A (UnionCF A f ay 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 @@ -686,39 +686,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 supf b) f b + m04 : ¬ HasPrev A (UnionCF A f ay 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 supf x) z + m13 : odef (UnionCF A f ay 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 supf x) a → + is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f supf x) f b ∨ IsSUP A (UnionCF A f supf b) b → - * a < * b → odef (UnionCF A f supf x) b + HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) b → + * a < * b → odef (UnionCF A f ay 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 ) + 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 ? ) ... | 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 supf b) f b + m04 : ¬ HasPrev A (UnionCF A f ay 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 supf x) b + m10 : odef (UnionCF A f ay 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 supf x) -- supf z o< supf ( supf x ) + m17 : MinSUP A (UnionCF A f ay 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 @@ -726,14 +726,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 supf b) f b + m04 : ¬ HasPrev A (UnionCF A f ay 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 supf x) z + m13 : odef (UnionCF A f ay 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 @@ -784,7 +784,7 @@ supf0 = ZChain.supf zc pchain : HOD - pchain = UnionCF A f supf0 px + pchain = UnionCF A f ay supf0 px supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b supf-mono = ZChain.supf-mono zc @@ -893,18 +893,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 supf0 a) + zc21 : MinSUP A (UnionCF A f ay supf0 a) zc21 = ZChain.minsup zc (o<→≤ a<px) - zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 : {x₁ : Ordinal} → odef (UnionCF A f ay 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.as sup1) zc24 ) ... | tri≈ ¬a b ¬c = zc18 where - zc21 : MinSUP A (UnionCF A f supf0 a) + zc21 : MinSUP A (UnionCF A f ay 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 supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 : {x₁ : Ordinal} → odef (UnionCF A f ay 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.as sup1) zc24 ) @@ -926,7 +926,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 supf1 b) w + → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay 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 @@ -935,7 +935,7 @@ 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 supf1 b) w + z50 : odef (UnionCF A f ay supf1 b) w z50 with osuc-≡< px≤sa ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ? ⟫ where sa≤px : supf0 a o≤ px @@ -955,7 +955,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 supf0 px) + m : MinSUP A (UnionCF A f ay supf0 px) m = ZChain.minsup zc o≤-refl m=spx : MinSUP.sup m ≡ supf1 (supf0 px) m=spx = begin @@ -972,7 +972,7 @@ supf0 px ∎ where open ≡-Reasoning 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 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f ay 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 @@ -999,7 +999,7 @@ 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 supf1 b) w + z50 : odef (UnionCF A f ay 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 , cp ⟫ = ⟪ az , ? ⟫ -- u o< px → u o< b ? @@ -1018,7 +1018,7 @@ 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 supf1 b) w + csupf1 : odef (UnionCF A f ay supf1 b) w csupf1 with trio< (supf0 px) x ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ? ⟫ where spx = supf0 px @@ -1056,7 +1056,7 @@ ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans ? 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 supf1 x) z → odef pchainpx z + zc11 : {z : Ordinal} → odef (UnionCF A f ay 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 @@ -1066,7 +1066,7 @@ record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field - tsup : MinSUP A (UnionCF A f supf1 z) + tsup : MinSUP A (UnionCF A f ay supf1 z) tsup=sup : supf1 z ≡ MinSUP.sup tsup sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x @@ -1074,26 +1074,26 @@ ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.as 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 supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 : {x : Ordinal} → odef (UnionCF A f ay 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 supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + odef (UnionCF A f ay 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.as 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 supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 : {x : Ordinal} → odef (UnionCF A f ay 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 supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + odef (UnionCF A f ay 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.as sup1 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where m = sup1 - ms00 : {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 : {x : Ordinal} → odef (UnionCF A f ay 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 supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m us ? @@ -1104,7 +1104,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 supf0 b) w + → a o< b → b o≤ x → supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f ay 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 @@ -1120,7 +1120,7 @@ -- supf a ≡ px -- a o< px → odef U w -- a ≡ px → supf px ≡ px → odef U w - cfcs0 : a ≡ px → odef (UnionCF A f supf0 b) w + cfcs0 : a ≡ px → odef (UnionCF A f ay 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 @@ -1129,7 +1129,7 @@ (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 supf0 (supf0 px)) + m : MinSUP A (UnionCF A f ay 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 @@ -1137,12 +1137,12 @@ supf0 (supf0 px) ∎ where open ≡-Reasoning - cfcs1 : odef (UnionCF A f supf0 b) w + cfcs1 : odef (UnionCF A f ay 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 supf0 b) w + cfcs2 : odef (UnionCF A f ay 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 ) @@ -1153,7 +1153,7 @@ 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 supf0 (supf0 a)) + m : MinSUP A (UnionCF A f ay supf0 (supf0 a)) m = ZChain.minsup zc (o≤-refl0 sa=px) m=sa : MinSUP.sup m ≡ supf0 (supf0 a) m=sa = begin @@ -1172,12 +1172,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 supf0 x) z → odef pchainpx z + zc11 : {z : Ordinal} → odef (UnionCF A f ay supf0 x) z → odef pchainpx z zc11 {z} ⟪ az , cp ⟫ = ? record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field - tsup : MinSUP A (UnionCF A f supf0 z) + tsup : MinSUP A (UnionCF A f ay supf0 z) tsup=sup : supf0 z ≡ MinSUP.sup tsup sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x @@ -1190,7 +1190,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 = ? - zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) + zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f ay 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 ) @@ -1201,10 +1201,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 supf0 z) + zc37 : MinSUP A (UnionCF A f ay 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 supf0 b) b ∧ (¬ HasPrev A (UnionCF A f supf0 b) f b ) → supf0 b ≡ b + b o≤ x → IsMinSUP A (UnionCF A f ay supf0 b) b ∧ (¬ HasPrev A (UnionCF A f ay 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 } , ? ⟫ ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫ @@ -1218,7 +1218,10 @@ zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) zc32 = ? - ... | no lim = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ? + ... | no lim with trio< x o∅ + ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) + ... | tri≈ ¬a b ¬c = record { supf = ? } + ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z @@ -1279,7 +1282,7 @@ ... | tri> ¬a ¬b c = spu pchain : HOD - pchain = UnionCF A f supf1 x + pchain = UnionCF A f ay supf1 x -- pchain ⊆ pchainx @@ -1316,7 +1319,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 supf1 b) w + → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay 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 @@ -1340,9 +1343,9 @@ 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 (ZChain.supf (pzc (ob<x lim m<x))) (osuc (omax a sa))) w + zcm : odef (UnionCF A f ay (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 supf1 b) w + zc40 : odef (UnionCF A f ay supf1 b) w zc40 with ZChain.cfcs (pzc (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) @@ -1354,14 +1357,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 supfb b) w + zcb : odef (UnionCF A f ay 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 supf1 b) w + zc40 : odef (UnionCF A f ay supf1 b) w zc40 with zcb ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ sup=u : {b : Ordinal} (ab : odef A b) → - b o≤ x → IsMinSUP A (UnionCF A f supf1 b) b ∧ (¬ HasPrev A (UnionCF A f supf1 b) f b ) → supf1 b ≡ b + 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 sup=u {b} ab b≤x is-sup with osuc-≡< b≤x ... | case1 b=x = ? where zc31 : spu o≤ b @@ -1378,8 +1381,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 (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) + → MinSUP A (UnionCF A f ay (ZChain.supf zc) x) + msp0 f mf {x} ay zc = minsupP (UnionCF A f ay (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)) @@ -1391,23 +1394,24 @@ sp = MinSUP.sup sp1 asp : odef A sp asp = MinSUP.as sp1 + ay = as0 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 (ZChain.supf zc) b) b + → HasPrev A chain f b ∨ IsSUP A (UnionCF A f ay (ZChain.supf zc) b) b → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl ) z22 : sp o< & A z22 = z09 asp z12 : odef chain sp z12 with o≡? (& s) sp - ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | 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 + ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ? ) + ... | 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 z13 : * (& s) < * sp - z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ) + z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ? ) ... | case1 eq = ⊥-elim ( ne eq ) ... | case2 lt = lt - z19 : IsSUP A (UnionCF A f (ZChain.supf zc) sp) sp + z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp z19 = record { x≤sup = z20 } where - z20 : {y : Ordinal} → odef (UnionCF A f (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) + z20 : {y : Ordinal} → odef (UnionCF A f ay (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 )