Nuprl Lemma : constrained-msg-interface-valueall-type
∀[f:Name ─→ Type]. ∀[locs:Id List]. ∀[hdrs:Name List].
valueall-type(Interface(to locs, with hdrs)) supposing (∀h∈hdrs.valueall-type(f h))
Proof
Definitions occuring in Statement :
constrained-msg-interface: Interface(to locs, with hdrs),
Id: Id,
name: Name,
l_all: (∀x∈L.P[x]),
list: T List,
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a,
function: x:A ─→ B[x],
universe: Type
Lemmas :
sq_stable__valueall-type,
decidable__lt,
length_wf,
name_wf,
false_wf,
less-iff-le,
add_functionality_wrt_le,
add-swap,
add-commutes,
le-add-cancel,
lelt_wf,
subtype_base_sq,
list_subtype_base,
atom_subtype_base,
equal-wf-base,
constrained-msg-interface_wf,
base_wf,
l_all_wf2,
valueall-type_wf,
l_member_wf,
list_wf,
Id_wf,
evalall-pair,
valueall-type-has-valueall,
int-valueall-type,
Id-valueall-type,
bool_wf,
union-valueall-type,
unit_wf2,
equal-valueall-type,
name-valueall-type,
has-value_wf_base
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[locs:Id List]. \mforall{}[hdrs:Name List].
valueall-type(Interface(to locs, with hdrs)) supposing (\mforall{}h\mmember{}hdrs.valueall-type(f h))
Date html generated:
2015_07_22-AM-11_59_18
Last ObjectModification:
2015_01_28-AM-08_42_09
Home
Index