Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 897:f52c610cca06
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Oct 2022 18:44:18 +0900 |
| parents | 1f3a93bb4229 |
| children | 37ddab37e189 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 21 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Oct 06 17:39:31 2022 +0900 +++ b/src/zorn.agda Thu Oct 06 18:44:18 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< z → (ab : odef A b) + 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) 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< x → (ab : odef A b) → + 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,7 +648,7 @@ 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< x → (ab : odef A b) → + 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 @@ -657,8 +657,6 @@ = ⟪ 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 ? (HasPrev.ay nhp) @@ -673,9 +671,21 @@ m09 {s} {z} s<b fcz = order b<A s<b fcz m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } + sb<sx : supf b o< supf x + sb<sx with osuc-≡< ( ZChain.supf-mono zc (o<→≤ b<x ) ) + ... | case2 lt = lt + ... | case1 eq = ⊥-elim ( <-irr (case1 (sym m11)) m12 ) where + --- supf b ≡ supf x * ( supf x ) ≤ * a < * b , * (supf x) ≡ * (supf b) ≡ * b + m10 : {a : Ordinal} → odef (UnionCF A f mf ay supf x) a → * ( supf x ) ≤ * a + m10 {a} ⟪ ua , ch-init fc ⟫ = ? + m10 {a} ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ? + m12 : * ( supf x ) < * b + m12 = ? + m11 : * ( supf x ) ≡ * b + m11 = ? ... | 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< x → (ab : odef A b) → + 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 @@ -710,12 +720,14 @@ 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< & A → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → 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< & A - z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) + z21 : & (SUP.sup sp1) o< & A + z21 = c<→o< (SUP.as sp1 ) + -- 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 )