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

changeset 1128:7d4966f2f74d

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, 10 Jan 2023 17:16:16 +0900
parents c4f4868a8cdd
children 5053fd12134a
files src/filter.agda
diffstat 1 files changed, 22 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Tue Jan 10 09:29:58 2023 +0900
+++ b/src/filter.agda	Tue Jan 10 17:16:16 2023 +0900
@@ -267,21 +267,33 @@
               mu24 = subst (λ k → & (r ∩ q) ≡ k ) (cong (&) mu26) (cong (&) (==→o≡ mu25) ) 
               mu20 : F ∋ (r ∩ q)
               mu20 = case1 record { y = & ( * ry ∩ * qy ) ; mfy = mu23 ; x=y∪p = mu24 }
-         mu02 {r} {q} (case1 record { y = ry ; mfy = mfry ; x=y∪p = x=ry∪p }) (case2 mfq) Lrq = 
-           case1 record { y = & ( * ry ∩ q ) ; mfy = mu23 ; x=y∪p = cong (&) (==→o≡ mu25) } where
+         mu02 {r} {q} (case1 record { y = ry ; mfy = mfry ; x=y∪p = x=ry∪p }) (case2 mfq) Lrq = case2 mu24 where
               mu21 : r ≡ * ry ∪ p
               mu21 = subst₂ (λ j k → j ≡ k ) *iso (trans *iso (cong (λ k → (* ry ∪ k)) *iso)) (cong (*) x=ry∪p )
               mu23 : odef (filter mf) (& (* ry ∩ q))
               mu23 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfry) mfq
                 (CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) (f⊆L mf mfq) )
-              mu25 : od (r ∩ q) == od (* (& (* ry ∩ q)) ∪ * (& p))
-              mu25 = subst (λ k → od (k ∩ q)== od (* (& (* ry ∩ q)) ∪ * (& p))) (sym mu21) record { eq→ = mu27 ; eq← = mu28 } where
-                  mu27 : {x : Ordinal} → odef (* ry ∪ p) x ∧ odef q x → odef (* (& (* ry ∩ q))) x ∨ odef (* (& p)) x
-                  mu27 {x} ⟪ case1 ryx , qx ⟫ = case1 (subst (λ k → odef k x) (sym *iso) ⟪ ryx , qx ⟫ )
-                  mu27 {x} ⟪ case2 px , qx ⟫ = case2 (subst (λ k → odef k x) (sym *iso) px )
-                  mu28 : {x : Ordinal} → odef (* (& (* ry ∩ q))) x ∨ odef (* (& p)) x → odef (* ry ∪ p) x ∧ odef q x
-                  mu28 {x} (case1 ryq) = ?
-                  mu28 {x} (case2 px) = ⟪  case2 (subst (λ k → odef k x) *iso px ) , ? ⟫
+              mu26 : (p ∩ q) =h= od∅
+              mu26 = record { eq→ = λ lt → ⊥-elim ( mu29 lt)  ; eq← = λ lt → ⊥-elim ( ¬x<0 lt  ) } where
+                  q-p : HOD
+                  q-p = q ＼ p
+                  [q-p]⊆q : ?
+                  [q-p]⊆q = ?
+                  mu30 : odef (filter mf ) (& ( q ∩ ( q ＼ p )))
+                  mu30 = filter2 mf ? ? ?
+                  mu31 : odef (filter mf ) (& p )
+                  mu31 = filter1 mf ? ? ?
+                  mu29 : {x : Ordinal} → ¬ ( odef (p ∩ q) x )
+                  mu29 {x} pqx = ?
+              mu25 : od (r ∩ q) == od (* (& (* ry ∩ q)))
+              mu25 = subst (λ k → od (k ∩ q)== od (* (& (* ry ∩ q)) )) (sym mu21) record { eq→ = mu27 ; eq← = mu28 } where
+                  mu27 : {x : Ordinal} → odef (* ry ∪ p) x ∧ odef q x → odef (* (& (* ry ∩ q))) x 
+                  mu27 {x} ⟪ case1 ryx , qx ⟫ = subst (λ k → odef k x) (sym *iso) ⟪ ryx , qx ⟫ 
+                  mu27 {x} ⟪ case2 px , qx ⟫ = ?
+                  mu28 : {x : Ordinal} → odef (* (& (* ry ∩ q))) x → odef (* ry ∪ p) x ∧ odef q x
+                  mu28 {x} ryq = ?
+              mu24 :   odef (filter mf) (& (r ∩ q))
+              mu24 = ?                             
          mu02 {r} {q} (case2 mfr) (case1 record { y = y ; mfy = mfp ; x=y∪p = x=y∪p }) Lrq = ?
          mu02 {r} {q} (case2 mfr) (case2 mfq ) Lrq = case2 (filter2 mf mfr mfq Lrq )
          FisFilter : Filter {L} {P} LP