Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 380:0a116938a564
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Jul 2020 02:39:09 +0900 |
| parents | 7b6592f0851a |
| children | d2cb5278e46d |
| files | filter.agda |
| diffstat | 1 files changed, 5 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/filter.agda Tue Jul 21 02:19:07 2020 +0900 +++ b/filter.agda Tue Jul 21 02:39:09 2020 +0900 @@ -219,11 +219,15 @@ find (j0 ∷ _) 0 v0 = i0 find (j1 ∷ _) 0 v1 = i1 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p + lemma : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p) + lemma j0 n {x} {p} = refl + lemma j1 n {x} {p} = refl + lemma j2 n {x} {p} = refl feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q feq n {0} {v0} {v0} = refl feq n {0} {v1} {v1} = refl feq [] {Suc x} {()} - feq (_ ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) {!!} {!!} (feq n {x} {p} {q}) + feq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (lemma h n) (lemma h n) (feq n {x} {p} {q}) record _f⊆_ (f g : PFunc) : Set (suc n) where field