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

changeset 435:b18ca68d115a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fi;ter1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Feb 2022 22:39:17 +0900
parents 5f22af3562b7
children 87b5303ceeb5
files src/generic-filter.agda
diffstat 1 files changed, 23 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Fri Feb 18 11:44:08 2022 +0900
+++ b/src/generic-filter.agda	Sun Feb 20 22:39:17 2022 +0900
@@ -148,7 +148,29 @@
         f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
              find-p-⊆P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
         f1 : {p q : HOD} → q ⊆ P → PDHOD C P ∋ p → p ⊆ q → PDHOD C P ∋ q
-        f1 {p} {q}  q⊆P PD∋p p⊆q = {!!}
+        f1 {p} {q}  q⊆P PD∋p p⊆q = f01 (& p) (& q) (⊆→o≤ f02) PD∋p (⊆→o≤ f03) where
+           f02 : {x : Ordinal} → odef q x → odef P x
+           f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) )
+           f03 : {x : Ordinal} → odef p x → odef q x
+           f03 {x} lt = subst (λ k → def (od q) k) &iso (incl p⊆q (subst (λ k → def (od p) k) (sym &iso) lt) )
+           f04 : (ip : Ordinal) → PDN C P ip → (x : Ordinal) → ((y : Ordinal) → y o< x → ip o< osuc y → PDN C P y) → ip o< osuc x → PDN C P x
+           f04 ip PD x prev lt with trio< ip (osuc x)
+           ... | tri≈ ¬a b ¬c = {!!}
+           ... | tri> ¬a ¬b c = ⊥-elim ( o<> c lt )
+           ... | tri< a ¬b ¬c with osuc-≡< a
+           ... | case1 ip=x = {!!}
+           ... | case2 ip<x = record { gr = ctl← C (find-p C P (PDN.gr PD) ( next-p x (λ p → PGHOD (PDN.gr PD) C P (& p)))) f05
+               ;  pn<gr = f07 ; x∈PP = f06 } where
+               next1 : Ordinal
+               next1 = find-p C P (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) C P (& p₁))) 
+               f05 : next1 o< ctl-M C
+               f05 = {!!}
+               f06 : odef (Power P) x
+               f06 = {!!}
+               f07 :  (y : Ordinal) → odef (* x) y → odef (* (find-p C P (ctl← C next1 f05) o∅)) y
+               f07 = {!!}
+           f01 : (ip iq : Ordinal) → iq o< osuc (& P) → PDN C P ip → ip o< osuc iq → PDN C P iq
+           f01 ip iq q<P PD = TransFinite0 {λ x → ip o< osuc x → PDN C P x } (f04 ip PD ) iq
         f2 : {p q : HOD} → PDHOD C P ∋ p → PDHOD C P ∋ q → PDHOD C P ∋ (p ∩ q)
         f2 {p} {q} PD∋p PD∋q = {!!}