Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project!

## existential quantification and congruence

Help
2013-11-03
2013-11-05

• Leonid Ryzhyk
2013-11-03

When running Reduce on the following input:

```load redlog;
rlset pasf;
phi := ex(x, cong(x+1, z, 16));
rlqe (phi);
```

I obtain this result:

```15*z + 14 ~16~ 0 or 15*z + 13 ~16~ 0 or 15*z + 11 ~16~ 0 or 15*z + 8 ~16~ 0
or 15*z + 7 ~16~ 0 or 15*z + 4 ~16~ 0 or 15*z + 2 ~16~ 0 or 15*z + 1 ~16~ 0
or 5*z + 4 ~16~ 0 or 5*z + 3 ~16~ 0 or 5*z + 2 ~16~ 0 or 5*z + 1 ~16~ 0
or 3*z + 2 ~16~ 0 or 3*z + 1 ~16~ 0 or z + 1 ~16~ 0 or z ~16~ 0
```

which is obviously correct; however I was hoping that Redlog would be able to simplify it all the way to "true". Is there a way to achieve this, e.g., by using a different encoding of the problem?

Thanks!
Leonid

• Thomas Sturm
2013-11-04

Unfortunately, the simplifier is not very good.

If you suspect that it is true, you can directly ask for it, like:

rlqe all(z, phi);

More conveniently you could go

rlqe rlall phi;

where rlall() is the universal closure, i.e. all remaining variables are universally quantified.

Best,

Thomas

• Leonid Ryzhyk
2013-11-05

Thanks for the explanation!

Leonid