Given the goal:
?- w2n (a: word4) + w2n (b: word4) < 32
gives the new goal
e (wordsLib.n2w_INTRO_TAC 6)
This goal can be solved using blastLib.BBLAST_TAC. Any word length strictly greater than five would have sufficed here; it is generally best to pick as small a word size as is necessary.
[ w2n a < 16, w2n b < 16 ] ?- w2w a + w2w b <+ 32w