Update
This commit is contained in:
parent
ccc12a619c
commit
1ea4f6d502
@ -1335,10 +1335,7 @@ Proof.
|
|||||||
rewrite tm_size_power2. assumption.
|
rewrite tm_size_power2. assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Theorem tm_step_flip_low_bit :
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_flip_low_bit :
|
|
||||||
forall (n m k j : nat),
|
forall (n m k j : nat),
|
||||||
0 < k -> j < m -> k * 2^m < 2^n
|
0 < k -> j < m -> k * 2^m < 2^n
|
||||||
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
|
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
|
||||||
|
Loading…
Reference in New Issue
Block a user