Дафное заявление о существовании вызывает медлительность?

apowAddition проверяет, когда я комментирую containsInverses(g) в моем определении допустимой алгебры теории групп, но когда я раскомментирую, проверка не выполняется, смерть по тайм-ауту. Я могу предположить, что Дафни пытается создать элементы, которые соответствуют определению. Однако, поскольку я не использую это свойство в доказательстве и не обеспечиваю его выполнение леммой, почему оно вызывает проблемы в доказательстве?

datatype Group<!A> = Group(elements: set<A>, identity: A, compose: (A,A) -> A)

predicate ValidGroup<A>(g: Group<A>) {
    g.identity in g.elements &&
    isIdentity(g) &&
    closedComposition(g) &&
    associativeComposition(g) //&& 
    // containsInverses(g)
}
function apow<A>(g: Group, elem: A, n: nat): A 
    requires elem in g.elements
{
    if n == 0 then g.identity else g.compose(elem, apow(g, elem, n-1))
}


lemma {:verify true} apowAddition<A>(g: Group<A>, elem: A, n: nat, k: nat)
    requires elem in g.elements
    requires ValidGroup(g)
    ensures g.compose(apow(g, elem, n), apow(g, elem, k)) == apow(g, elem, n+k)
{
    apowClosed(g, elem, n);
    apowClosed(g, elem, k);
    if k == 0 {
        assert apow(g, elem, k) == g.identity;
        assert g.compose(apow(g, elem, n), g.identity) == apow(g, elem, n+0);
    }else if n == 0 {
        assert apow(g, elem, n) == g.identity;
        assert g.compose(g.identity, apow(g, elem, k)) == apow(g, elem, k+0);
    }else{
        apowClosed(g, elem, n-1);
        apowClosed(g, elem, n+k);
        calc {
            g.compose(apow(g, elem, n), apow(g, elem, k));
            g.compose(g.compose(elem, apow(g, elem, n-1)), apow(g, elem, k));
            g.compose(elem, g.compose(apow(g, elem, n-1), apow(g, elem, k)));
            == {apowAddition(g,elem, n-1,k);}
            g.compose(elem, apow(g, elem, n-1+k));
            apow(g, elem, n+k);
        }
    }
}

predicate isIdentity<A>(g: Group<A>) {
    forall a :: a in g.elements ==> g.compose(a,g.identity) == a && g.compose(g.identity, a) == a
}

predicate closedComposition<A>(g: Group<A>) {
    forall x,y :: x in g.elements && y in g.elements ==> g.compose(x,y) in g.elements
}

predicate associativeComposition<A>(g: Group<A>) {
    forall a,b,c :: a in g.elements && b in g.elements && c in g.elements ==> g.compose(g.compose(a,b),c) == g.compose(a, g.compose(b,c))
}

predicate containsInverses<A>(g: Group<A>) {
    forall x :: x in g.elements ==> exists xbar :: xbar in g.elements && g.compose(x,xbar) == g.identity
}

lemma apowClosed<A>(g: Group, elem: A, n: nat)
    requires elem in g.elements
    requires g.identity in g.elements
    requires isIdentity(g)
    requires closedComposition(g)
    ensures apow(g,elem, n) in g.elements
{}

Редактировать 2: добавление правильной инверсии к isInverse быстро проверяет groupCompositionInverse, но apowAddition снова бесконечно проверяет. Изменить 3: добавление apowClosed(g, elem, n+k) в apowAddition все исправляет!

predicate isInverse<A>(g: Group<A>) {
  forall x {:trigger g.inverse(x)} :: x in g.elements ==> g.compose(x,g.inverse(x)) == g.identity && g.compose(g.inverse(x),x) == g.identity
}
lemma {:verify true} groupCompositionInverse<A>(g: Group<A>, a: A, b: A, abar: A, bbar: A, abbar: A)
    requires ValidGroup(g)
    requires a in g.elements
    requires b in g.elements
    // requires containsInverses(g)
    // requires abar in g.elements
    // requires bbar in g.elements
    // requires abbar in g.elements
    requires g.inverse(a) == abar
    requires g.inverse(b) == bbar
    requires g.inverse(g.compose(a,b)) == abbar
    // requires g.compose(a, abar) == g.identity
    // requires g.compose(b, bbar) == g.identity
    // requires g.compose(g.compose(a, b), abbar) == g.identity
    ensures abbar == g.compose(bbar, abar)
{
    calc {
        g.compose(g.compose(a, b), g.compose(bbar, abar));
        ==
        g.compose(a, g.compose(g.compose(b, bbar),abar));
        ==
        g.compose(a, g.compose(g.identity,abar));
        ==
        g.compose(a, abar);
        ==
        g.identity;
    }
}