Nuprl Definition : satisfies-int-constraint-problem

xs |= p ==  case p of inl(q) => let eqs,ineqs = q in (∀as∈eqs.xs ⋅ as =0) ∧ (∀bs∈ineqs.xs ⋅ bs ≥0) | inr(_) => False


Definitions occuring in Statement :  satisfies-integer-inequality: xs ⋅ as ≥0,  satisfies-integer-equality: xs ⋅ as =0,  l_all: (∀x∈L.P[x]),  and: P ∧ Q,  false: False,  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  and: P ∧ Q,  satisfies-integer-equality: xs ⋅ as =0,  l_all: (∀x∈L.P[x]),  satisfies-integer-inequality: xs ⋅ as ≥0,  false: False
FDL editor aliases :  sat-icp
Latex:
xs  |=  p  ==
    case  p
      of  inl(q)  =>
      let  eqs,ineqs  =  q 
      in  (\mforall{}as\mmember{}eqs.xs  \mcdot{}  as  =0)  \mwedge{}  (\mforall{}bs\mmember{}ineqs.xs  \mcdot{}  bs  \mgeq{}0)
      |  inr($_{}$)  =>
      False


Date html generated: 2016_05_14-AM-07_17_05
Last ObjectModification: 2015_09_22-PM-05_53_35

Theory : omega


Home Index