Nuprl Lemma : OARcast_deliverer_for_sender_seq_update_wf
∀[M:ValueAllType]. ∀[deqM:EqDecider(M)].
(OARcast_deliverer_for_sender_seq_update(M;deqM) ∈ Id
─→ ℤ
─→ Id
─→ (Id × Id × ℤ × M)
─→ (bag(Id) × ((M × ℕ) List))
─→ (bag(Id) × ((M × ℕ) List)))
Proof
Definitions occuring in Statement :
OARcast_deliverer_for_sender_seq_update: OARcast_deliverer_for_sender_seq_update(M;deqM),
Id: Id,
deq: EqDecider(T),
list: T List,
nat: ℕ,
vatype: ValueAllType,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
product: x:A × B[x],
int: ℤ,
bag: bag(T)
Lemmas :
eq_id_wf,
bool_wf,
eqtt_to_assert,
assert-eq-id,
eq_int_wf,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert_of_eq_int,
bag-deq-member_wf,
Id_wf,
id-deq_wf,
assert-bag-deq-member,
value-type-has-value,
bag_wf,
bag-value-type,
eval_bag_wf,
bag-remove_wf,
list_wf,
list-value-type,
Error :eval_list_wf,
weak-update-alist_wf,
subtype_rel_list,
nat_wf,
subtype_rel_product,
false_wf,
le_wf,
decidable__le,
not-le-2,
sq_stable__le,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
eqff_to_assert,
assert-bnot,
bag-member_wf,
deq_wf,
set_wf,
valueall-type_wf
Latex:
\mforall{}[M:ValueAllType]. \mforall{}[deqM:EqDecider(M)].
(OARcast\_deliverer\_for\_sender\_seq\_update(M;deqM) \mmember{} Id
{}\mrightarrow{} \mBbbZ{}
{}\mrightarrow{} Id
{}\mrightarrow{} (Id \mtimes{} Id \mtimes{} \mBbbZ{} \mtimes{} M)
{}\mrightarrow{} (bag(Id) \mtimes{} ((M \mtimes{} \mBbbN{}) List))
{}\mrightarrow{} (bag(Id) \mtimes{} ((M \mtimes{} \mBbbN{}) List)))
Date html generated:
2015_07_23-PM-00_32_52
Last ObjectModification:
2015_01_29-AM-00_44_56
Home
Index