Nuprl Definition : oar-failure-model

There are 3f+1 orderers and no more than f of them are incorrect.
(Without assuming that "correct" is decidable, we can't say that 2f+1 of
them are correct because we don't know which of them is correct.)⋅

oar-failure-model(orderers;f;correct) ==
  (#(orderers) = ((3 * f) + 1) ∈ ℤ)
  ∧ bag-no-repeats(Id;orderers)
  ∧ (¬(∃b:bag(Id). (f < #(b) ∧ bag-no-repeats(Id;b) ∧ (∀x:Id. (x ↓∈ b ⇒ (x ↓∈ orderers ∧ (¬(correct x))))))))

Definitions occuring in Statement : Id: Id, less_than: a < b, all: ∀x:A. B[x], exists: ∃x:A. B[x], not: ¬A, implies: P ⇒ Q, and: P ∧ Q, apply: f a, multiply: n * m, add: n + m, natural_number: $n, int: ℤ, equal: s = t ∈ T, bag-member: x ↓∈ bs, bag-no-repeats: bag-no-repeats(T;bs), bag-size: #(bs), bag: bag(T)
FDL editor aliases : oar-failure-model

Latex:
oar-failure-model(orderers;f;correct) == (\#(orderers) = ((3 * f) + 1)) \mwedge{} bag-no-repeats(Id;orderers) \mwedge{} (\mneg{}(\mexists{}b:bag(Id) (f < \#(b) \mwedge{} bag-no-repeats(Id;b) \mwedge{} (\mforall{}x:Id. (x \mdownarrow{}\mmember{} b {}\mRightarrow{} (x \mdownarrow{}\mmember{} orderers \mwedge{} (\mneg{}(correct x)))))))) Date html generated: 2015_07_23-PM-00_27_07 Last ObjectModification: 2014_07_07-PM-01_13_49 Home Index