---

Step * of Lemma fpf-join-wf

∀[A:Type]. ∀[B,C,D:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[eq:EqDecider(A)].
  (f ⊕ g ∈ a:A fp-> D[a]) supposing 
     ((∀a:A. ((↑a ∈ dom(g)) ⇒ (C[a] ⊆r D[a]))) and 
     (∀a:A. ((↑a ∈ dom(f)) ⇒ (B[a] ⊆r D[a]))))
BY
{ ((UnivCD THENA Auto)
   THEN DVar `f'
   THEN DVar `g'
   THEN RepUR ``fpf-join fpf fpf-dom fpf-cap`` 0
   THEN All (RepUR ``fpf-dom``)) }

1
1. A : Type
2. B : A ⟶ Type
3. C : A ⟶ Type
4. D : A ⟶ Type
5. d : A List
6. f1 : a:{a:A| (a ∈ d)}  ⟶ B[a]
7. d1 : A List
8. g1 : a:{a:A| (a ∈ d1)}  ⟶ C[a]
9. eq : EqDecider(A)
10. ∀a:A. ((↑a ∈b d) ⇒ (B[a] ⊆r D[a]))
11. ∀a:A. ((↑a ∈b d1) ⇒ (C[a] ⊆r D[a]))
⊢ <d @ filter(λa.(¬ba ∈b d);d1), λa.if a ∈b d then f1 a else g1 a fi > ∈ d:A List × (a:{a:A| (a ∈ d)}  ⟶ D[a])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B,C,D:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[g:a:A  fp->  C[a]].  \mforall{}[eq:EqDecider(A)].
    (f  \moplus{}  g  \mmember{}  a:A  fp->  D[a])  supposing 
          ((\mforall{}a:A.  ((\muparrow{}a  \mmember{}  dom(g))  {}\mRightarrow{}  (C[a]  \msubseteq{}r  D[a])))  and 
          (\mforall{}a:A.  ((\muparrow{}a  \mmember{}  dom(f))  {}\mRightarrow{}  (B[a]  \msubseteq{}r  D[a]))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  DVar  `f'
  THEN  DVar  `g'
  THEN  RepUR  ``fpf-join  fpf  fpf-dom  fpf-cap``  0
  THEN  All  (RepUR  ``fpf-dom``))

---

Home Index