---

{ tg:Id. links:IdLnk List. k:Knd.
    ((k  Rcvs(tg) on links)
     (isrcv(k))  (tag(k) = tg)  (lnk(k)  links)) }

{ Proof }

---

Definitions occuring in Statement :  rcvs-on: Rcvs(tg) on links,  tagof: tag(k),  lnk: lnk(k),  isrcv: isrcv(k),  Knd: Knd,  IdLnk: IdLnk,  Id: Id,  assert: b,  all: x:A. B[x],  iff: P  Q,  and: P  Q,  list: type List,  equal: s = t,  l_member: (x  l)
Definitions :  iff: P  Q,  and: P  Q,  product: x:A  B[x],  Knd: Knd,  list: type List,  IdLnk: IdLnk,  Id: Id,  all: x:A. B[x],  function: x:A  B[x],  member: t  T,  equal: s = t,  rcvs-on: Rcvs(tg) on links,  rev_implies: P  Q,  map: map(f;as),  combination: Combination(n;T),  listp: A List,  exists: x:A. B[x],  apply: f a,  lambda: x.A[x],  rcv: rcv(l,tg),  subtype_rel: A r B,  strong-subtype: strong-subtype(A;B),  union: left + right,  atom: Atom$n,  isrcv: isrcv(k),  cand: A c B,  prop: ,  l_member: (x  l),  universe: Type,  tagof: tag(k),  lnk: lnk(k),  implies: P  Q,  assert: b,  select: l[i],  remove-repeats: remove-repeats(eq;L),  last: last(L),  hd: hd(l),  set: {x:A| B[x]} ,  append: as @ bs,  limited-type: LimitedType,  nil: [],  cons: [car / cdr],  or: P  Q,  so_apply: x[s],  nat: ,  bool: ,  less_than: a < b,  ifthenelse: if b then t else f fi ,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  isrcv_rcv: isrcv_rcv{isrcv_rcv_compseq_tag_def:o}(tg; l),  true: True,  tag_rcv: tag_rcv{tag_rcv_compseq_tag_def:o}(tg; l),  sq_type: SQType(T),  guard: {T},  lnk_rcv: lnk_rcv{lnk_rcv_compseq_tag_def:o}(tg; l),  pair: <a, b>,  tactic: Error :tactic,  CollapseTHEN: Error :CollapseTHEN,  MaAuto: Error :MaAuto,  Auto: Error :Auto,  false: False
Lemmas :  Id_sq,  Knd_sq,  l_member_subtype,  lnk_wf,  l_member_wf,  tagof_wf,  isrcv_wf,  assert_wf,  rcv_wf,  map_wf,  rev_implies_wf,  iff_wf,  member_map,  iff_functionality_wrt_iff,  Id_wf,  IdLnk_wf,  Knd_wf

---

\mforall{}tg:Id.  \mforall{}links:IdLnk  List.  \mforall{}k:Knd.
    ((k  \mmember{}  Rcvs(tg)  on  links)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}isrcv(k))  \mwedge{}  (tag(k)  =  tg)  \mwedge{}  (lnk(k)  \mmember{}  links))


Date html generated: 2010_08_26-PM-11_34_16
Last ObjectModification: 2009_10_09-PM-10_31_10

Home Index