[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Help with (both-sides) strategy*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Mon, 23 May 2016 11:54:20 -0400*Authentication-results*: symauth.service.identifier*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=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)? |

**Follow-Ups**:**Re: [PVS-Help] Help with (both-sides) strategy***From:*Sam Owre

**Re: [PVS-Help] Help with (both-sides) strategy***From:*Ben Hocking

- Prev by Date:
**Re: [PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand*** - Next by Date:
**Re: [PVS-Help] Help with (both-sides) strategy** - Previous by thread:
**[PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand*** - Next by thread:
**Re: [PVS-Help] Help with (both-sides) strategy** - Index(es):