Nuprl Definition : q-sat-constraints
q-sat-constraints(k;A;y) ==
(||y|| = k ∈ ℤ)
c∧ (∀a∈A.let F,r,G = a in
if (r =z 0) then q-linear(k;j.F[j]?0;y) = q-linear(k;j.G[j]?0;y) ∈ ℚ
if (r =z 1) then q-linear(k;j.F[j]?0;y) ≤ q-linear(k;j.G[j]?0;y)
else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
fi )
Definitions occuring in Statement :
select?: as[i]?a,
q-linear: q-linear(k;i.X[i];y),
qle: r ≤ s,
qless: r < s,
rationals: ℚ,
l_all: (∀x∈L.P[x]),
length: ||as||,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
spreadn: spread3,
cand: A c∧ B,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
cand: A c∧ B,
int: ℤ,
length: ||as||,
l_all: (∀x∈L.P[x]),
spreadn: spread3,
equal: s = t ∈ T,
rationals: ℚ,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
qle: r ≤ s,
qless: r < s,
q-linear: q-linear(k;i.X[i];y),
select?: as[i]?a,
natural_number: $n
FDL editor aliases :
q-sat-constraints
Latex:
q-sat-constraints(k;A;y) ==
(||y|| = k)
c\mwedge{} (\mforall{}a\mmember{}A.let F,r,G = a in
if (r =\msubz{} 0) then q-linear(k;j.F[j]?0;y) = q-linear(k;j.G[j]?0;y)
if (r =\msubz{} 1) then q-linear(k;j.F[j]?0;y) \mleq{} q-linear(k;j.G[j]?0;y)
else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
fi )
Date html generated:
2016_05_15-PM-11_31_21
Last ObjectModification:
2015_09_23-AM-08_29_57
Theory : rationals
Home
Index