Nuprl Lemma : PiDataVal-induction
∀[P:PiDataVal() ⟶ ℙ]
((∀id:Id. P[pDVloc(id)])
⇒ (∀id:Id. ∀name:Name. P[pDVloc_tag(id;name)])
⇒ (∀from:Id. ∀preList:pi_prefix() List. P[pDVguards(from;preList)])
⇒ (∀val:Name. ∀index:ℕ. P[pDVmsg(val;index)])
⇒ P[pDVfire()]
⇒ P[pDVcontinue()]
⇒ (∀rndv1:ℕ × Id × ℕ × Name. P[pDVselex(rndv1)])
⇒ (∀rndv2:ℕ × Id × ℕ × Name. ∀counter:ℕ. P[pDVrequest(rndv2;counter)])
⇒ {∀x:PiDataVal(). P[x]})
Proof
Definitions occuring in Statement :
pDVrequest: pDVrequest(rndv2;counter),
pDVselex: pDVselex(rndv1),
pDVcontinue: pDVcontinue(),
pDVfire: pDVfire(),
pDVmsg: pDVmsg(val;index),
pDVguards: pDVguards(from;preList),
pDVloc_tag: pDVloc_tag(id;name),
pDVloc: pDVloc(id),
PiDataVal: PiDataVal(),
pi_prefix: pi_prefix(),
Id: Id,
name: Name,
list: T List,
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
product: x:A × B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
guard: {T},
all: ∀x:A. B[x],
member: t ∈ T,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
PiDataVal: PiDataVal(),
pDVloc: pDVloc(id),
pDVloc_tag: pDVloc_tag(id;name),
pDVguards: pDVguards(from;preList),
pDVmsg: pDVmsg(val;index),
unit: Unit,
it: ⋅,
pDVfire: pDVfire(),
pDVcontinue: pDVcontinue(),
pDVselex: pDVselex(rndv1),
pDVrequest: pDVrequest(rndv2;counter)
Latex:
\mforall{}[P:PiDataVal() {}\mrightarrow{} \mBbbP{}]
((\mforall{}id:Id. P[pDVloc(id)])
{}\mRightarrow{} (\mforall{}id:Id. \mforall{}name:Name. P[pDVloc\_tag(id;name)])
{}\mRightarrow{} (\mforall{}from:Id. \mforall{}preList:pi\_prefix() List. P[pDVguards(from;preList)])
{}\mRightarrow{} (\mforall{}val:Name. \mforall{}index:\mBbbN{}. P[pDVmsg(val;index)])
{}\mRightarrow{} P[pDVfire()]
{}\mRightarrow{} P[pDVcontinue()]
{}\mRightarrow{} (\mforall{}rndv1:\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name. P[pDVselex(rndv1)])
{}\mRightarrow{} (\mforall{}rndv2:\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name. \mforall{}counter:\mBbbN{}. P[pDVrequest(rndv2;counter)])
{}\mRightarrow{} \{\mforall{}x:PiDataVal(). P[x]\})
Date html generated:
2016_05_17-AM-11_27_18
Last ObjectModification:
2015_12_29-PM-06_52_44
Theory : event-logic-applications
Home
Index