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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
PiDataVal: PiDataVal(),
PiDataVal_ind: PiDataVal_ind,
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
so_apply: x[s1;s2]
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:
2016_05_17-AM-11_27_09
Last ObjectModification:
2015_12_29-PM-06_52_50
Theory : event-logic-applications
Home
Index