# Re: [PVS-Help] Help with (both-sides) strategy

```Hi Sam,

Here are my files:
```

Attachment: SelectorAssignment.pvs
Description: Binary data

Attachment: SelectorAssignment.prf
Description: Binary data

```
It’s with noting that p_Data_Type_Conversion is of type posint8_from_1_to_5, which is defined as:
posint8_from_1_to_5?(n: number): bool = posint8?(n) AND
(1 <= n) AND (n <= 5);
posint8_from_1_to_5: NONEMPTY_TYPE = (posint8_from_1_to_5?)
CONTAINING 1;

Cesar Muñoz has pointed out that if I replace “number” with “real” in my definition, my problem goes away. I still think the FALSE = TRUE issue seems problematic, but by switching all of my definitions of types from using numbers to using reals, I’ve reduced the generated TCCs by more than 20%, so that’s definitely something.

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

> On May 25, 2016, at 3:12 AM, Sam Owre <owre@xxxxxxxxxxx> wrote:
>
> Hi Ben,
>
> I'm having trouble recreating this.  With the spec
>
> -----
> test: THEORY
> BEGIN
> p_Data_Type_Conversion: nat
> f: formula 1 <= p_Data_Type_Conversion => p_Data_Type_Conversion - 1 >= 0
> END test
> -----
>
> I get:
>
> f :
>
>  |-------
> {1}   1 <= p_Data_Type_Conversion IMPLIES p_Data_Type_Conversion - 1 >= 0
>
> Rule? (flatten)
> Applying disjunctive simplification to flatten sequent,
> this simplifies to:
> f :
>
> {-1}  1 <= p_Data_Type_Conversion
>  |-------
> {1}   p_Data_Type_Conversion - 1 >= 0
>
> Rule? (both-sides "+" "1" 1)
> Applying + 1 to both sides of an inequality/equality conjunction,
> this simplifies to:
> f :
>
> [-1]  1 <= p_Data_Type_Conversion
>  |-------
> {1}   p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>
> Rule?
>
> I suspect that the decision procedures have already recorded something in
> your case that is affecting the behavior of both-sides (yours shows that
> you're in the fourth branch of the proof).  Is it possible for you to send
>
> Thanks,
> Sam
>
> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>
>> From: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
>> Date: Mon, 23 May 2016 11:54:20 -0400
>> To: pvs-help@xxxxxxxxxxx
>> Subject: [PVS-Help] Help with (both-sides) strategy
>> Sender: pvs-help-bounces+owre=csl.sri.com@xxxxxxxxxxx
>>
>> I don’t use the (both-sides) strategy very often, so perhaps I’m using it wrong, but I’m not sure what I’m doing
>> wrong in the following:
>> Selector_TCC2.4 :
>>
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> [1] p_Data_Type_Conversion - 1 >= 0
>>
>> Rule? (both-sides "+" "1" 1)
>> Applying + 1 to both sides of an inequality/equality conjunction,
>> this yields 3 subgoals:
>> Selector_TCC2.4.1 :
>>
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>>
>> Rule? (grind)
>> Trying repeated skolemization, instantiation, and if-lifting,
>>
>> This completes the proof of Selector_TCC2.4.1.
>>
>> Selector_TCC2.4.2 :
>>
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> {1} p_Data_Type_Conversion - 1 >= 0 =
>> p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>> [2] p_Data_Type_Conversion - 1 >= 0
>>
>> Rule? (assert)
>> Simplifying, rewriting, and recording with decision procedures,
>> this simplifies to:
>> Selector_TCC2.4.2 :
>>
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> {1} FALSE = TRUE
>> [2] p_Data_Type_Conversion - 1 >= 0
>>
>> At this point, since {1} is clearly false, I’m back to where I started (notwithstanding an additional TCC to prove
>> that real_pred(p_Data_Type_Conversion - 1), which can be proved with (lemma "reals.closed_minus" ("x"
>> "p_Data_Type_Conversion" "y" "1"))).
>>
>> Any idea what I’m doing wrong?
>>
>> And how does:
>> {1} p_Data_Type_Conversion - 1 >= 0 =
>> p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>> get resolved to:
>> {1} FALSE = TRUE
>> upon using (assert)?
>>
>> Best Regards,
>> Ben Hocking
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>

```