---

Step * 1 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
⊢ (↑x ∈ dom(g1)) ∨ (↑x ∈ dom(g2))
BY
{ (((RWO "fpf-join-dom" (-1)) THENA Auto)
   THEN ParallelLast
   THEN AllHyps h.((InstHyp [⌈x⌉] h)⋅ THEN ExRepD THEN Complete (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
\mvdash{}  (\muparrow{}x  \mmember{}  dom(g1))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g2))


By

(((RWO  "fpf-join-dom"  (-1))  THENA  Auto)
  THEN  ParallelLast
  THEN  AllHyps  h.((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THEN  ExRepD  THEN  Complete  (Auto))  )

---

Home Index