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