Sequences involving increments or decrements on indices

[andrewjkennedy]

I want to write something like

P0 |- P1
...
Pn-1 |- Pn

P0 |- Pn

But this is rejected, as is the equivalent comprehension form:

</ Pi-1 |- Pi // i IN 1 ... n />

P0 |- Pn

[PeterSewell]

Ott doesn't understand any index arithmetic, I'm afraid. One might workaround with a metaproduction, defining it in the prover backend, or in in-line prover code in premises. Or with a binary transitive closure?

…

On 21 February 2018 at 14:53, Andrew Kennedy ***@***.***> wrote: I want to write something like P0 |- P1 ... Pn-1 |- Pn P0 |- Pn But this is rejected, as is the equivalent comprehension form: </ Pi-1 |- Pi // i IN 1 ... n /> P0 |- Pn — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#31>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5idvNFUdYzjPDf3oI2FB8prq-BECks5tXC3NgaJpZM4SNxAa> .