Nuprl Lemma : PiDataVal_ind_wf
∀[X:𝕌{j}]. ∀[x:PiDataVal()]. ∀[loc:id:Id ─→ X]. ∀[loc_tag:id:Id ─→ name:Name ─→ X].
∀[guards:from:Id ─→ preList:(pi_prefix() List) ─→ X]. ∀[msg:val:Name ─→ index:ℕ ─→ X]. ∀[fire,continue:X].
∀[selex:rndv1:(ℕ × Id × ℕ × Name) ─→ X]. ∀[request:rndv2:(ℕ × Id × ℕ × Name) ─→ counter:ℕ ─→ X].
(F((x) where
F(id) = loc[id]
F(id,name) = loc_tag[id;name]
F(from,preList) = guards[from;preList]
F(val,index) = msg[val;index]
F(fire) = fire
F(continue) = continue
F(rndv1) = selex[rndv1]
F(rndv2,counter) = request[rndv2;counter] ∈ X)
Proof
Definitions occuring in Statement :
PiDataVal_ind: PiDataVal_ind,
PiDataVal: PiDataVal(),
pi_prefix: pi_prefix(),
Id: Id,
name: Name,
list: T List,
nat: ℕ,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
function: x:A ─→ B[x],
product: x:A × B[x],
universe: Type
Lemmas :
nat_wf,
Id_wf,
name_wf,
list_wf,
pi_prefix_wf,
PiDataVal_wf
Latex:
\mforall{}[X:\mBbbU{}\{j\}]. \mforall{}[x:PiDataVal()]. \mforall{}[loc:id:Id {}\mrightarrow{} X]. \mforall{}[loc$_{tag}$:id:Id {}\mrightarrow{} name:Name\000C {}\mrightarrow{} X].
\mforall{}[guards:from:Id {}\mrightarrow{} preList:(pi\_prefix() List) {}\mrightarrow{} X]. \mforall{}[msg:val:Name {}\mrightarrow{} index:\mBbbN{} {}\mrightarrow{} X].
\mforall{}[fire,continue:X]. \mforall{}[selex:rndv1:(\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name) {}\mrightarrow{} X]. \mforall{}[request:rndv2:(\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name)
{}\mrightarrow{} counter:\mBbbN{}
{}\mrightarrow{} X].
(F((x) where
F(id) = loc[id]
F(id,name) = loc$_{tag}$[id;name]
F(from,preList) = guards[from;preList]
F(val,index) = msg[val;index]
F(fire) = fire
F(continue) = continue
F(rndv1) = selex[rndv1]
F(rndv2,counter) = request[rndv2;counter] \mmember{} X)
Date html generated:
2015_07_23-AM-11_34_51
Last ObjectModification:
2015_01_29-AM-00_56_02
Home
Index