# Using Resolve and ForAll to prove takes a really long time

I've been trying to prove a lemma for my paper using Mathematica... basically that

$$\forall \{n, d_i, d_j\} \in \mathbb{Z},\ n \ge d_i > d_j \ge 2$$

it's true that

$$V[1, n, d_i-1, d_j-1] > 0 \Longrightarrow V[1, n, d_i, d_j] > 0$$

When I manually plug in different values for $n$ (500, in this example), all return true:

Resolve[ForAll[{di, dj},
di ∈ Integers && dj ∈ Integers && 500 >= di > dj >= 2,
Implies[V[1, 500, di - 1, dj - 1] > 0, V[1, 500, di, dj] > 0]]]


But when I do

Resolve[ForAll[{n, di, dj},
n ∈ Integers && di ∈ Integers &&
dj ∈ Integers && n >= di > dj >= 1,
Implies[V[1, n, di - 1, dj - 1] > 0, V[1, n, di, dj] > 0]], Reals]


Then it takes forever (as in I've never been able to get it to spit out the result) to run.

For those who are interested, here's my full code.

V[amg_,n_,di_,dj_] = amg^2 (-((1 + 2 dj)/(7 + 5 dj + n + 2 dj n)) - (1 - 2 di)^2/(2 - n + di (5 + 2 n))^2 + (4 (2 + di)^2)/(7 + n + di (5 + 2 n))^2 + (-1 + 2 dj)/(2 - n + dj (5 + 2 n)))

(*this works*)
Resolve[ForAll[{di, dj}, di ∈ Integers && dj ∈ Integers && 500 >= di > dj >= 2, Implies[V[1, 500, di - 1, dj - 1] > 0, V[1, 500, di, dj] > 0]]]

(*this doesn't*)
Resolve[ForAll[{n, di, dj}, n ∈ Integers && di ∈ Integers && dj ∈ Integers && n >= di > dj >= 1, Implies[V[1, n, di - 1, dj - 1] > 0, V[1, n, di, dj] > 0]], Reals]


Thanks rm -rf. The function you suggested sure looks interesting. I played around with my code a bit. Apparently the domain plays a huge role. I changed it to

Resolve[ForAll[{n, di, dj}, n >= di >= 2 && n >= dj >= 2, Implies[V[1, n, di - 1, dj - 1] > 0, V[1, n, di, dj] > 0]], Reals]


and now it's working >.< even though the domain is larger than before.

• I'm not surprised that the unbounded Resolve[...] line takes forever to run, especially in non-trivial cases, but I don't know anything about this subject to suggest something better. That said, either you or someone else could perhaps fiddle with the undocumented EquationalLogicProve` and friends... seems like it's a good fit for this problem (but zero documentation). See this question and MattW-D's answer for more. – rm -rf Feb 1 '13 at 0:18