Nuprl Definition : consensus-rel-mod

CR(in ws)[x, y]  ==
  ∃a:{a:Id| (a ∈ A)} 
   ((a ∈ ws)
   ∧ (∀b:{a:Id| (a ∈ A)} 
        ((¬(b a ∈ Id))  ((Inning(y;b) Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) Estimate(x;b) ∈ i:ℤ fp-> V))))
   ∧ (((Inning(y;a) (Inning(x;a) 1) ∈ ℤ) ∧ (Estimate(y;a) Estimate(x;a) ∈ i:ℤ fp-> V))
     ∨ ((Inning(y;a) Inning(x;a) ∈ ℤ)
       ∧ (Inning(x;a) ∈ fpf-domain(Estimate(x;a))))
       ∧ (∃v:V
           (state may consider in inning Inning(x;a)
           ∧ (Estimate(y;a) Estimate(x;a) ⊕ Inning(x;a) v ∈ i:ℤ fp-> V))))))



Definitions occuring in Statement :  cs-precondition: state may consider in inning i cs-estimate: Estimate(s;a) cs-inning: Inning(s;a) fpf-single: v fpf-join: f ⊕ g fpf-domain: fpf-domain(f) fpf: a:A fp-> B[a] Id: Id int-deq: IntDeq l_member: (x ∈ l) all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q or: P ∨ Q and: P ∧ Q set: {x:A| B[x]}  add: m natural_number: $n int: equal: t ∈ T
FDL editor aliases :  consensus-rel-mod
CR(in  ws)[x,  y]    ==
    \mexists{}a:\{a:Id|  (a  \mmember{}  A)\} 
      ((a  \mmember{}  ws)
      \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
                ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((Inning(y;b)  =  Inning(x;b))  \mwedge{}  (Estimate(y;b)  =  Estimate(x;b)))))
      \mwedge{}  (((Inning(y;a)  =  (Inning(x;a)  +  1))  \mwedge{}  (Estimate(y;a)  =  Estimate(x;a)))
          \mvee{}  ((Inning(y;a)  =  Inning(x;a))
              \mwedge{}  (\mneg{}(Inning(x;a)  \mmember{}  fpf-domain(Estimate(x;a))))
              \mwedge{}  (\mexists{}v:V
                      (state  x  may  consider  v  in  inning  Inning(x;a)
                      \mwedge{}  (Estimate(y;a)  =  Estimate(x;a)  \moplus{}  Inning(x;a)  :  v))))))



Date html generated: 2015_07_17-AM-11_26_20
Last ObjectModification: 2012_02_25-AM-11_42_16

Home Index