Nuprl Definition : consensus-rel-knowledge-inning-step
consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a) ==
(Inning(y1;a) = (Inning(x1;a) + 1) ∈ ℤ)
∧ (Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V)
∧ (Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))
Definitions occuring in Statement :
cs-knowledge: Knowledge(x;a),
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
fpf: a:A fp-> B[a],
Id: Id,
top: Top,
and: P ∧ Q,
product: x:A × B[x],
union: left + right,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-rel-knowledge-inning-step
consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a) ==
(Inning(y1;a) = (Inning(x1;a) + 1))
\mwedge{} (Estimate(y1;a) = Estimate(x1;a))
\mwedge{} (Knowledge(y2;a) = Knowledge(x2;a))
Date html generated:
2015_07_17-AM-11_40_19
Last ObjectModification:
2012_02_25-AM-11_46_06
Home
Index