---

{ [M:IdLnk  Id  Type]. [rt:Id  Id]. [rtinv:Id  (Id?)].
    [m:Msg(M)]
      msg-rename(rtinv;m)  Msg(l,tg.(M l (rt tg))) 
      supposing isl(rtinv mtag(m)) 
    supposing inv-rel(Id;Id;rt;rtinv) }

{ Proof }

---

Definitions occuring in Statement :  msg-rename: msg-rename(rtinv;m),  mtag: mtag(m),  Msg: Msg(M),  IdLnk: IdLnk,  Id: Id,  isl: isl(x),  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  union: left + right,  universe: Type,  inv-rel: inv-rel(A;B;f;finv)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  member: t  T,  Msg: Msg(M),  msg-rename: msg-rename(rtinv;m),  pi1: fst(t),  pi2: snd(t),  assert: b,  isl: isl(x),  outl: outl(x),  implies: P  Q,  all: x:A. B[x],  btrue: tt,  bfalse: ff,  ifthenelse: if b then t else f fi ,  mtag: mtag(m),  false: False,  inv-rel: inv-rel(A;B;f;finv),  and: P  Q,  prop: ,  guard: {T}
Lemmas :  assert_wf,  isl_wf,  Id_wf,  unit_wf,  mtag_wf,  Msg_wf,  inv-rel_wf,  IdLnk_wf,  outl_wf,  true_wf,  false_wf

---

\mforall{}[M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type].  \mforall{}[rt:Id  {}\mrightarrow{}  Id].  \mforall{}[rtinv:Id  {}\mrightarrow{}  (Id?)].
    \mforall{}[m:Msg(M)].  msg-rename(rtinv;m)  \mmember{}  Msg(\mlambda{}l,tg.(M  l  (rt  tg)))  supposing  \muparrow{}isl(rtinv  mtag(m)) 
    supposing  inv-rel(Id;Id;rt;rtinv)


Date html generated: 2011_08_10-AM-07_46_28
Last ObjectModification: 2011_06_18-AM-08_12_11

Home Index