Update
This commit is contained in:
parent
b0e15fc10a
commit
a8cdd31830
12
thue-morse.v
12
thue-morse.v
@ -835,13 +835,11 @@ Lemma tm_step_single_bit_index : forall (n : nat),
|
|||||||
nth_error (tm_step (S n)) (2^n) = Some true.
|
nth_error (tm_step (S n)) (2^n) = Some true.
|
||||||
Proof.
|
Proof.
|
||||||
intros n.
|
intros n.
|
||||||
induction n.
|
rewrite tm_build.
|
||||||
- simpl. reflexivity.
|
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
|
||||||
- rewrite tm_build.
|
replace (true) with (negb false). apply map_nth_error.
|
||||||
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
|
rewrite tm_step_head_1. simpl. reflexivity.
|
||||||
replace (true) with (negb false). apply map_nth_error.
|
reflexivity. rewrite tm_size_power2. easy.
|
||||||
rewrite tm_step_head_1. simpl. reflexivity.
|
|
||||||
reflexivity. rewrite tm_size_power2. easy.
|
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma tm_step_repunit_index : forall (n : nat),
|
Lemma tm_step_repunit_index : forall (n : nat),
|
||||||
|
Loading…
Reference in New Issue
Block a user