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) ∈ ℤ} )) \000Csupposing
(Continuous+(P.M[P]) and
(∀P:Type. value-type(M[P])) and
M[Top])
Proof
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,
length: ||as||,
list: T List,
strong-type-continuous: Continuous+(T.F[T]),
nat: ℕ,
value-type: value-type(T),
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,
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions :
select: L[n],
nil: [],
it: ⋅
Lemmas :
nat_properties,
less_than_transitivity1,
less_than_irreflexivity,
ge_wf,
less_than_wf,
int_seg_wf,
decidable__le,
subtract_wf,
false_wf,
not-ge-2,
less-iff-le,
condition-implies-le,
minus-one-mul,
zero-add,
minus-add,
minus-minus,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
decidable__equal_int,
subtype_rel-int_seg,
le_weakening,
int_seg_properties,
le_wf,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
int_upper_subtype_nat,
nequal-le-implies,
decidable__lt,
not-equal-2,
le-add-cancel-alt,
lelt_wf,
not-le-2,
sq_stable__le,
add-mul-special,
zero-mul,
nat_wf,
pEnvType_wf,
System_wf,
Id_wf,
pMsg_wf,
strong-type-continuous_wf,
all_wf,
value-type_wf,
top_wf,
norm-system_wf,
id-fun_wf,
set_wf,
has-value_wf_base,
cons_wf,
unit_wf2,
it_wf,
nil_wf,
length_of_cons_lemma,
length_of_nil_lemma,
int_subtype_base,
length_wf,
subtract-is-less,
list_wf,
value-type-has-value,
set-value-type,
list-value-type,
select_wf,
do-chosen-command_wf,
last_wf,
list-cases,
null_nil_lemma,
stuck-spread,
base_wf,
le_antisymmetry_iff,
product_subtype_list,
null_cons_lemma,
assert_wf,
null_wf3,
subtype_rel_list,
norm-runinfo_wf,
pRunInfo_wf,
append_wf,
length-append,
and_wf
Latex:
\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:
2015_07_23-AM-11_10_13
Last ObjectModification:
2015_01_29-AM-00_13_18
Home
Index