Re: TLAPS and string search algorithms

[Y2i <yur...@xxxxxxxxx>]

Andrew, would quantification over tuple domain be useful for your project?

\A i \in DOMAIN(<<1,2,3,4,5>>) : i < 6

On Tuesday, May 19, 2015 at 11:25:48 AM UTC-7, Andrew Helwer wrote:

As a fun side-project with TLAPS, I'd like to prove correctness of some string search algorithms. However, TLAPS says it doesn't support quantification over tuples and set constructors. Would this affect ability to prove things about strings (which I guess are represented by sequences of characters)?