---

Step * of Lemma fpf-join-list-ap-disjoint

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[L:a:A fp-> B[a] List]. ∀[x:A].
  (∀[f:a:A fp-> B[a]]. (⊕(L)(x) = f(x) ∈ B[x]) supposing ((↑x ∈ dom(f)) and (f ∈ L))) supposing 
     ((∀f,g∈L.  ∀x:A. (¬((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))))) and 
     (↑x ∈ dom(⊕(L))))
BY
{ (InstLemma `fpf-join-list-ap` []
   THEN RepeatFor 5 ((ParallelLast THEN Thin (-3)))
   THEN (D 0 THENA Auto)
   THEN (D -2 THENA Auto)
   THEN D -1
   THEN Auto) }

1
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. L : a:A fp-> B[a] List
5. x : A
6. ↑x ∈ dom(⊕(L))
7. i : ℕ||L||
8. ↑x ∈ dom(L[i])
9. ⊕(L)(x) = L[i](x) ∈ B[x]
10. (∀f,g∈L.  ∀x:A. (¬((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g)))))
11. f : a:A fp-> B[a]
12. (f ∈ L)
13. ↑x ∈ dom(f)
⊢ ⊕(L)(x) = f(x) ∈ B[x]

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[L:a:A  fp->  B[a]  List].  \mforall{}[x:A].
    (\mforall{}[f:a:A  fp->  B[a]].  (\moplus{}(L)(x)  =  f(x))  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  (f  \mmember{}  L)))  supposing 
          ((\mforall{}f,g\mmember{}L.    \mforall{}x:A.  (\mneg{}((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}x  \mmember{}  dom(g)))))  and 
          (\muparrow{}x  \mmember{}  dom(\moplus{}(L))))


By

(InstLemma  `fpf-join-list-ap`  []
  THEN  RepeatFor  5  ((ParallelLast  THEN  Thin  (-3)))
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index