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

changeset 1249:c57b8068f97c

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 Wed, 15 Mar 2023 12:59:55 +0900
parents b1d024385208
children 6c467705e6e4
files src/generic-filter.agda
diffstat 1 files changed, 13 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Wed Mar 15 09:41:57 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 15 12:59:55 2023 +0900
@@ -62,7 +62,7 @@
        ctl← : (x : Ordinal )→  odef (ctl-M ) x → ℕ
        ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x )  → ctl→ (ctl← x lt ) ≡ x
        TC : {x y : Ordinal} → odef ctl-M x → odef (* x) y → odef ctl-M y
-       is-model : (x : HOD) → ctl-M ∋ (x ∩ ctl-M)
+       is-model : (x : HOD) → & x o< & ctl-M → ctl-M ∋ (x ∩ ctl-M)
        -- we have no otherway round
        -- ctl-iso← : { x : ℕ }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
 --
@@ -373,24 +373,27 @@
       → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
       → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
       → (C : CountableModel ) 
+      → ctl-M C ∋ L
       → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
       →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C ))
-lemma232 P L p0 LPP Lp0 CAP UNI NEG C NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj2 rgf∩D) (proj1 rgf∩D)) 
+lemma232 P L p0 LPP Lp0 CAP UNI NEG C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj2 rgf∩D) (proj1 rgf∩D)) 
         ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
-    GF =  genf ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C )
-    rgf =  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C )
+    PG = P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C 
+    GF =  genf PG
+    rgf =  rgen PG
     M = ctl-M C
     D : HOD  
     D = L ＼ rgf
     M∋DM : M ∋ (D ∩ M )
-    M∋DM = is-model C D
+    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 ⊆ rgf ) ∧ (r ⊆ rgf )
-    ll01 {q} {r} rgfpq = ⟪ ll02 , ? ⟫  where
-        ll02 : {x : Ordinal } → odef q x → odef rgf x
-        ll02 {x} qx = record { z = ? ; az = record { z = ? ; az = ? ; x=ψz = ? }  ; x=ψz = ? }
-        -- filter2 GF ? ? ?
+    -- 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