Update
This commit is contained in:
parent
354a87fddc
commit
787dab1159
12
thue-morse.v
12
thue-morse.v
@ -1152,9 +1152,9 @@ 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.
|
intros a b. destruct a. destruct b. destruct b0; destruct b; simpl.
|
||||||
destruct b; simpl. split; intro; reflexivity. split; intro; inversion H2.
|
split; intro; reflexivity. split; intro; inversion H2.
|
||||||
destruct b; simpl. split; intro; inversion H2. split; intro; reflexivity.
|
split; intro; inversion H2. split; intro; reflexivity.
|
||||||
split; intro; inversion H2.
|
split; intro; inversion H2.
|
||||||
destruct b. split; intro; inversion H2. split; intro; reflexivity.
|
destruct b. split; intro; inversion H2. split; intro; reflexivity.
|
||||||
|
|
||||||
@ -1253,11 +1253,9 @@ Proof.
|
|||||||
|
|
||||||
destruct (nth_error (tm_step n) (k * 2 ^ m)).
|
destruct (nth_error (tm_step n) (k * 2 ^ m)).
|
||||||
destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)).
|
destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)).
|
||||||
destruct b. destruct b0.
|
destruct b; destruct b0; destruct H0.
|
||||||
destruct H0.
|
|
||||||
assert (Some true = Some true). reflexivity.
|
assert (Some true = Some true). reflexivity.
|
||||||
apply H1 in H2. rewrite <- H2 at 1. easy. easy.
|
apply H1 in H2. rewrite <- H2 at 1. easy. easy. easy.
|
||||||
destruct b0. easy. destruct H0.
|
|
||||||
assert (Some false = Some false). reflexivity.
|
assert (Some false = Some false). reflexivity.
|
||||||
apply H1 in H2. rewrite H2 at 1. easy. easy.
|
apply H1 in H2. rewrite H2 at 1. easy. easy.
|
||||||
rewrite nth_error_nth' with (d := false). easy.
|
rewrite nth_error_nth' with (d := false). easy.
|
||||||
|
Loading…
Reference in New Issue
Block a user