MATLAB: ERROR IN ISALWAYS : UNABLE TO PROVE

assumeassumptionsisalwayspositiverestrictionssymbol [~]

Hi,
I would like to see if
2/(g - d + 2*r + 1) - 4 >= 0
with some restrictions.
Hence, I am trying to use
isAlways(2/(g - d + 2*r + 1) - 4 >= 0 & r>=1 
            & g>=1 & d>=1 & r+g-d>=0 
            & nchoosek(r+2,2) >= 1+2*d-g 
            & g-(r+1)*(r+g-d)-(nchoosek(r+2,2)-2*d+g)>=0 
            & N == nchoosek(r+2,2)-2*d+g);
Where N is a value that I enter by computer at the beginning.
MatLab returns 
Warning: Unable to prove '1 == g - 2*d + nchoosek(r + 2, 2) & 0 <= 2*d - (r + 1)*(g - d + r) - nchoosek(r + 2, 2) & 0 <= g -
d + r & 2*d - g + 1 <= nchoosek(r + 2, 2) & 1 <= d & 1 <= g & 1 <= r & 0 <= 2/(g - d + 2*r + 1) - 4'. 
> In symengine
  In sym/isAlways (line 38)
  In partitions1 (line 38)
r,g,d are symbolic variables.
WHY DO THIS HAPPEN? CAN ANYONE HELP ME?

Best Answer

Within isAlways those relations you have do not form restrictions, they form tests. The isAlways(A&B&C) semantics is not "is A always true under the conditions B and C: the semantics is "Are A and B and C always simultaneously true?"
If you want to test whether A is always true under conditions B and C then you would assume(B&C); isAlways(A)
Also, isAlways(A) has three possibilities:
  1. the engine is able to prove that A is true under all conditions taking into account assumptions .
  2. the engine is able to decisively prove there is a contradiction to the assumptions
  3. the engine finds a combination of conditions that involve variables that are not completely pinned down by assumptions, that could be true or false depending on the values of the variables . There is not enough information to prove or disprove the system . This case generates the error message you saw unless you pass isAlways the option telling it which way to answer .
The option permits you to use isAlways as either "can you prove this is definitely true ?" or "can you definitely disprove this?" but without the option the "not enough information" resolution generates the error you saw.
Related Question