Dafny递归触发器调试：整数抽象幂定义的验证困境

我正在为所有整数扩展抽象幂（apow）的定义，尽管已经设置了触发器，但仍陷入递归触发器引发的无限验证循环。目前只能通过任务管理器观察Z3是否占用大量内存，希望能找到更高效的递归触发器调试方法，避免盲目试错。

相关代码如下：

function apow<A>(g: Group, elem: A, n: int): A
    decreases n*n
    ensures n == 0 ==> apow(g,elem,n) == g.identity
{
    if n == 0 then g.identity else if n > 0 then g.compose(elem, apow(g, elem, n-1)) else if n < 0 then g.compose(g.inverse(elem), apow(g, elem, n+1)) else g.identity
}

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

lemma allApowClosed<A>(g: Group, elem: A) 
    requires ValidGroup(g)
    requires elem in g.elements
    ensures forall x: int :: apow(g, elem, x) in g.elements
{
    reveal apow();
    forall x: int {
        apowClosed(g, elem, x);
    }
}

lemma {:verify true} apowAdditionInt<A>(g: Group<A>, elem: A, n: int, k: int)
    requires elem in g.elements
    // requires ValidGroup(g)
    requires closedComposition(g)
    requires closedInverse(g)
    requires g.identity in g.elements
    requires isIdentity(g);
    requires associativeComposition(g)
    ensures g.compose(apow(g, elem, n), apow(g, elem, k)) == apow(g, elem, n+k)
{
    allApowClosed(g, elem);
    if k == 0 {
        assert apow(g, elem, k) == g.identity;
        assert g.compose(apow(g, elem, n), g.identity) == apow(g, elem, n+k);
    }else if n == 0 {
        assert apow(g, elem, n) == g.identity;
        assert g.compose(g.identity, apow(g, elem, k)) == apow(g, elem, n+k);
    }else if n > 0 && n+k > k {
        apowPos(g, elem, n);
        apowPos(g, elem, n+k);
        assert apow(g, elem, n-1) in g.elements;
        assert apow(g, elem, k) in g.elements;
        assert apow(g, elem, n+k) in g.elements;
        // assume g.compose(elem, g.compose(apow(g, elem, n-1), apow(g, elem, k))) == g.compose(elem, apow(g, elem, n-1+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)));
            == {apowAdditionInt(g,elem, n-1,k);}
            g.compose(elem, apow(g, elem, n-1+k));
            // apow(g, elem, n+k);
        }
    }else{

    }
}

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

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 closedInverse<A>(g: Group<A>) {
forall x {:trigger g.inverse(x)} :: x in g.elements ==> g.inverse(x) in g.elements
}

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
}

内容的提问来源于stack exchange，提问作者Hath995