def m5(u, x):
    return x + 5 * u

def d5(u, index_structure, y):
    return y - index_structure

def get_index_structure(u):
    return u * 5

def example(u, x):
    assert d5(u, get_index_structure(u), m5(u, x)) == x



Y = m5(U, X), Z = d5(U, _, Y) :- Z = X.

Y = abs(X), Z = abs(Y) :- Z = Y.



declare_rule(m5, [1, 2], d5, [1, 3, 0], 2)
declare_rule(abs, [1], abs, [0], 0)
declare_rule(operator.neg, [1], abs, [0], 0)


declare_rule(rbigint.add, [1, 2], rbigint.sub, [0, 2], 1)
declare_rule(rbigint.add, [2, 1], rbigint.sub, [0, 2], 1)