Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 896:1f3a93bb4229
fixing u<x is no good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Oct 2022 17:39:31 +0900 |
| parents | aa496c232604 |
| children | f52c610cca06 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 15 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Oct 06 16:43:09 2022 +0900 +++ b/src/zorn.agda Thu Oct 06 17:39:31 2022 +0900 @@ -458,7 +458,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 ) → supf b o< supf z → (ab : odef A b) + is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< 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 @@ -598,7 +598,7 @@ → 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 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → - ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → + ZChain.supf zc b o< 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 @@ -648,22 +648,24 @@ 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 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → - supf b o< supf x → (ab : odef A b) → + supf b o< 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 + = ⟪ 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 + sb<sx : supf b o< supf x + 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) + chain-mono1 ? (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) (chain-mono1 (o<→≤ b<x) uz) } , m04 ⟫ + ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? uz) } , m04 ⟫ m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -673,14 +675,14 @@ 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 → - supf b o< supf x → (ab : odef A b) → + supf b o< 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 ) ... | 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 ? 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)) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b @@ -690,12 +692,11 @@ m08 {s} {z1} s<b fc = order m09 s<b fc 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) + chain-mono1 ? (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) (chain-mono1 (o<→≤ b<x) lt )} - , m04 ⟫ -- ZChain on x + ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? lt )} , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } @@ -709,18 +710,12 @@ supf = ZChain.supf zc sp1 : SUP A chain sp1 = sp0 f mf as0 zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< & 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 : supf (& (SUP.sup sp1)) o< supf (& A) - z21 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (c<→o< ( SUP.as sp1))) ) - ... | case2 lt = lt - ... | case1 eq = ? where - z24 : supf (& (SUP.sup sp1)) ≡ & (SUP.sup sp1) - z24 = ZChain.sup=u zc ? ? ? - z25 : supf (& A) ≡ MinSUP.sup ( ZChain.minsup zc o≤-refl ) - z25 = ZChain.supf-is-minsup zc o≤-refl + 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)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )