---

Step * of Lemma fpf-domain-union-join

∀[A:Type]
  ∀f:a:A fp-> Top List. ∀g:a:A fp-> Top. ∀eq:EqDecider(A). ∀x:A. ∀R:Top.
    ((x ∈ fpf-domain(fpf-union-join(eq;R;f;g))) ⇐⇒ (x ∈ fpf-domain(f)) ∨ (x ∈ fpf-domain(g)))
BY
{ ((UnivCD THENA Auto)
   THEN DVar `f'
   THEN DVar `g'
   THEN RepUR ``fpf-domain fpf-union-join fpf-dom`` 0
   THEN ((RWO "member_append" 0 THENM RWO "member_filter" 0) THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN Try ((ProveProp THEN Auto))
   THEN Decide ⌈↑x ∈b d)⌉⋅
   THEN Auto
   THEN ((RW assert_pushdownC (-1)) THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN ProveProp
   THEN Auto) }

---

Latex:


\mforall{}[A:Type]
    \mforall{}f:a:A  fp->  Top  List.  \mforall{}g:a:A  fp->  Top.  \mforall{}eq:EqDecider(A).  \mforall{}x:A.  \mforall{}R:Top.
        ((x  \mmember{}  fpf-domain(fpf-union-join(eq;R;f;g)))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  fpf-domain(f))  \mvee{}  (x  \mmember{}  fpf-domain(g)))


By

((UnivCD  THENA  Auto)
  THEN  DVar  `f'
  THEN  DVar  `g'
  THEN  RepUR  ``fpf-domain  fpf-union-join  fpf-dom``  0
  THEN  ((RWO  "member\_append"  0  THENM  RWO  "member\_filter"  0)  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((ProveProp  THEN  Auto))
  THEN  Decide  \mkleeneopen{}\muparrow{}x  \mmember{}\msubb{}  d)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ((RW  assert\_pushdownC  (-1))  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  ProveProp
  THEN  Auto)

---

Home Index