Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1247:0350fe03d73a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Mar 2023 14:41:39 +0900
parents dd3debafba2d
children b1d024385208
files src/generic-filter.agda
diffstat 1 files changed, 6 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Tue Mar 14 13:17:31 2023 +0900
+++ b/src/generic-filter.agda	Tue Mar 14 14:41:39 2023 +0900
@@ -72,6 +72,11 @@
 
 open CountableModel
 
+abs-minus : {p q : HOD} → (C : CountableModel) → ctl-M C ∋ (p ＼ q) 
+abs-minus {p} {q} C = ? where
+    p-q : {x : Ordinal } → odef (p ＼ q) x →  ℕ
+    p-q pqx = ctl← C _ ?
+
 ----
 --   a(n) ∈ M
 --   ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ p(n) ⊆ q
@@ -365,7 +370,7 @@
     D : HOD  
     D = L ＼ gf
     M∋D : M ∋ D
-    M∋D = ?
+    M∋D = subst (λ k → odef M k) ? (ctl<M C ?) 
     D⊆PP : D ⊆ Power P
     D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
     DD : Dense {L} {P} LPP