Readable signature
AllBits(b,c,l)Exact expansion
forall ff_i_defined_all_bits. (exists ff_lt_defined_all_bits_bound. ff_lt_defined_all_bits_bound + S ff_i_defined_all_bits = l) -> exists ff_bit_defined_all_bits. ((((exists ff_h_defined_all_bits_decoded. ff_h_defined_all_bits_decoded + S (ff_bit_defined_all_bits) = S ((S (ff_i_defined_all_bits)) * c)) /\ exists ff_q_defined_all_bits_decoded. b = ff_q_defined_all_bits_decoded * S ((S (ff_i_defined_all_bits)) * c) + (ff_bit_defined_all_bits))) /\ (ff_bit_defined_all_bits = 0 \/ ff_bit_defined_all_bits = 1))This node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.