event-b:是否有可能在一个表达式中通过lambda生成从...到...的素数序列？

Question

我想知道是否有可能在event-b中只生成一个lambda表达式的素数序列.这是我到目前为止:

@axm1 primeSet = {x? x ? 1?100 ? ¬(?y·y < x ? y > 1 ? x mod y = 0)} ? finite(primeSet)
@axm2 primeSeq ? 1?card(primeSet) >->> primeSet
@axm3 ?a,b,c,d·a?b ? primeSeq ? c?d ? primeSeq ? a?b ? c?d ? (a < c ? b < d)

@axm1生成一组素数,@axm2定义序列的类型,并将@axm3此集合进一步约束到确定性解决方案.我不知道怎么用一个lambda表达式来做这个,我不认为它甚至可能,但我想知道其他人的想法.

Answer 1

我相信这个 lambda 函数可以满足您的要求：

\n\n

@axm1 primeSeq = {size\xe2\x86\xa6X| size\xe2\x88\x88\xe2\x84\x95 \xe2\x88\xa7 X\xe2\x8a\x86\xe2\x84\x95 \xe2\x88\xa7 \xe2\x88\x80x\xc2\xb7x\xe2\x88\x88X \xe2\x87\x92 (x\xe2\x88\x881\xe2\x80\xa5size \xe2\x88\xa7 (\xe2\x88\x80y\xc2\xb7y\xe2\x88\x881\xe2\x80\xa5x \xe2\x88\xa7 y\xe2\x89\xa01 \xe2\x88\xa7 y\xe2\x89\xa0x \xe2\x87\x92 x mod y \xe2\x89\xa0 0))}\n

\n