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
Definitions unfolded in proof :
pi_prefix: pi_prefix(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a
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:
2016_05_17-AM-11_19_40
Last ObjectModification:
2015_12_29-PM-06_58_46
Theory : event-logic-applications
Home
Index