Nuprl Lemma : oar-failure-model_wf
∀[orderers:bag(Id)]. ∀[f:ℤ]. ∀[correct:Id ─→ ℙ]. (oar-failure-model(orderers;f;correct) ∈ ℙ)
Proof
Definitions occuring in Statement :
oar-failure-model: oar-failure-model(orderers;f;correct),
Id: Id,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ─→ B[x],
int: ℤ,
bag: bag(T)
Lemmas :
equal-wf-T-base,
bag-size_wf,
Id_wf,
nat_wf,
int_subtype_base,
bag-no-repeats_wf,
not_wf,
exists_wf,
bag_wf,
less_than_wf,
all_wf,
bag-member_wf
Latex:
\mforall{}[orderers:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[correct:Id {}\mrightarrow{} \mBbbP{}]. (oar-failure-model(orderers;f;correct) \mmember{} \mBbbP{})
Date html generated:
2015_07_23-PM-00_27_11
Last ObjectModification:
2015_01_29-AM-01_28_37
Home
Index