Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 919:213f12f27003
supf u o< supf x
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 16 Oct 2022 10:09:54 +0900 |
| parents | 4c33f8383d7d |
| children | a2f8d14012aa |
| files | src/zorn.agda |
| diffstat | 1 files changed, 54 insertions(+), 45 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Oct 15 20:05:34 2022 +0900 +++ b/src/zorn.agda Sun Oct 16 10:09:54 2022 +0900 @@ -262,7 +262,7 @@ 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 ) + ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : supf u o< supf 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 -- @@ -386,12 +386,12 @@ chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) - {a b c : Ordinal} → a o≤ b + (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 {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = +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 {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 ⟫ +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 (supf-mono a≤b ) ) is-sup fc ⟫ 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 @@ -460,7 +460,7 @@ {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) + is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsSup A (UnionCF A f mf ay supf z) ab → * a < * b → odef ((UnionCF A f mf ay supf z)) b @@ -589,9 +589,9 @@ SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x 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 - chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b + 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 → - b o< x → (ab : odef A b) → + ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev @@ -612,7 +612,7 @@ zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s zc07 = fc zc06 : supf u ≡ u @@ -638,18 +638,20 @@ zc1 x prev with Oprev-p x -- prev is not used now.... ... | yes op = record { is-max = is-max } where px = Oprev.oprev op - zc-b<x : {b : Ordinal } → b o< x → b o< osuc px - zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt + zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px + zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt ) is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → - b o< x → (ab : odef A b) → + ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → * a < * b → odef (UnionCF A f mf 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 b<x ab has-prev a<b - is-max {a} {b} ua b<x ab P a<b | case2 is-sup - = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup + = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab + b<x : b o< x + b<x = ZChain.supf-inject zc sb<sx m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f 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 } ) @@ -665,16 +667,18 @@ m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } ... | no lim = record { is-max = is-max } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → - b o< x → (ab : odef A b) → + ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → * a < * b → odef (UnionCF A f mf 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 b<x 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 sb<sx ab P a<b with ODC.or-exclude O P + is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua sb<sx ab has-prev a<b + is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) ... | 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 )) ⟫ - ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) + b<x : b o< x + b<x = ZChain.supf-inject zc sb<sx m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -700,12 +704,12 @@ supf = ZChain.supf zc sp1 : SUP A chain sp1 = sp0 f mf as0 zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) → HasPrev A chain b f ∨ IsSup A chain {b} ab → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) - z21 : & (SUP.sup sp1) o< & A - z21 = c<→o< (SUP.as sp1 ) + z21 : supf (& (SUP.sup sp1)) o< supf (& A) + z21 = ? -- z21 : supf (& (SUP.sup sp1)) o< & A -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) z12 : odef chain (& (SUP.sup sp1)) @@ -907,7 +911,7 @@ zc21 : MinSUP A (UnionCF A f mf ay 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₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a<px) ux ) ) + 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 @@ -916,7 +920,7 @@ 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₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux ) ) + 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 ) ... | tri> ¬a ¬b c = o≤-refl @@ -928,14 +932,16 @@ fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc 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 + zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where + u<x : u o< x + u<x = ? zc21 : {z1 : Ordinal } → FClosure A f (supf1 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< u px | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17 + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) @@ -951,26 +957,28 @@ ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where + zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where + u<x : u o< x + u<x = ? zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u - (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) - record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 (o<→≤ u<x)) (ChainP.supu=u is-sup) } zc14 ⟫ where + ? + record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) } zc14 ⟫ where zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<x)) ss<spx) (fcup fc s≤px) ) where + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ ?))) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ ?)) ss<spx) (fcup fc s≤px) ) where s≤px : s o≤ px - s≤px = ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x) + s≤px = ? -- ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x) zc14 : FClosure A f (supf1 u) (supf0 u) - zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 (o<→≤ u<x))) asp) (sf1=sf0 (o<→≤ u<x)) + zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (pxo<x op) record { fcy<sup = zc13 + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) @@ -989,14 +997,14 @@ zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) s≤px : s o≤ px s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , o<→≤ u<x ⟫ ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ? ⟫ ) zc12 {z} (case2 fc) = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) - ... | case1 sfpx=px = ⟪ asp , ch-is-sup px (pxo<x op) + ... | case1 sfpx=px = ⟪ asp , ch-is-sup px ? -- (pxo<x op) record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) @@ -1022,22 +1030,22 @@ ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) - record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ? + record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫ where z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc) + z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc) z11 : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1 → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u ) - z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) + z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.order is-sup lt0 (fcup fc s≤px )) where s<u : s o< u s<u = supf-inject0 supf1-mono lt s≤px : s o≤ px - s≤px = ordtrans s<u (o<→≤ u≤x) + s≤px = ordtrans s<u ? -- (o<→≤ u≤x) lt0 : supf0 s o< supf0 u - lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u≤x)) lt + lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt z12 : supf1 u ≡ u - z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup) + z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) @@ -1103,7 +1111,8 @@ cs06 : supf0 px o< osuc px cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) + csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? + -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) zc4 : ZChain A f mf ay x --- x o≤ supf px