[tlaplus] Using a Division Operator with TLAPS

Hi,

I'm working on proving an algorithm using TLAPS that requires dividing integers by two. I understand there's no support for real numbers/division in the backend provers, so I am using an operator:

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

The problem I'm running into is when trying to prove properties using the above operator with set expressions. The following example demonstrates this:

EXTENDS Integers, TLAPS, FiniteSets

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

CONSTANTS N

VARIABLES x

Init == x = divide_by_two(N)

PositiveInvariant == x >= 0

ASSUME NumberAssumption == N \in {2,4,6,8,10}

THEOREM PositiveDivisionProperty == Init => PositiveInvariant
  <1> SUFFICES ASSUME Init
               PROVE  PositiveInvariant
    OBVIOUS
  <1> QED
    BY NumberAssumption DEF Init, PositiveInvariant, divide_by_two

The backend provers are unable to prove the above theorem. SMT specifically times out and increasing the timeout doesn't appear to help.

Changing the assumption to:

ASSUME NumberAssumption == N = 10

will successfully prove the theorem. Are the backend provers able to work with 'CHOOSE' _expression_ in conjunction with sets? Is there anything wrong with how I'm specifying the assumption? The actual algorithm will require using the division operator with a few 'min'/'max' operators, which may also complicate the proof process, so I'm wondering if TLAPS is able to prove these sort of algorithms that require arithmetic.

Best,

Hans