Update
This commit is contained in:
parent
7c36b66a21
commit
1fb8dd5022
23
thue-morse.v
23
thue-morse.v
@ -956,12 +956,6 @@ Proof.
|
|||||||
rewrite tm_size_power2. apply Nat.le_add_l.
|
rewrite tm_size_power2. apply Nat.le_add_l.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
|
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
|
||||||
S k < 2^n ->
|
S k < 2^n ->
|
||||||
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
|
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
|
||||||
@ -993,6 +987,23 @@ Proof.
|
|||||||
rewrite L. rewrite M. reflexivity.
|
rewrite L. rewrite M. reflexivity.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
|
||||||
|
S k < 2^n ->
|
||||||
|
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
|
||||||
|
<->
|
||||||
|
nth_error (tm_step (S n)) (k + 2^n)
|
||||||
|
= nth_error (tm_step (S n)) (S k + 2^n).
|
||||||
|
Proof.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
|
Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
|
||||||
S k < 2^n ->
|
S k < 2^n ->
|
||||||
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
|
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
|
||||||
|
Loading…
Reference in New Issue
Block a user