../../Task/Binary-digits/ACL2