Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1031:f276cf614fc5
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 30 Nov 2022 10:16:02 +0900 |
| parents | 40532b0ed230 |
| children | 382680c3e9be |
| files | src/zorn.agda |
| diffstat | 1 files changed, 106 insertions(+), 128 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Nov 28 18:53:10 2022 +0900 +++ b/src/zorn.agda Wed Nov 30 10:16:02 2022 +0900 @@ -23,7 +23,7 @@ import BAlgbra open import Data.Nat hiding ( _<_ ; _≤_ ) -open import Data.Nat.Properties +open import Data.Nat.Properties open import nat @@ -55,8 +55,8 @@ _<<_ : (x y : Ordinal ) → Set n x << y = * x < * y -_<=_ : (x y : Ordinal ) → Set n -- we can't use * x ≡ * y, it is Set (Level.suc n). Level (suc n) troubles Chain -x <= y = (x ≡ y ) ∨ ( * x < * y ) +_≤_ : (x y : Ordinal ) → Set n -- we can't use * x ≡ * y, it is Set (Level.suc n). Level (suc n) troubles Chain +x ≤ y = (x ≡ y ) ∨ ( * x < * y ) POO : IsStrictPartialOrder _≡_ _<<_ POO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } @@ -64,36 +64,19 @@ ; irrefl = λ x=y x<y → IsStrictPartialOrder.irrefl PO (cong (*) x=y) x<y ; <-resp-≈ = record { fst = λ {x} {y} {y1} y=y1 xy1 → subst (λ k → x << k ) y=y1 xy1 ; snd = λ {x} {x1} {y} x=x1 x1y → subst (λ k → k << x ) x=x1 x1y } } -_≤_ : (x y : HOD) → Set (Level.suc n) -x ≤ y = ( x ≡ y ) ∨ ( x < y ) - -≤-ftrans : {x y z : HOD} → x ≤ y → y ≤ z → x ≤ z +≤-ftrans : {x y z : Ordinal } → x ≤ y → y ≤ z → x ≤ z ≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl ≤-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) -<=-trans : {x y z : Ordinal } → x <= y → y <= z → x <= z -<=-trans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl -<=-trans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z -<=-trans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y -<=-trans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) - -ftrans<=-< : {x y z : Ordinal } → x <= y → y << z → x << z -ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq)) y<z -ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z +ftrans≤-< : {x y z : Ordinal } → x ≤ y → y << z → x << z +ftrans≤-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq)) y<z +ftrans≤-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z -ftrans<-<= : {x y z : Ordinal } → x << y → y <= z → x << z -ftrans<-<= {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y -ftrans<-<= {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt - -<=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y -<=to≤ (case1 eq) = case1 (cong (*) eq) -<=to≤ (case2 lt) = case2 lt - -≤to<= : {x y : Ordinal } → * x ≤ * y → x <= y -≤to<= (case1 eq) = case1 ( subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) eq) ) -≤to<= (case2 lt) = case2 lt +ftrans<-≤ : {x y z : Ordinal } → x << y → y ≤ z → x << z +ftrans<-≤ {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y +ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (sym a=b) b<a @@ -113,8 +96,8 @@ -- Closure of ≤-monotonic function f has total order -- -≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n) -≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧ odef A (f x ) +≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n +≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( x ≤ (f x) ) ∧ odef A (f x ) <-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n <-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x < * (f x) ) ∧ odef A (f x ) @@ -131,12 +114,12 @@ A∋fcs {A} s f mf (init as refl) = as A∋fcs {A} s f mf (fsuc y fcy) = A∋fcs {A} s f mf fcy -s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y +s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → s ≤ y s≤fc {A} s {.s} f mf (init x refl ) = case1 refl s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) ) -... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy ) +... | case1 x=fx = subst₂ (λ j k → j ≤ k ) refl x=fx (s≤fc s f mf fcy) ... | case2 x<fx with s≤fc {A} s f mf fcy -... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx ) +... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym (cong (*) s≡x )) refl x<fx ) ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx ) fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ @@ -155,33 +138,33 @@ fc07 : {x : Ordinal } (cx : FClosure A f s x ) → 0 ≡ fcn s mf cx → * s ≡ * x fc07 {x} (init as refl) eq = refl fc07 {.(f x)} (fsuc x cx) eq with proj1 (mf x (A∋fc s f mf cx ) ) - ... | case1 x=fx = subst (λ k → * s ≡ k ) x=fx ( fc07 cx eq ) + ... | case1 x=fx = subst (λ k → * s ≡ k ) (cong (*) x=fx) ( fc07 cx eq ) -- ... | case2 x<fx = ? fc00 : (i j : ℕ ) → i ≡ j → {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx → j ≡ fcn s mf cy → * x ≡ * y fc00 (suc i) (suc j) x cx (init x₃ x₄) x₁ x₂ = ⊥-elim ( fc06 x₄ x₂ ) fc00 (suc i) (suc j) x (init x₃ x₄) (fsuc x₅ cy) x₁ x₂ = ⊥-elim ( fc06 x₄ x₁ ) fc00 zero zero refl (init _ refl) (init x₁ refl) i=x i=y = refl fc00 zero zero refl (init as refl) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) ) - ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy (fc07 cy i=y) -- ( fc00 zero zero refl (init as refl) cy i=x i=y ) + ... | case1 y=fy = subst (λ k → * s ≡ * k ) y=fy (fc07 cy i=y) -- ( fc00 zero zero refl (init as refl) cy i=x i=y ) fc00 zero zero refl (fsuc x cx) (init as refl) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) - ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx (sym (fc07 cx i=x)) -- ( fc00 zero zero refl cx (init as refl) i=x i=y ) + ... | case1 x=fx = subst (λ k → * k ≡ * s ) x=fx (sym (fc07 cx i=x)) -- ( fc00 zero zero refl cx (init as refl) i=x i=y ) fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) - ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy i=x i=y ) + ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → * j ≡ * k ) x=fx y=fy ( fc00 zero zero refl cx cy i=x i=y ) fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) - ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy i=x j=y ) - ... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where + ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → * j ≡ * k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy i=x j=y ) + ... | case1 x=fx | case2 y<fy = subst (λ k → * k ≡ * (f y)) x=fx (fc02 x cx i=x) where fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) → suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y) fc02 x1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x) fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) ) - ... | case1 eq = trans (sym eq) ( fc02 x1 cx1 i=x1 ) -- derefence while f x ≡ x + ... | case1 eq = trans (sym (cong (*) eq )) ( fc02 x1 cx1 i=x1 ) -- derefence while f x ≡ x ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where fc04 : * x1 ≡ * y fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y) - ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy (fc03 y cy j=y) where + ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ * k ) y=fy (fc03 y cy j=y) where fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) → suc j ≡ fcn s mf cy1 → * (f x) ≡ * y1 fc03 y1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x) fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) ) - ... | case1 eq = trans ( fc03 y1 cy1 j=y1 ) eq + ... | case1 eq = trans ( fc03 y1 cy1 j=y1 ) (cong (*) eq) ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where fc05 : * x ≡ * y1 fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1) @@ -198,7 +181,7 @@ fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y fc01 (suc i) cx (init x₁ x₂) x (s≤s x₃) = ⊥-elim (fc06 x₂ x) fc01 (suc i) {y} cx (fsuc y1 cy) i=y (s≤s x<i) with proj1 (mf y1 (A∋fc s f mf cy ) ) - ... | case1 y=fy = subst (λ k → * x < k ) y=fy ( fc01 (suc i) {y1} cx cy i=y (s≤s x<i) ) + ... | case1 y=fy = subst (λ k → * x < k ) (cong (*) y=fy) ( fc01 (suc i) {y1} cx cy i=y (s≤s x<i) ) ... | case2 y<fy with <-cmp (fcn s mf cx ) i ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i c ) ... | tri≈ ¬a b ¬c = subst (λ k → k < * (f y1) ) (fcn-inject s mf cy cx (sym (trans b (cong pred i=y) ))) y<fy @@ -247,22 +230,17 @@ ay : odef B y x=fy : x ≡ f y -record IsSUP (A B : HOD) {x : Ordinal } (xa : odef A x) : Set n where +record IsSUP (A B : HOD) (x : Ordinal ) : Set n where field - x≤sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) - -record IsMinSUP (A B : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (xa : odef A x) : Set n where - field - x≤sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) - minsup : { sup1 : Ordinal } → odef A sup1 - → ( {z : Ordinal } → odef B z → (z ≡ sup1 ) ∨ (z << sup1 )) → x o≤ sup1 - not-hp : ¬ ( HasPrev A B f x ) + ax : odef A x + x≤sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -- B is Total, use positive record SUP ( A B : HOD ) : Set (Level.suc n) where field sup : HOD - as : A ∋ sup - x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive + isSUP : IsSUP A B (& sup) + ax = IsSUP.ax isSUP + x≤sup = IsSUP.x≤sup isSUP -- @@ -280,15 +258,15 @@ → (aa : odef A a ) →( {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl )) ... | case1 eq = trans eq (sym a=b) -... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-<= lt (≤to<= fc00 )) ) where - fc00 : * b ≤ * (f b) +... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-≤ lt fc00 ) ) where + fc00 : b ≤ (f b) fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa )) 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) + (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₁ ? +... | tri< a₁ ¬b ¬c with order a₁ ca ... | 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 @@ -296,7 +274,7 @@ ct02 : * a < * b ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri≈ a₁ ¬b ¬c = ? -fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri< a₁ ¬b ¬c = ? +fc-total A f mf supf order {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 @@ -309,7 +287,7 @@ -- 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 } --- order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf 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 } @@ -331,13 +309,20 @@ ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy ) ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) +record IsMinSUP ( A B : HOD ) (sup : Ordinal) : Set n where + field + axm : odef A sup + x≤sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup ) + minsup : { sup1 : Ordinal } → odef A sup1 + → ( {x : Ordinal } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 )) → sup o≤ sup1 + record MinSUP ( A B : HOD ) : Set n where field sup : Ordinal - asm : odef A sup - x≤sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup ) - minsup : { sup1 : Ordinal } → odef A sup1 - → ( {x : Ordinal } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 )) → sup o≤ sup1 + isMinSUP : IsMinSUP A B sup + axm = IsMinSUP.axm isMinSUP + x≤sup = IsMinSUP.x≤sup isMinSUP + minsup = IsMinSUP.minsup isMinSUP z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) @@ -347,7 +332,7 @@ → 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 + ; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.axm ms) ; x≤sup = ? } } where msup = MinSUP.sup ms ms00 : {z : HOD} → UnionCF A f supf x ∋ z → (z ≡ * msup) ∨ (z < * msup) ms00 {z} uz with MinSUP.x≤sup ms uz @@ -360,16 +345,21 @@ → 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 ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ +chain-minsup : {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) + {x : Ordinal} → IsMinSUP A (UnionCF A f supf x) x +chain-minsup = ? + 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 field supf : Ordinal → Ordinal sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z - → IsSUP A (UnionCF A f supf b) ab ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b + → IsSUP A (UnionCF A f supf b) b ∧ (¬ 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 supf b) w - order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y + 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 @@ -394,7 +384,7 @@ 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 : {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 @@ -427,20 +417,20 @@ → ({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 supf x) f sp ) - IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr ( <=to≤ fsp≤sp) sp<fsp ) where + IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr ? sp<fsp ) where sp<fsp : sp << f sp sp<fsp = <-mono-f asp pr = HasPrev.y hp - im00 : f (f pr) <= sp + im00 : f (f pr) ≤ sp im00 = is-sup ( f-next (f-next (HasPrev.ay hp))) - fsp≤sp : f sp <= sp - fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 + fsp≤sp : f sp ≤ sp + fsp≤sp = subst (λ k → f k ≤ sp ) (sym (HasPrev.x=fy hp)) im00 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) ) 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 + (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 @@ -459,7 +449,7 @@ 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) ab + → 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 record Maximal ( A : HOD ) : Set (Level.suc n) where @@ -503,7 +493,7 @@ ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( begin supfb x ≡⟨ sbx=spb ⟩ - spb ≤⟨ MinSUP.minsup mb (MinSUP.asm ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩ + spb ≤⟨ MinSUP.minsup mb (MinSUP.axm ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩ spa ≡⟨ sym sax=spa ⟩ supfa x ∎ ) a ) where open o≤-Reasoning O @@ -512,7 +502,7 @@ ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin supfa x ≡⟨ sax=spa ⟩ - spa ≤⟨ MinSUP.minsup ma (MinSUP.asm mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩ + spa ≤⟨ MinSUP.minsup ma (MinSUP.axm mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩ spb ≡⟨ sym sbx=spb ⟩ supfb x ∎ ) c ) where open o≤-Reasoning O @@ -588,7 +578,7 @@ ... | tri< a ¬b ¬c with prev z a ... | case2 mins = case2 mins ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z) - ... | case1 mins = case2 record { sup = z ; asm = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } where + ... | case1 mins = case2 record { sup = z ; isMinSUP = record { axm = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1 m04 {s} as lt with trio< z s ... | tri< a ¬b ¬c = o<→≤ a @@ -596,14 +586,14 @@ ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫ ) ... | case2 notz = case1 (λ _ → notz ) m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z) - m03 not = ⊥-elim ( not s1 (z09 (SUP.as S)) ⟪ SUP.as S , m05 ⟫ ) where + m03 not = ⊥-elim ( not s1 (z09 (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where S : SUP A B S = supP B B⊆A total s1 = & (SUP.sup S) m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 ) - m05 {w} bw with SUP.x≤sup S {* w} (subst (λ k → odef B k) (sym &iso) bw ) - ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) eq) ) - ... | case2 lt = case2 ( subst (λ k → _ < k ) (sym *iso) lt ) + m05 {w} bw with SUP.x≤sup S ? -- ? (subst (λ k → odef B k) (sym &iso) bw ) + ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl ?) -- (cong (&) eq) ) + ... | case2 lt = case2 ? -- ( subst (λ k → _ < k ) (sym *iso) lt ) m02 : MinSUP A B m02 = dont-or (m00 (& A)) m03 @@ -656,7 +646,7 @@ px = Oprev.oprev op 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 supf x) f b ∨ IsSUP A (UnionCF A f supf b) ab → + 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 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 @@ -693,7 +683,7 @@ ... | no lim = record { is-max = is-max } where 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 supf x) f b ∨ IsSUP A (UnionCF A f supf b) ab → + 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 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 @@ -746,7 +736,7 @@ SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B - SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt) } + SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; isSUP = record { ax = SUP.ax sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt) } } zc43 : (x sp1 : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x ) zc43 x sp1 with trio< x sp1 @@ -802,14 +792,14 @@ 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 ∧ ? → 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 - zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b + zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a ≤ b zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb )) - ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) - ... | case2 lt = <=-trans (zc05 fb) (case2 lt) + ... | case1 eq = subst (λ k → a ≤ k ) (subst₂ (λ j k → j ≡ k) &iso &iso ?) (zc05 fb) + ... | case2 lt = ≤-ftrans (zc05 fb) (case2 lt) zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (subst (λ k → odef A k ∧ ?) (sym &iso) ca ) ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) @@ -842,13 +832,8 @@ sup1 = minsupP pchainpx pcha ptotal sp1 = MinSUP.sup sup1 - sfpx<=sp1 : supf0 px <= sp1 - sfpx<=sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) - - sfpx≤sp1 : supf0 px o≤ sp1 - sfpx≤sp1 = subst ( λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc o≤-refl )) - ( MinSUP.minsup (ZChain.minsup zc o≤-refl) (MinSUP.asm sup1) - (λ {x} ux → MinSUP.x≤sup sup1 (case1 ux)) ) + sfpx≤sp1 : supf0 px ≤ sp1 + sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) -- -- supf0 px o≤ sp1 @@ -884,7 +869,7 @@ asupf1 {z} with trio< z px ... | tri< a ¬b ¬c = ZChain.asupf zc ... | tri≈ ¬a b ¬c = ZChain.asupf zc - ... | tri> ¬a ¬b c = MinSUP.asm sup1 + ... | tri> ¬a ¬b c = MinSUP.axm sup1 supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b supf1-mono {a} {b} a≤b with trio< b px @@ -897,7 +882,7 @@ 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 ) + zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.axm sup1) zc24 ) ... | tri≈ ¬a b ¬c = zc18 where zc21 : MinSUP A (UnionCF A f supf0 a) zc21 = ZChain.minsup zc (o≤-refl0 b) @@ -906,7 +891,7 @@ 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 ) + zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.axm sup1) zc24 ) ... | tri> ¬a ¬b c = o≤-refl sf≤ : { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z @@ -1003,7 +988,7 @@ ... | 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 ? z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc - ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ where -- u o< px → u o< b ? + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ -- 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 @@ -1045,14 +1030,14 @@ ... | 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 - m12 with osuc-≡< sfpx≤sp1 + m12 with osuc-≡< ? -- sfpx≤sp1 ... | case1 eq = eq ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) -- supf0 px o< sp1 , x o< sp1 m10 : f (supf0 px) ≡ supf0 px m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1) m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc) - ... | 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 ( 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 @@ -1070,7 +1055,7 @@ sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x sup {z} z≤x with trio< z px - ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m + ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.axm 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) @@ -1078,7 +1063,7 @@ ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 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 + ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.axm 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) @@ -1086,7 +1071,7 @@ ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 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 + ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.axm 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) @@ -1172,7 +1157,7 @@ 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} ⟪ az , cp ⟫ = ? where + zc11 {z} ⟪ az , cp ⟫ = ? record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field @@ -1194,7 +1179,7 @@ zc33 : supf0 z ≡ & (SUP.sup zc32) zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl ) zc36 : ¬ (supf0 px ≡ px) → STMP z≤x - zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x≤sup = zc34 ne } ; tsup=sup = zc33 } + zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.ax zc32 ; x≤sup = zc34 ne } ; tsup=sup = zc33 } zc35 : STMP z≤x zc35 with trio< (supf0 px) px ... | tri< a ¬b ¬c = zc36 ¬b @@ -1203,10 +1188,10 @@ 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 supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f supf0 b) f b ) → supf0 b ≡ b + b o≤ x → IsMinSUP A (UnionCF A f supf0 b) b ∧ (¬ 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 ⟫ + ... | 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 } , ? ⟫ ... | tri> ¬a ¬b px<b = ? where zc30 : x ≡ b zc30 with osuc-≡< b≤x @@ -1254,14 +1239,14 @@ uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 with trio< (IChain.i ia) (IChain.i ib) ... | tri< ia<ib ¬b ¬c with - <=-trans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (≤to<= (s≤fc _ f mf (IChain.fc ib))) + ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib)) ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * (& a) ≡ * (& b) ct00 = cong (*) eq1 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1) uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) uz01 | tri> ¬a ¬b ib<ia with - <=-trans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (≤to<= (s≤fc _ f mf (IChain.fc ia))) + ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia)) ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * (& a) ≡ * (& b) ct00 = sym (cong (*) eq1) @@ -1302,19 +1287,12 @@ zc11 : {z : Ordinal } → odef pchain z → odef pchainx z zc11 {z} lt = ? - sfpx<=spu : {z : Ordinal } → supf1 z <= spu - sfpx<=spu {z} with trio< z x + sfpx≤spu : {z : Ordinal } → supf1 z ≤ spu + sfpx≤spu {z} with trio< z x ... | tri< a ¬b ¬c = MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc (ob<x lim a)) ) refl ) ... | tri≈ ¬a b ¬c = case1 refl ... | tri> ¬a ¬b c = case1 refl - sfpx≤spu : {z : Ordinal } → supf1 z o≤ spu - sfpx≤spu {z} with trio< z x - ... | tri< a ¬b ¬c = subst ( λ k → k o≤ spu) ? - ( MinSUP.minsup (ZChain.minsup ? o≤-refl) ? (λ {x} ux → MinSUP.x≤sup ? ?) ) - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? - supf-mono : {x y : Ordinal } → x o≤ y → supf1 x o≤ supf1 y supf-mono {x} {y} x≤y with trio< y x ... | tri< a ¬b ¬c = ? @@ -1367,7 +1345,7 @@ ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ sup=u : {b : Ordinal} (ab : odef A 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 + b o≤ x → IsMinSUP A (UnionCF A f supf1 b) b ∧ (¬ 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 @@ -1396,9 +1374,9 @@ sp : Ordinal sp = MinSUP.sup sp1 asp : odef A sp - asp = MinSUP.asm sp1 + asp = MinSUP.axm 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 (ZChain.supf zc) b) ab + → HasPrev A chain f b ∨ IsSUP A (UnionCF A f (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 @@ -1411,7 +1389,7 @@ 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) asp + z19 : IsSUP A (UnionCF A f (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} zy with MinSUP.x≤sup sp1 @@ -1422,8 +1400,8 @@ z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 ) ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ - z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.asm sp1 )) - ... | case1 eq = ⊥-elim (¬b (sym eq) ) + z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.axm sp1 )) + ... | case1 eq = ⊥-elim (¬b (sym (cong (*) eq ) )) ... | case2 lt = ⊥-elim (¬c lt ) ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b ) ... | tri> ¬a ¬b c = ⊥-elim z17 where @@ -1453,10 +1431,10 @@ z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} - (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm msp1 )))) - (subst (λ k → odef A k) (sym &iso) (MinSUP.asm msp1) ) + (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.axm msp1 )))) + (subst (λ k → odef A k) (sym &iso) (MinSUP.axm msp1) ) (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1 ))) -- x ≡ f x ̄ - (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where -- x < f x + (proj1 (cf-is-<-monotonic nmx c (MinSUP.axm msp1 ))) where -- x < f x supf = ZChain.supf zc msp1 : MinSUP A (ZChain.chain zc)