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