Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 463:433866b43992
generic filter done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 20 Mar 2022 17:03:08 +0900 |
| parents | 667c54e6fa1f |
| children | 5acf6483a9e3 |
| files | src/generic-filter.agda |
| diffstat | 1 files changed, 17 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/generic-filter.agda Sun Mar 20 16:29:03 2022 +0900 +++ b/src/generic-filter.agda Sun Mar 20 17:03:08 2022 +0900 @@ -194,13 +194,22 @@ fd09 Zero = Lp0 fd09 (Suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) ) ... | yes _ = fd09 i - ... | no _ = {!!} + ... | no not = fd17 where + fd19 = ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)) + fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19 + fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)) + fd17 : odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) ) + fd17 = proj1 fd18 an : Nat an = ctl← C (& (dense D)) MD pn : Ordinal pn = find-p L C an (& p0) pn+1 : Ordinal pn+1 = find-p L C (Suc an) (& p0) + fd26 : dense D ≡ * (ctl→ C an) + fd26 = begin dense D ≡⟨ sym *iso ⟩ + * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→ C MD )) ⟩ + * (ctl→ C an) ∎ where open ≡-Reasoning fd07 : odef (dense D) pn+1 fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) ) ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 ⟪ fd13 , ⟪ fd14 , fd15 ⟫ ⟫ ) ) where @@ -211,18 +220,19 @@ fd13 : L ∋ ( dense-f D fd12 ) fd13 = incl (d⊆P D) ( dense-d D fd12 ) fd14 : (* (ctl→ C an)) ∋ ( dense-f D fd12 ) - fd14 = subst (λ k → odef k (& ( dense-f D fd12 ) )) fd16 ( dense-d D fd12 ) where - fd16 : dense D ≡ * (ctl→ C an) - fd16 = begin dense D ≡⟨ sym *iso ⟩ - * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→ C MD )) ⟩ - * (ctl→ C an) ∎ where open ≡-Reasoning + fd14 = subst (λ k → odef k (& ( dense-f D fd12 ) )) fd26 ( dense-d D fd12 ) fd15 : (y : Ordinal) → odef (* (& (dense-f D fd12))) y → odef (* (find-p L C an (& p0))) y fd15 y lt = subst (λ k → odef (* (find-p L C an (& p0))) k ) &iso ( incl (dense-p D fd12 ) fd16 ) where fd16 : odef (dense-f D fd12) (& ( * y)) fd16 = subst₂ (λ j k → odef j k ) (*iso) (sym &iso) lt fd10 : PGHOD an L C (find-p L C an (& p0)) =h= od∅ fd10 = ≡o∅→=od∅ y - ... | no _ = {!!} + ... | no not = fd27 where + fd29 = ODC.minimal O ( PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq)) + fd28 : PGHOD an L C (find-p L C an (& p0)) ∋ fd29 + fd28 = ODC.x∋minimal O (PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq)) + fd27 : odef (dense D) (& fd29) + fd27 = subst (λ k → odef k (& fd29)) (sym fd26) (proj1 (proj2 fd28)) fd03 : odef (PDHOD L p0 C) pn+1 fd03 = record { gr = Suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (Suc an)} fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1)