---

Step * of Lemma fpf-union-contains2

∀[A,V:Type]. ∀[B:A ─→ Type].
  ∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List.
    ∀x:A. ∀R:(V List) ─→ V ─→ 𝔹.  (fpf-union-compatible(A;V;x.B[x];eq;R;f;g) ⇒ g(x)?[] ⊆ fpf-union(f;g;eq;R;x)) 
    supposing fpf-single-valued(A;eq;x.B[x];V;g) 
  supposing ∀a:A. (B[a] ⊆r V)
BY
{ (Auto THEN RepUR ``fpf-union fpf-cap`` 0 THEN RepeatFor 2 (AutoSplit) THEN (Assert B[x] ⊆r V BY Auto)⋅) }

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

---

Latex:


\mforall{}[A,V:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f,g:x:A  fp->  B[x]  List.
        \mforall{}x:A.  \mforall{}R:(V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}.
            (fpf-union-compatible(A;V;x.B[x];eq;R;f;g)  {}\mRightarrow{}  g(x)?[]  \msubseteq{}  fpf-union(f;g;eq;R;x)) 
        supposing  fpf-single-valued(A;eq;x.B[x];V;g) 
    supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  V)


By

(Auto
  THEN  RepUR  ``fpf-union  fpf-cap``  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (Assert  B[x]  \msubseteq{}r  V  BY
                          Auto)\mcdot{})

---

Home Index