---

Step * 1 of Lemma lnk-decl-dom-join


1. l : IdLnk
2. k : Knd
3. dt1 : tg:Id fp-> Type
4. dt2 : tg:Id fp-> Type
⊢ ↑k ∈b map(λtg.rcv(l,tg);fst(dt1 ⊕ dt2))) ⇐⇒ ↑(k ∈b map(λtg.rcv(l,tg);fst(dt1))) ∨bk ∈b map(λtg.rcv(l,tg);fst(dt2))))
BY
{ (D -2
   THEN D -1
   THEN RepUR ``fpf-join fpf-dom`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "map_append_sq" 0 THENA Auto)
   THEN (RWO "member_append" 0 THENA Auto)
   THEN Fold `mapfilter` 0
   THEN (RWO "member_map_filter" 0 THENA (Reduce 0 THEN Auto THEN Reduce 0 THEN Auto))
   THEN Reduce 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Auto
   THEN D -1
   THEN Auto) }

1
1. l : IdLnk
2. k : Knd
3. d : Id List
4. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
5. d2 : Id List
6. d3 : tg:{tg:Id| (tg ∈ d2)}  ─→ Type
7. (k ∈ map(λtg.rcv(l,tg);d2))@i
⊢ (k ∈ map(λtg.rcv(l,tg);d)) ∨ (∃y:Id. ((y ∈ d2) ∧ ((¬(y ∈ d)) c∧ (k = rcv(l,y) ∈ Knd))))

---

Latex:



1.  l  :  IdLnk
2.  k  :  Knd
3.  dt1  :  tg:Id  fp->  Type
4.  dt2  :  tg:Id  fp->  Type
\mvdash{}  \muparrow{}k  \mmember{}\msubb{}  map(\mlambda{}tg.rcv(l,tg);fst(dt1  \moplus{}  dt2)))
\mLeftarrow{}{}\mRightarrow{}  \muparrow{}(k  \mmember{}\msubb{}  map(\mlambda{}tg.rcv(l,tg);fst(dt1)))  \mvee{}\msubb{}k  \mmember{}\msubb{}  map(\mlambda{}tg.rcv(l,tg);fst(dt2))))


By

(D  -2
  THEN  D  -1
  THEN  RepUR  ``fpf-join  fpf-dom``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
  THEN  (RWO  "member\_append"  0  THENA  Auto)
  THEN  Fold  `mapfilter`  0
  THEN  (RWO  "member\_map\_filter"  0  THENA  (Reduce  0  THEN  Auto  THEN  Reduce  0  THEN  Auto))
  THEN  Reduce  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index