Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 916:f0b98f57ec65
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 13 Oct 2022 17:47:19 +0900 |
| parents | 8695050933a7 |
| children | 4d99a1306f40 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 31 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 12 20:49:21 2022 +0900 +++ b/src/zorn.agda Thu Oct 13 17:47:19 2022 +0900 @@ -456,14 +456,6 @@ -- ordering is not proved here but in ZChain1 - csupf< : {a b : Ordinal } → a o≤ b → odef (UnionCF A f mf ay supf z) (supf b) → odef (UnionCF A f mf ay supf z) (supf a) - csupf< {a} {b} a≤b ⟪ as , ch-init fc ⟫ = ⟪ ? , ch-init ? ⟫ - csupf< {a} {b} a≤b ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? , ch-is-sup (supf a) uz01 ? ? ⟫ where - a≤u : ? - a≤u = ? - uz01 : supf a o< z - uz01 = ordtrans≤-< (subst (λ k → supf a o< k) (cong osuc (ChainP.supu=u is-sup)) (supf-mono a≤u )) u<x - 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 @@ -1103,24 +1095,38 @@ supf1 px ≡⟨ sym sfz=sfpx ⟩ supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ supf0 z1 ∎ where open ≡-Reasoning - ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px + ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where + --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x + cs05 : px o< supf0 px + cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx + cs06 : supf0 px o< osuc px + cs06 = subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) 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 } with trio< sp1 px - ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px, sp1 o< z1 - ... | tri≈ ¬a sp1=px ¬c = ⟪ 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, sp1 o< x -- sp1 o< z1 - -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1 - asm : odef A (supf1 z1) - asm = subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) - cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) - cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl ) ⟩ - supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩ - supf1 sp1 ∎ ))) where open ≡-Reasoning - supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = ? - ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) + csupf2 | tri> ¬a ¬b px<z1 | 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 + supu=u : supf1 (supf1 z1) ≡ supf1 z1 + supu=u = ? + sp1≤px : sp1 o≤ px + sp1≤px with trio< sp1 px + ... | tri< a ¬b ¬c = o<→≤ a + ... | tri≈ ¬a b ¬c = o≤-refl0 b + ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) + + -- with trio< sp1 px + -- ... | tri< sp1<px ¬b ¬c = ? -- supf1 z1 = sp1 o< px o< z1 + -- ... | tri≈ ¬a sp1=px ¬c = ⟪ 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, sp1 o< x -- sp1 o< z1 + -- -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1 + -- asm : odef A (supf1 z1) + -- asm = subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) + -- cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) + -- cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin + -- supf0 px ≡⟨ sym (sf1=sf0 o≤-refl ) ⟩ + -- supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩ + -- supf1 sp1 ∎ ))) where open ≡-Reasoning + --... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px)