Update
This commit is contained in:
parent
b64c29e8a0
commit
443008fbb5
10
thue-morse.v
10
thue-morse.v
|
@ -384,13 +384,6 @@ Proof.
|
||||||
rewrite rev_length. assumption. apply rev_involutive. assumption.
|
rewrite rev_length. assumption. apply rev_involutive. assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
|
|
||||||
l = l1 ++ b :: l2 -> length l1 < length l.
|
|
||||||
Proof.
|
|
||||||
intros l l1 l2 b. intro H. rewrite H.
|
|
||||||
rewrite app_length. simpl. apply Nat.lt_add_pos_r.
|
|
||||||
apply Nat.lt_0_succ.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma tm_step_next_range :
|
Lemma tm_step_next_range :
|
||||||
forall (n k : nat) (b : bool),
|
forall (n k : nat) (b : bool),
|
||||||
|
@ -399,7 +392,8 @@ Proof.
|
||||||
intros n k b. intro H. assert (I := H).
|
intros n k b. intro H. assert (I := H).
|
||||||
apply nth_error_split in H. destruct H. destruct H. inversion H.
|
apply nth_error_split in H. destruct H. destruct H. inversion H.
|
||||||
rewrite tm_build. rewrite nth_error_app1. apply I.
|
rewrite tm_build. rewrite nth_error_app1. apply I.
|
||||||
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
|
rewrite H0. rewrite app_length. rewrite <- H1. simpl.
|
||||||
|
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma tm_step_add_range : forall (n m k : nat),
|
Lemma tm_step_add_range : forall (n m k : nat),
|
||||||
|
|
Loading…
Reference in New Issue
Block a user