---

Step * 1 1 of Lemma fpf-union-contains2


1. [A] : Type
2. [V] : Type
3. [B] : A ⟶ Type
4. ∀a:A. ((B a) ⊆r V)
5. eq : EqDecider(A)
6. f : x:A fp-> (B x) List
7. g : x:A fp-> (B x) List
8. fpf-single-valued(A;eq;x.B x;V;g)
9. x : A
10. R : (V List) ⟶ V ⟶ 𝔹
11. fpf-union-compatible(A;V;x.B x;eq;R;f;g)
12. ↑x ∈ dom(g)
13. ↑x ∈ dom(f)
14. (B x) ⊆r V
15. a : B x
16. (a ∈ g(x))
⊢ (a ∈ f(x) @ filter(R f(x);g(x)))
BY
{ (((RWO "member_append" 0 THENM RWO "member_filter" 0) THENA Auto) THEN Decide ⌜↑(R f(x) a)⌝⋅ THEN Auto)⋅ }

1
1. [A] : Type
2. [V] : Type
3. [B] : A ⟶ Type
4. ∀a:A. ((B a) ⊆r V)
5. eq : EqDecider(A)
6. f : x:A fp-> (B x) List
7. g : x:A fp-> (B x) List
8. fpf-single-valued(A;eq;x.B x;V;g)
9. x : A
10. R : (V List) ⟶ V ⟶ 𝔹
11. fpf-union-compatible(A;V;x.B x;eq;R;f;g)
12. ↑x ∈ dom(g)
13. ↑x ∈ dom(f)
14. (B x) ⊆r V
15. a : B x
16. (a ∈ g(x))
17. ¬↑(R f(x) a)
⊢ (a ∈ f(x))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [V]  :  Type
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  \mforall{}a:A.  ((B  a)  \msubseteq{}r  V)
5.  eq  :  EqDecider(A)
6.  f  :  x:A  fp->  (B  x)  List
7.  g  :  x:A  fp->  (B  x)  List
8.  fpf-single-valued(A;eq;x.B  x;V;g)
9.  x  :  A
10.  R  :  (V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}
11.  fpf-union-compatible(A;V;x.B  x;eq;R;f;g)
12.  \muparrow{}x  \mmember{}  dom(g)
13.  \muparrow{}x  \mmember{}  dom(f)
14.  (B  x)  \msubseteq{}r  V
15.  a  :  B  x
16.  (a  \mmember{}  g(x))
\mvdash{}  (a  \mmember{}  f(x)  @  filter(R  f(x);g(x)))


By

---

Latex:
(((RWO  "member\_append"  0  THENM  RWO  "member\_filter"  0)  THENA  Auto)
  THEN  Decide  \mkleeneopen{}\muparrow{}(R  f(x)  a)\mkleeneclose{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index