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

changeset 452:76aba34438f2

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 Mon, 14 Mar 2022 23:37:18 +0900
parents 31f0a5a745a5
children e5f0ac638c01
files src/generic-filter.agda
diffstat 1 files changed, 10 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Mon Mar 14 19:53:54 2022 +0900
+++ b/src/generic-filter.agda	Mon Mar 14 23:37:18 2022 +0900
@@ -226,11 +226,17 @@
     ... | case1 q = Incompatible.q (I x PP∋x)
     ... | case2 r = Incompatible.r (I x PP∋x)
     df¬⊆ : {x : HOD} → (lt : x ⊆ P) → ¬ ( df lt  ⊆ x )
-    df¬⊆ {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x
-    ... | case1 q = {!!}
-    ... | case2 r = {!!}
+    df¬⊆ {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x
+    ... | case1 q = q
+    ... | case2 r = r
+    df¬⊆P : {x : HOD} → (lt : x ⊆ P) → df lt  ⊆ P 
+    df¬⊆P {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x
+    ... | case1 q = Incompatible.PP∋q (I x PP∋x)
+    ... | case2 r = Incompatible.PP∋r (I x PP∋x)
+    ¬G∋df : {x : HOD} → (lt : x ⊆ P) → ¬ G ∋ (df lt ) 
+    ¬G∋df {x} lt g = {!!}
     df-d : {x : HOD} → (lt : x ⊆ P) → D ∋ df lt
-    df-d {x} lt = {!!}
+    df-d {x} lt = ⟪  power← P _ (incl (df¬⊆P lt)) , ¬G∋df lt ⟫
     df-p : {x : HOD} → (lt : x ⊆ P) → x ⊆ df lt
     df-p {x} lt with Incompatible.incompatible (I x lt) x lt
     ... | case1 q = Incompatible.p⊆q (I x lt)