---

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
{ xxx((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)xxx }

---

Latex:

---

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

---

Latex:
xxx((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)xxx

---

Home Index