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]
Lemmas :
PiDataVal_wf,
all_wf,
nat_wf,
Id_wf,
name_wf,
pDVrequest_wf,
pDVselex_wf,
pDVcontinue_wf,
pDVfire_wf,
pDVmsg_wf,
list_wf,
pi_prefix_wf,
pDVguards_wf,
pDVloc_tag_wf,
pDVloc_wf
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:
2015_07_23-AM-11_34_56
Last ObjectModification:
2015_01_29-AM-00_55_55
Home
Index