---

Step * 2 of Lemma fpf-join-sub


1. A : Type
2. B : A ─→ Type
3. eq : EqDecider(A)
4. f1 : a:A fp-> B[a]
5. g1 : a:A fp-> B[a]
6. f2 : a:A fp-> B[a]
7. g2 : a:A fp-> B[a]
8. f2 || g1
9. ∀x:A. ((↑x ∈ dom(f1)) ⇒ ((↑x ∈ dom(g1)) c∧ (f1(x) = g1(x) ∈ B[x])))
10. ∀x:A. ((↑x ∈ dom(f2)) ⇒ ((↑x ∈ dom(g2)) c∧ (f2(x) = g2(x) ∈ B[x])))
11. x : A@i
12. ↑x ∈ dom(f1 ⊕ f2)@i
13. ↑x ∈ dom(g1 ⊕ g2)
⊢ f1 ⊕ f2(x) = g1 ⊕ g2(x) ∈ B[x]
BY
{ (((((((RWO "fpf-join-ap-sq" 0 THENA Auto) THEN SplitOnConclITE) THENA Auto) THEN SplitOnConclITE) THENA Auto)
    THEN AllHyps h.((InstHyp [⌈x⌉] h)⋅ THEN ExRepD THEN Complete (Auto)) 
    THEN AllHyps h.((RWO "fpf-join-dom" h) THENA Auto) )
   THEN SplitOrHyps⋅
   THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)
4.  f1  :  a:A  fp->  B[a]
5.  g1  :  a:A  fp->  B[a]
6.  f2  :  a:A  fp->  B[a]
7.  g2  :  a:A  fp->  B[a]
8.  f2  ||  g1
9.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(f1))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(g1))  c\mwedge{}  (f1(x)  =  g1(x))))
10.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(f2))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(g2))  c\mwedge{}  (f2(x)  =  g2(x))))
11.  x  :  A@i
12.  \muparrow{}x  \mmember{}  dom(f1  \moplus{}  f2)@i
13.  \muparrow{}x  \mmember{}  dom(g1  \moplus{}  g2)
\mvdash{}  f1  \moplus{}  f2(x)  =  g1  \moplus{}  g2(x)


By

(((((((RWO  "fpf-join-ap-sq"  0  THENA  Auto)  THEN  SplitOnConclITE)  THENA  Auto)  THEN  SplitOnConclITE)
      THENA  Auto
      )
    THEN  AllHyps  h.((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THEN  ExRepD  THEN  Complete  (Auto)) 
    THEN  AllHyps  h.((RWO  "fpf-join-dom"  h)  THENA  Auto)  )
  THEN  SplitOrHyps\mcdot{}
  THEN  Auto)

---

Home Index