# [Why3-club] A predicate that cannot be proved by why3

```Dear Why3 Club,

I have a why3 script that I think is relatively simple but why3 cannot
prove it.  I wander if I did anything wrong.```
```
*constant X : (map int int)*

*context:
*

*  X[4] = X[6] && X[5] = X[6] && X[6] < X[7]
*

*predicate:
*

*  exists k : int.  0 <= k && k <= 3 && not(X[k+4] = X[k+5])*

It is obvious that there exists such a k = 2.   If I modify the predicate a
lilltle bit to :

*predicate:
*

*  exists k : int.  0 <= k && k <= 3 && k = 2 && not(X[k+4] = X[k+5])*

why3 then has no problem to prove it.  So I'm confused that why why3 cannot
prove the original case.

Thanks,
Ziqing Luo
University of Delaware

The following is the whole why3 script:

theory Why3Query_408

use import int.Int

use import map.Map

constant _X : (map int int)

(*

context:

X[4] = X[6]

X[5] = X[6]

X[6] < X[7]

predicate:

exists k : int.  0 <= k && k <= 3 && not(X[k+4] = X[k+5])

*)

predicate context = (((0)  =  ((get _X (4))  +  ((-1)  *  (get _X (6)))))
&&

((0)  =  ((get _X (5))  +  ((-1)  *  (get _X (6)))))  &&

(((get _X (6))  +  ((-1)  *  (get _X (7)))  +  (1))
<=  (0)))

goal G0: context -> ((exists k : int. (((k  +  (-3))  <=  (0))  &&  ((0)
<=  k)  &&

(not ((0)  =  ((get _X (k  +  (4)))  +  ((-1)  *
(get _X (k  +  (5))))))))) )

end
```
```_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
```