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

changeset 1258:04fc80af6f77

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 Fri, 17 Mar 2023 00:33:43 +0900
parents 004d8794697f
children 4993a95d3fc8
files src/generic-filter.agda
diffstat 1 files changed, 1 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Fri Mar 17 00:30:43 2023 +0900
+++ b/src/generic-filter.agda	Fri Mar 17 00:33:43 2023 +0900
@@ -130,23 +130,6 @@
 gf05 {a} {b} {x} (case1 ax) nax nbx = nax ax
 gf05 {a} {b} {x} (case2 bx) nax nbx = nbx bx
 
-gf02 : {P a b : HOD } → (P ＼ a) ∩ (P ＼ b) ≡ ( P ＼ (a ∪ b) )
-gf02 {P} {a} {b} = ==→o≡  record { eq→ = gf03 ; eq← = gf04 } where
-       gf03 : {x : Ordinal} → odef ((P ＼ a) ∩ (P ＼ b)) x → odef (P ＼ (a ∪ b)) x
-       gf03 {x} ⟪ ⟪ Px , ¬ax ⟫ , ⟪ _ , ¬bx ⟫ ⟫ = ⟪ Px , (λ pab → gf05 {a} {b} {x} pab ¬ax ¬bx )   ⟫
-       gf04 : {x : Ordinal} → odef (P ＼ (a ∪ b)) x → odef ((P ＼ a) ∩ (P ＼ b)) x
-       gf04 {x} ⟪ Px , abx ⟫  = ⟪ ⟪ Px , (λ ax → abx (case1 ax) ) ⟫ , ⟪ Px  , (λ bx → abx (case2 bx) ) ⟫ ⟫
-
-gf45 : {P a b : HOD } → (P ＼ a) ∪ (P ＼ b) ≡ ( P ＼ (a ∩ b) )
-gf45 {P} {a} {b} = ==→o≡  record { eq→ = gf03 ; eq← = gf04 } where
-       gf03 : {x : Ordinal} → odef ((P ＼ a) ∪ (P ＼ b)) x → odef (P ＼ (a ∩ b)) x
-       gf03 {x} (case1 pa) = ⟪ proj1 pa , (λ ab → proj2 pa (proj1 ab) ) ⟫ 
-       gf03 {x} (case2 pb) = ⟪ proj1 pb , (λ ab → proj2 pb (proj2 ab) ) ⟫ 
-       gf04 : {x : Ordinal} → odef (P ＼ (a ∩ b)) x → odef ((P ＼ a) ∪ (P ＼ b)) x
-       gf04 {x} ⟪ Px , nab ⟫ with ODC.p∨¬p O (odef b x)
-       ... | case1 bx = case1 ⟪ Px , ( λ ax → nab ⟪ ax , bx ⟫ ) ⟫
-       ... | case2 nbx = case2 ⟪ Px , ( λ bx → nbx bx ) ⟫
-
 open import Data.Nat.Properties
 open import nat
 
@@ -187,7 +170,7 @@
 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
       → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
 P-GenericFilter P L p0 L⊆PP Lp0 C = record {
-      genf = record { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; ideal2 =  ? }
+      genf = record { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; ideal2 =  ideal2 }
     ; generic = fdense
    } where
        ideal1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → q ⊆ p → PDHOD L p0 C ∋ q