Size

Statistics

Metric	Count
Definitions	0
Theorems `lt_size`, `lt_size_self`, `shiftLeft'_ne_zero_left`, `shiftLeft'_true_eq_mul_pow`, `shiftLeft'_true_ne_zero`, `shiftLeft'_tt_eq_mul_pow`, `shiftLeft'_tt_ne_zero`, `shiftLeft_eq_mul_pow`, `size_bit`, `size_eq_bits_len`, `size_eq_zero`, `size_le`, `size_le_size`, `size_one`, `size_pos`, `size_pow`, `size_shiftLeft`, `size_shiftLeft'`, `size_zero`	19
Total	19

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_size` 📖	mathematical	—	`size`	—	`size_le`
`lt_size_self` 📖	mathematical	—	`size`	—	`size_bit` `bit_ne_zero_iff` `bit_lt_two_pow_succ_iff`
`shiftLeft'_ne_zero_left` 📖	—	—	—	—	—
`shiftLeft'_true_eq_mul_pow` 📖	mathematical	—	`shiftLeft'`	—	`shiftLeft'.eq_2` `bit_val`
`shiftLeft'_true_ne_zero` 📖	—	—	—	—	—
`shiftLeft'_tt_eq_mul_pow` 📖	mathematical	—	`shiftLeft'`	—	`shiftLeft'_true_eq_mul_pow`
`shiftLeft'_tt_ne_zero` 📖	—	—	—	—	`shiftLeft'_true_ne_zero`
`shiftLeft_eq_mul_pow` 📖	—	—	—	—	—
`size_bit` 📖	mathematical	—	`size` `bit`	—	`binaryRec_eq` `bit_ne_zero_iff`
`size_eq_bits_len` 📖	mathematical	—	`bits` `size`	—	`zero_bits` `size_bit` `bits_append_bit`
`size_eq_zero` 📖	mathematical	—	`size`	—	`size_pos`
`size_le` 📖	mathematical	—	`size`	—	`lt_size_self` `size_bit` `bit_ne_zero_iff` `bit_lt_two_pow_succ_iff`
`size_le_size` 📖	mathematical	—	`size`	—	`size_le` `lt_size_self`
`size_one` 📖	mathematical	—	`size`	—	—
`size_pos` 📖	mathematical	—	`size`	—	`lt_size`
`size_pow` 📖	mathematical	—	`size`	—	`size_shiftLeft`
`size_shiftLeft` 📖	mathematical	—	`size`	—	`size_shiftLeft'` `shiftLeft'_ne_zero_left`
`size_shiftLeft'` 📖	mathematical	—	`size` `shiftLeft'`	—	`size_bit` `shiftLeft'_true_eq_mul_pow`
`size_zero` 📖	mathematical	—	`size`	—	—

---