CLP(FD) labeling on possibly infinite domains

As a follow-up to this SO question, I implemented, for my Prolog-based language Brachylog, my own labeling predicate brachylog_equals/2 which is not guaranteed to terminate but works for infinite domains:

brachylog_equals(Z,Z) :-
    brachylog_equals_('init',10,Z).

brachylog_equals_(I,J,'integer':Z) :-
    fd_inf(Z,'inf'),
    fd_sup(Z,'sup')
    -> (
        (
            I = 'init'
            ;
            I \= 'init',
            abs(Z) #>= I
        ),
        abs(Z) # (
        (
            I = 'init'
            ;
            I \= 'init',
            Z #= -J,
        label([Z])
        ;
        I2 is J,
        J2 is J*10,
        brachylog_equals_(I2,J2,'integer':Z)
    )
    ;
    fd_sup(Z,'sup')
    -> (
        (
            I = 'init'
            ;
            I \= 'init',
            Z #>= I
        ),
        Z #< J,
        label([Z])
        ;
        I2 is J,
        J2 is J*10,
        brachylog_equals_(I2,J2,'integer':Z)
    )
    ;
    label([Z]).

A few notes about this code:

• This predicate is supposed to be used in automatically generated Prolog code, therefore its name does not describe its function but rather follows a convention.

• 'integer':Z rather than simply Z is simply here to comply with the rest of the project (it is used to check easily the type of arguments in some other predicates)

Here are my worries:

• Is this the most idiomatic solution? (i.e. impose a finite bound on the variable where it has an infinite bound, and increase it recursively if backtracking occurs?)

• Is this actually correct in all cases? (From what I tested it is, but I'm wondering if I missed some odd domains where it would break)

• Is this computationally efficient?

Of course comments on code style (which I know does not respect usual conventions) or code simplication are also welcome.

Before discussing correctness, efficiency and alternative approaches, I first have three smaller suggestions to simplify the predicate a bit:

-
Its seems I2 is nowhere really needed, you can always simply use J instead.

-
for J2, I would stick to CLP(FD) constraints like: J2 #= J*10.

-
instead of (\=)/2, I recommend to use dif/2.

These changes make the code a bit easier to read and more uniform, and put us into a better position to discuss the remaining issues.

StackExchange Code Review Q#129924, answer score: 2