---

Step * 1 of Lemma fpf-union-join-dom


1. [A] : Type
2. eq : EqDecider(A)
3. f : a:A fp-> Top
4. g : a:A fp-> Top
5. x : A
6. R : Top
⊢ ↑x ∈ dom(fpf-union-join(eq;R;f;g)) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g))
BY
{ xxx(DVar `f'
      THEN DVar `g'
      THEN RepUR ``fpf-dom fpf-union-join`` 0
      THEN ((RW assert_pushdownC 0 THENM RWO "member_append" 0 THENM RWO "member_filter" 0) THENA Auto)
      THEN Reduce 0
      THEN Auto
      THEN Try ((ProveProp THEN Auto)))xxx }

1
1. [A] : Type
2. eq : EqDecider(A)
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ⟶ Top
5. d1 : A List
6. g1 : a:{a:A| (a ∈ d1)}  ⟶ Top
7. x : A
8. R : Top
9. (x ∈ d) ∨ (x ∈ d1)
⊢ (x ∈ d) ∨ ((x ∈ d1) ∧ (↑¬bx ∈b d))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  eq  :  EqDecider(A)
3.  f  :  a:A  fp->  Top
4.  g  :  a:A  fp->  Top
5.  x  :  A
6.  R  :  Top
\mvdash{}  \muparrow{}x  \mmember{}  dom(fpf-union-join(eq;R;f;g))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g))


By

---

Latex:
xxx(DVar  `f'
        THEN  DVar  `g'
        THEN  RepUR  ``fpf-dom  fpf-union-join``  0
        THEN  ((RW  assert\_pushdownC  0  THENM  RWO  "member\_append"  0  THENM  RWO  "member\_filter"  0)
                    THENA  Auto
                    )
        THEN  Reduce  0
        THEN  Auto
        THEN  Try  ((ProveProp  THEN  Auto)))xxx

---

Home Index