Nuprl Lemma : pi_prefix-ext
pi_prefix() ≡ lbl:Atom × if lbl =a "send" then chan:Name × Name
if lbl =a "rcv" then chan:Name × Name
else Void
fi
Proof
Definitions occuring in Statement :
pi_prefix: pi_prefix(),
name: Name,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
ext-eq: A ≡ B,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
Lemmas :
ext-eq_weakening,
pi_prefix_wf
Latex:
pi\_prefix() \mequiv{} lbl:Atom \mtimes{} if lbl =a "send" then chan:Name \mtimes{} Name
if lbl =a "rcv" then chan:Name \mtimes{} Name
else Void
fi
Date html generated:
2015_07_23-AM-11_31_18
Last ObjectModification:
2015_01_29-AM-00_52_53
Home
Index