Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1253:507f443c97ce
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 15 Mar 2023 22:45:05 +0900 (2023-03-15) |
parents | c99c37121d47 |
children | abd86d493c61 |
files | src/generic-filter.agda |
diffstat | 1 files changed, 1 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/generic-filter.agda Wed Mar 15 22:26:00 2023 +0900 +++ b/src/generic-filter.agda Wed Mar 15 22:45:05 2023 +0900 @@ -451,18 +451,10 @@ M∋DM = is-model C D ? D⊆PP : D ⊆ Power P D⊆PP {x} ⟪ Lx , ngx ⟫ = LPP Lx - -- ll01 : {q r : HOD } → (rgf ∋ q) ∧ (rgf ∋ r) → (q ⊆ (q ∪ r) ) ∧ (r ⊆ (q ∪ r) ) - -- ll01 {q} {r} rgfpq with gfilter2 PG rgfpq - -- ... | record { z = z₁ ; az = record { z = z ; az = az ; x=ψz = x=ψz₁ } ; x=ψz = x=ψz } = ? - -- ll02 : {x : Ordinal } → odef q x → odef rgf x - -- ll02 {x} qx = record { z = ? ; az = record { z = ? ; az = ? ; x=ψz = ? } ; x=ψz = ? } - -- -- filter2 GF ? ? ? - -- with contra-position ? ? - -- ... | t = ? DD : Dense {L} {P} LPP Dense.dense DD = D Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx - Dense.dense-f DD Lp = ? where + Dense.dense-f DD Lp = ll00 where ll00 : HOD ll00 with NotCompatible.¬compat (NC Lp) ... | nc = ?