Функция isPrime с TLA +

Этот вопрос касается TLA + с использованием набора инструментов (https://github.com/tlaplus/tlaplus/releases) Мне не удалось найти ни одной отметки об этом. Извини за это. Вот почему я выбрал только простые числа. Если мне чего-то не хватает, пожалуйста, добавьте лучшие теги или создайте недостающие.

Вот в чем проблема

Есть хорошо известная функция и алгоритм для НОД. Вот.

------------------ MODULE Euclid -------------------------------
EXTENDS Naturals, TLC
CONSTANT K
Divides(i,j) == \E k \in 0..j: j = i * k
IsGCD(i,j,k) ==
    Divides(i,j)
    /\ Divides(i,k)
    /\ \A r \in 0..j \cup 0..k :
        (Divides(r,j ) /\ Divides(r,k)) => Divides(r,i)
    (* --algorithm EuclidSedgewick
    {
        variables m \in 1..K, n \in 1..m, u = m, v = n;
        {
            L1: while (u # 0) {
            if (u < v) { u := v || v := u };
            L2: u := u - v
            };
            assert IsGCD(v, m, n)
        }
    }
    *)

Это хорошо известное решение, которое работает.

Теперь я пытаюсь написать функцию isPrime, используя эту. Но я считаю, что делаю неправильно. Я хотел бы знать, есть ли у вас идеи.

isPrime(nb) ==
        \E k \in 2..nb: isGCD(nb,k,1) \/ isGCD(nb,k,nb)

Спасибо