Nuprl Lemma : pRun2_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])]. [t:].
(pRun2(S0;env;nat2msg;loc2msg;t)
{L:(
Id Id pMsg(P.M[P])? System(P.M[P])) List| ||L|| = (t + 1)} )) supposing
(Continuous+(P.M[P]) and
(P:Type. value-type(M[P])) and
M[Top])
Proof not projected
Definitions occuring in Statement :
pRun2: pRun2(S0;env;nat2msg;loc2msg;t),
pEnvType: pEnvType(T.M[T]),
System: System(P.M[P]),
pMsg: pMsg(P.M[P]),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
length: ||as||,
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
all: x:A. B[x],
unit: Unit,
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
add: n + m,
natural_number: $n,
int: ,
universe: Type,
equal: s = t,
value-type: value-type(T)
Definitions :
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 ,
ycomb: Y,
prop: 
,
so_lambda: 
x.t[x],
pRun2: pRun2(S0;env;nat2msg;loc2msg;t),
member: t T,
all: x:A. B[x],
so_apply: x[s],
uimplies: b supposing a,
uall: [x:A]. B[x],
has-value: has-value(a),
id-fun: id-fun(T),
length: ||as||,
System: System(P.M[P]),
subtype: S 
T,
spreadn: spread3,
top: Top,
null: null(as),
assert: 
b,
pRunInfo: pRunInfo(P.M[P]),
and: P 
Q,
uiff: uiff(P;Q),
bool: 
,
unit: Unit,
int_seg: {i..j
},
it: 
Lemmas :
le_wf,
less_than_wf,
ge_wf,
nat_properties,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
assert_of_eq_int,
eqtt_to_assert,
assert_wf,
equal_wf,
uiff_transitivity,
bool_wf,
eq_int_wf,
top_wf,
value-type_wf,
all_wf,
strong-type-continuous_wf,
pMsg_wf,
Id_wf,
System_wf,
pEnvType_wf,
nat_wf,
length_wf,
unit_wf2,
it_wf,
pInTransit_wf,
ldag_wf,
component_wf,
product-value-type,
id-fun_wf,
norm-system_wf,
subtype_rel_self,
subtype_rel_simple_product,
select_wf,
list-value-type,
set-value-type,
last_wf,
pi2_wf,
do-chosen-command_wf,
true_wf,
false_wf,
norm-runinfo_wf,
pRunInfo_wf,
and_wf,
length-append,
append_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])]. \mforall{}[t:\mBbbN{}].
(pRun2(S0;env;nat2msg;loc2msg;t) \mmember{} \{L:(\mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])? \mtimes{} System(P.M[P])) List|
||L|| = (t + 1)\} )) supposing
(Continuous+(P.M[P]) and
(\mforall{}P:Type. value-type(M[P])) and
M[Top])
Date html generated:
2012_01_23-PM-12_42_41
Last ObjectModification:
2011_12_14-PM-03_19_53
Home
Index