---

Step * of Lemma fpf-join-dom-sq

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[x:A].  (x ∈ dom(f ⊕ g) ~ x ∈ dom(f) ∨bx ∈ dom(g))
BY
{ (Auto
   THEN D -3
   THEN D -2
   THEN RepUR ``fpf-join fpf-dom`` 0
   THEN (BLemma `iff_imp_equal_bool` THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "member_append" 0 THENA Auto)
   THEN ((RWO "member_filter" 0 THENM Reduce 0) THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)⋅) }

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
⊢ (x ∈ d) ∨ ((x ∈ d1) ∧ (¬(x ∈ d))) ⇐⇒ (x ∈ d) ∨ (x ∈ d1)

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  Top].  \mforall{}[x:A].
    (x  \mmember{}  dom(f  \moplus{}  g)  \msim{}  x  \mmember{}  dom(f)  \mvee{}\msubb{}x  \mmember{}  dom(g))


By

(Auto
  THEN  D  -3
  THEN  D  -2
  THEN  RepUR  ``fpf-join  fpf-dom``  0
  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "member\_append"  0  THENA  Auto)
  THEN  ((RWO  "member\_filter"  0  THENM  Reduce  0)  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)\mcdot{})

---

Home Index