---

Step * 1 1 of Lemma fpf-union-join-member


1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. f : a:A fp-> B[a] List@i
5. g : a:A fp-> B[a] List@i
6. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
7. a : A@i
8. ↑a ∈ dom(fpf-union-join(eq;R;f;g))
9. x : B[a]@i
10. R ∈ (B[a] List) ─→ B[a] ─→ 𝔹
11. ↑a ∈ dom(f)
12. ↑a ∈ dom(g)
13. (x ∈ f(a) @ filter(R f(a);g(a)))@i
⊢ (True ∧ (x ∈ f(a))) ∨ (True ∧ (x ∈ g(a)))
BY
{ ((RWO "member_append" (-1) THENM RWO "member_filter" (-1)) THENA Auto) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. f : a:A fp-> B[a] List@i
5. g : a:A fp-> B[a] List@i
6. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
7. a : A@i
8. ↑a ∈ dom(fpf-union-join(eq;R;f;g))
9. x : B[a]@i
10. R ∈ (B[a] List) ─→ B[a] ─→ 𝔹
11. ↑a ∈ dom(f)
12. ↑a ∈ dom(g)
13. (x ∈ f(a)) ∨ ((x ∈ g(a)) ∧ (↑(R f(a) x)))
⊢ (True ∧ (x ∈ f(a))) ∨ (True ∧ (x ∈ g(a)))

---

Latex:



1.  [A]  :  Type
2.  eq  :  EqDecider(A)@i
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  f  :  a:A  fp->  B[a]  List@i
5.  g  :  a:A  fp->  B[a]  List@i
6.  R  :  \mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{})@i
7.  a  :  A@i
8.  \muparrow{}a  \mmember{}  dom(fpf-union-join(eq;R;f;g))
9.  x  :  B[a]@i
10.  R  \mmember{}  (B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{}
11.  \muparrow{}a  \mmember{}  dom(f)
12.  \muparrow{}a  \mmember{}  dom(g)
13.  (x  \mmember{}  f(a)  @  filter(R  f(a);g(a)))@i
\mvdash{}  (True  \mwedge{}  (x  \mmember{}  f(a)))  \mvee{}  (True  \mwedge{}  (x  \mmember{}  g(a)))


By

((RWO  "member\_append"  (-1)  THENM  RWO  "member\_filter"  (-1))  THENA  Auto)

---

Home Index