---

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


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))))
BY
{ ((((RWO "member_map" (-1)) THENM Reduce (-1)) THENA Auto) THEN ExRepD THEN Decide (y ∈ d)⋅ THEN Auto) }

---

Latex:



1.  l  :  IdLnk
2.  k  :  Knd
3.  d  :  Id  List
4.  d1  :  tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type
5.  d2  :  Id  List
6.  d3  :  tg:\{tg:Id|  (tg  \mmember{}  d2)\}    {}\mrightarrow{}  Type
7.  (k  \mmember{}  map(\mlambda{}tg.rcv(l,tg);d2))@i
\mvdash{}  (k  \mmember{}  map(\mlambda{}tg.rcv(l,tg);d))  \mvee{}  (\mexists{}y:Id.  ((y  \mmember{}  d2)  \mwedge{}  ((\mneg{}(y  \mmember{}  d))  c\mwedge{}  (k  =  rcv(l,y)))))


By

((((RWO  "member\_map"  (-1))  THENM  Reduce  (-1))  THENA  Auto)
  THEN  ExRepD
  THEN  Decide  (y  \mmember{}  d)\mcdot{}
  THEN  Auto)

---

Home Index