---

input-code(lp.M[lp];n;T;code;decode) ==
  (v:T. ((decode (code v)) = (inl v )))
   (msg:process-input'(lp.M[lp];n)
       ((isl(decode msg))  ((code outl(decode msg)) = msg)))

---

Definitions :  and: P  Q,  union: left + right,  top: Top,  inl: inl x ,  all: x:A. B[x],  implies: P  Q,  assert: b,  isl: isl(x),  equal: s = t,  process-input': process-input'(lp.M[lp];n),  outl: outl(x),  apply: f a
FDL editor aliases :  input-code

---

input-code(lp.M[lp];n;T;code;decode)  ==
    (\mforall{}v:T.  ((decode  (code  v))  =  (inl  v  )))
    \mwedge{}  (\mforall{}msg:process-input'(lp.M[lp];n).  ((\muparrow{}isl(decode  msg))  {}\mRightarrow{}  ((code  outl(decode  msg))  =  msg)))


Date html generated: 2010_08_27-PM-08_36_05
Last ObjectModification: 2010_02_02-PM-05_46_20

Home Index