Nuprl Lemma : pisend_wf
∀[chan,var:Name]. (pisend(chan;var) ∈ pi_prefix())
Proof
Definitions occuring in Statement :
pisend: pisend(chan;var),
pi_prefix: pi_prefix(),
name: Name,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
pi_prefix: pi_prefix(),
pisend: pisend(chan;var),
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
btrue: tt
Latex:
\mforall{}[chan,var:Name]. (pisend(chan;var) \mmember{} pi\_prefix())
Date html generated:
2016_05_17-AM-11_19_44
Last ObjectModification:
2015_12_29-PM-06_58_49
Theory : event-logic-applications
Home
Index