---

Step * 1 of Lemma fpf-compatible-update3


1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. f : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. h : a:A fp-> B[a]
7. f || g
⊢ h ⊕ f || h ⊕ g
BY
{ (D 0
   THEN Auto
   THEN (RWO "fpf-join-ap-sq" 0 THENA Auto)
   THEN SplitOnConclITE
   THEN Auto
   THEN (((RWO "fpf-join-dom" (-3)) THENM (D -3 THEN Auto)) THENA Auto)
   THEN (((RWO "fpf-join-dom" (-2)) THENM (D -2 THEN Auto)) THENA Auto))⋅ }

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  B  :  A  {}\mrightarrow{}  Type
4.  f  :  a:A  fp->  B[a]
5.  g  :  a:A  fp->  B[a]
6.  h  :  a:A  fp->  B[a]
7.  f  ||  g
\mvdash{}  h  \moplus{}  f  ||  h  \moplus{}  g


By

(D  0
  THEN  Auto
  THEN  (RWO  "fpf-join-ap-sq"  0  THENA  Auto)
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  (((RWO  "fpf-join-dom"  (-3))  THENM  (D  -3  THEN  Auto))  THENA  Auto)
  THEN  (((RWO  "fpf-join-dom"  (-2))  THENM  (D  -2  THEN  Auto))  THENA  Auto))\mcdot{}

---

Home Index