Update
This commit is contained in:
parent
dc91289017
commit
ccc12a619c
|
@ -1378,9 +1378,7 @@ Proof.
|
||||||
rewrite tm_size_power2. apply lt_split_bits.
|
rewrite tm_size_power2. apply lt_split_bits.
|
||||||
assumption. assumption. assumption.
|
assumption. assumption. assumption.
|
||||||
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
||||||
rewrite tm_build. rewrite nth_error_app2. rewrite tm_size_power2.
|
rewrite tm_step_single_bit_index. reflexivity.
|
||||||
rewrite Nat.sub_diag. rewrite tm_step_head_1. simpl. reflexivity.
|
|
||||||
rewrite tm_size_power2. apply Nat.le_refl.
|
|
||||||
apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
|
apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
|
||||||
rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r.
|
rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r.
|
||||||
apply Nat.lt_1_2.
|
apply Nat.lt_1_2.
|
||||||
|
|
Loading…
Reference in New Issue
Block a user