# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678772499 -32400
# Node ID 0350fe03d73a9ff140de570abc4c986a22023303
# Parent  dd3debafba2d24bfa61dac962788008c6d33626b
...

diff -r dd3debafba2d -r 0350fe03d73a src/generic-filter.agda
--- 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