Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 909:fec6064b44be
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 12 Oct 2022 01:46:29 +0900 |
| parents | d917831fb607 |
| children | f28f119bfa6f |
| files | src/zorn.agda |
| diffstat | 1 files changed, 10 insertions(+), 32 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Oct 11 22:47:13 2022 +0900 +++ b/src/zorn.agda Wed Oct 12 01:46:29 2022 +0900 @@ -456,22 +456,6 @@ -- ordering is not proved here but in ZChain1 - supf-¬hp : {x : Ordinal } → x o≤ z → odef (UnionCF A f mf ay supf x) (supf x) - → ( supf x ≡ f (supf x) ) ∨ ( ¬ HasPrev A chain (supf x) f ) - supf-¬hp {x} x≤z usx with proj1 ( mf (supf x) asupf ) - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) eq)) - ... | case2 s<fs = case2 sh00 where - sh00 : ( ¬ HasPrev A chain (supf x) f ) - sh00 hp = <-irr (<=to≤ sh01) s<fs where - sh01 : ( f ( supf x ) ≡ supf x ) ∨ ( f ( supf x ) << supf x ) - sh01 = subst (λ k → ( f ( supf x ) ≡ k ) ∨ ( f ( supf x ) << k )) (sym (supf-is-minsup x≤z)) - ( MinSUP.x<sup ( minsup x≤z ) (f-next usx )) - - supf-idem : {x : Ordinal } → supf x o< z → supf (supf x) ≡ supf x - supf-idem {x} sf<z with csupf sf<z - ... | ⟪ au , ch-init fc ⟫ = ? - ... | ⟪ au , ch-is-sup u u<z is-sup fc ⟫ = ? - record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc @@ -1093,6 +1077,8 @@ -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x + cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px) + cs01 spx<px = ZChain.csupf zc spx<px cs00 : supf1 (supf1 px) ≡ supf1 px cs00 = ? csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) @@ -1103,28 +1089,20 @@ -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px supu=u : supf1 (supf1 z1) ≡ supf1 z1 supu=u = ? -- ZChain.sup=u zc ? ? ? - ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) - ... | ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫ - ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , - ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) - record { fcy<sup = ? ; order = ? ; supu=u = ? } (fcpu fc (o<→≤ u<x)) ⟫ where - supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = ? -- ZChain.sup=u zc ? ? ? - csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) - record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where - -- supf1 z1 ≡ supf0 z1, z1 ≡ px - supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = ? + ... | case2 lt = zc12 (case1 cs03) where + cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) + cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) + csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where - -- supf1 z1 ≡ sp1, px o< z1 + -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x asm : odef A (supf1 z1) asm = subst (λ k → odef A k ) (sym (sf1=sp1 c)) ( MinSUP.asm sup1) sp1=px : sp1 ≡ px sp1=px with trio< sp1 px - ... | tri> ¬a ¬b c = ? - ... | tri≈ ¬a b ¬c = b - ... | tri< a ¬b ¬c = ? + ... | tri< a ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) supu=u : supf1 (supf1 z1) ≡ supf1 z1 supu=u = ?