Nuprl Lemma : pircv_wf
∀[chan,var:Name]. (pircv(chan;var) ∈ pi_prefix())
Proof
Definitions occuring in Statement :
pircv: pircv(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(),
pircv: pircv(chan;var),
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt
Latex:
\mforall{}[chan,var:Name]. (pircv(chan;var) \mmember{} pi\_prefix())
Date html generated:
2016_05_17-AM-11_19_48
Last ObjectModification:
2015_12_29-PM-06_58_48
Theory : event-logic-applications
Home
Index