Dafny recursive trigger debugging

Question

Following up from a previous question here. I'm trying to extend my definition of an abstract power for all integers.

I thought I setup the triggers correctly but I'm still running into recursive triggers endlessly verifying. Is there a better way to debug recursive triggers than just guessing and checking? I basically sit there with task manager open seeing if z3 is eating all the memory. I hope there is a way to get better visibility about what is happening.

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{

        }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
    }