---

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


1. [A] : Type
2. eq : EqDecider(A)@i
3. f : a:A fp-> Top@i
4. g : a:A fp-> Top@i
5. x : A@i
6. R : Top@i
⊢ ↑x ∈ dom(fpf-union-join(eq;R;f;g)) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g))
BY
{ (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))) }

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

---

Latex:



1.  [A]  :  Type
2.  eq  :  EqDecider(A)@i
3.  f  :  a:A  fp->  Top@i
4.  g  :  a:A  fp->  Top@i
5.  x  :  A@i
6.  R  :  Top@i
\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

(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)))

---

Home Index