AllBits(b,c,l)

Hygienic expanded first-order definition

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))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Definitions depending on this notation

Checked theorems using this definition