Update
This commit is contained in:
parent
065a7df946
commit
354a87fddc
13
thue-morse.v
13
thue-morse.v
@ -1152,14 +1152,11 @@ Proof.
|
|||||||
rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2.
|
rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2.
|
||||||
|
|
||||||
assert (forall a b, option_map negb a = option_map negb b <-> a = b).
|
assert (forall a b, option_map negb a = option_map negb b <-> a = b).
|
||||||
intros a b. destruct a. destruct b. destruct b0. destruct b.
|
intros a b. destruct a. destruct b. destruct b0.
|
||||||
simpl. split. intro. reflexivity. intro. reflexivity.
|
destruct b; simpl. split; intro; reflexivity. split; intro; inversion H2.
|
||||||
simpl. split. intro. inversion H2. intro. inversion H2.
|
destruct b; simpl. split; intro; inversion H2. split; intro; reflexivity.
|
||||||
destruct b. simpl. split. intro. inversion H2. intro. inversion H2.
|
split; intro; inversion H2.
|
||||||
simpl. split. intro. reflexivity. intro. reflexivity.
|
destruct b. split; intro; inversion H2. split; intro; reflexivity.
|
||||||
split. intro. inversion H2. intro. inversion H2.
|
|
||||||
destruct b. split. intro. inversion H2. intro. inversion H2.
|
|
||||||
split. intro. reflexivity. intro. reflexivity.
|
|
||||||
|
|
||||||
replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i).
|
replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i).
|
||||||
replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j).
|
replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j).
|
||||||
|
Loading…
Reference in New Issue
Block a user