Nuprl Lemma : pRun_wf
[M:Type 
Type]
[nat2msg:
pMsg(P.M[P])]. [loc2msg:Id pMsg(P.M[P])]. [S0:System(P.M[P])]. [env:pEnvType(P.M[P])].
(pRun(S0;env;nat2msg;loc2msg) 
fulpRunType(P.M[P]))
supposing Continuous+(P.M[P])
Proof not projected
Definitions occuring in Statement :
pRun: pRun(S0;env;nat2msg;loc2msg),
pEnvType: pEnvType(T.M[T]),
fulpRunType: fulpRunType(T.M[T]),
System: System(P.M[P]),
pMsg: pMsg(P.M[P]),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
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],
fulpRunType: fulpRunType(T.M[T]),
member: t T,
so_apply: x[s],
uimplies: b supposing a,
uall: [x:A]. B[x],
ycomb: Y,
pRun: pRun(S0;env;nat2msg;loc2msg),
top: Top,
nat: ,
false: False,
not: 
A,
le: A 
B,
ge: i 
j ,
guard: {T},
bfalse: ff,
btrue: tt,
exposed-bfalse: exposed-bfalse,
implies: P 
Q,
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
nat_plus: 
,
pEnvType: pEnvType(T.M[T]),
spreadn: spread3,
prop: 
,
and: P 
Q,
uiff: uiff(P;Q),
bool: 
,
unit: Unit,
lelt: i j < k,
int_seg: {i..j
},
System: System(P.M[P]),
it: 
Lemmas :
strong-type-continuous_wf,
nat_wf,
pMsg_wf,
Id_wf,
System_wf,
pEnvType_wf,
top_wf,
le_wf,
less_than_wf,
ge_wf,
nat_properties,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
it_wf,
assert_of_eq_int,
eqtt_to_assert,
assert_wf,
equal_wf,
uiff_transitivity,
bool_wf,
eq_int_wf,
int_seg_wf,
pInTransit_wf,
ldag_wf,
subtype_rel_self,
subtype_rel_simple_product,
do-chosen-command_wf,
unit_wf2,
pi2_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[nat2msg:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[loc2msg:Id {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[S0:System(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])].
(pRun(S0;env;nat2msg;loc2msg) \mmember{} fulpRunType(P.M[P]))
supposing Continuous+(P.M[P])
Date html generated:
2012_01_23-PM-12_42_25
Last ObjectModification:
2011_12_05-AM-11_55_15
Home
Index