Nuprl Lemma : run-command_wf
[M:Type 
Type]. [r:pRunType(P.M[P])]. [t,n:
].
run-command(r;t;n) 
pInTransit(P.M[P]) supposing run-command-node(r;t;n)
Proof not projected
Definitions occuring in Statement :
run-command: run-command(r;t;n),
run-command-node: run-command-node(r;t;n),
pRunType: pRunType(T.M[T]),
pInTransit: pInTransit(P.M[P]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
so_lambda: 
x.t[x],
member: t T,
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
and: P 
Q,
lelt: i 
j < k,
int_seg: {i..j
},
pi2: snd(t),
run-command: run-command(r;t;n),
run-command-node: run-command-node(r;t;n),
implies: P 
Q,
pRunType: pRunType(T.M[T]),
all: x:A. B[x],
ldag: LabeledDAG(T),
prop: 
,
nat:
Lemmas :
pRunType_wf,
nat_wf,
run-command-node_wf,
less_than_wf,
lg-size_wf_dag,
lelt_wf,
lg-label_wf_dag,
pInTransit_wf,
ldag_wf,
top_wf,
unit_wf2,
pMsg_wf,
Id_wf,
pi2_wf,
is-dag_wf
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[r:pRunType(P.M[P])]. \mforall{}[t,n:\mBbbN{}].
run-command(r;t;n) \mmember{} pInTransit(P.M[P]) supposing run-command-node(r;t;n)
Date html generated:
2012_01_23-PM-12_44_26
Last ObjectModification:
2012_01_06-AM-10_24_21
Home
Index