Update
This commit is contained in:
parent
2099d9f563
commit
ec0ce5c4c9
21
thue-morse.v
21
thue-morse.v
@ -807,19 +807,19 @@ Proof.
|
|||||||
rewrite H2. apply Nat.le_add_r.
|
rewrite H2. apply Nat.le_add_r.
|
||||||
rewrite tm_morphism_length in H3.
|
rewrite tm_morphism_length in H3.
|
||||||
|
|
||||||
destruct J. destruct H0; destruct H0.
|
assert (H4: Nat.div2 (length hd) <= length l).
|
||||||
|
|
||||||
assert (L: length hd = length hd). reflexivity.
|
|
||||||
rewrite H0 in L at 2. rewrite app_length in L.
|
|
||||||
rewrite tm_morphism_length in L.
|
|
||||||
|
|
||||||
assert (Nat.div2 (length hd) <= length l).
|
|
||||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||||
rewrite <- Nat.add_0_r at 1.
|
rewrite <- Nat.add_0_r at 1.
|
||||||
replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
|
replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
|
||||||
rewrite <- Nat.div2_odd. assumption.
|
rewrite <- Nat.div2_odd. assumption.
|
||||||
rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.
|
rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.
|
||||||
|
|
||||||
|
destruct J. destruct H0; destruct H0.
|
||||||
|
|
||||||
|
assert (L: length hd = length hd). reflexivity.
|
||||||
|
rewrite H0 in L at 2. rewrite app_length in L.
|
||||||
|
rewrite tm_morphism_length in L.
|
||||||
|
|
||||||
apply firstn_length_le in H4. rewrite H4 in L.
|
apply firstn_length_le in H4. rewrite H4 in L.
|
||||||
replace (2 * Nat.div2 (length hd))
|
replace (2 * Nat.div2 (length hd))
|
||||||
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
|
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
|
||||||
@ -836,13 +836,6 @@ Proof.
|
|||||||
reflexivity. rewrite H0 in L at 2. rewrite app_length in L.
|
reflexivity. rewrite H0 in L at 2. rewrite app_length in L.
|
||||||
rewrite tm_morphism_length in L.
|
rewrite tm_morphism_length in L.
|
||||||
|
|
||||||
assert (Nat.div2 (length hd) <= length l).
|
|
||||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
|
||||||
rewrite <- Nat.add_0_r at 1.
|
|
||||||
replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
|
|
||||||
rewrite <- Nat.div2_odd. assumption.
|
|
||||||
rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.
|
|
||||||
|
|
||||||
apply firstn_length_le in H4. rewrite H4 in L.
|
apply firstn_length_le in H4. rewrite H4 in L.
|
||||||
replace (2 * Nat.div2 (length hd))
|
replace (2 * Nat.div2 (length hd))
|
||||||
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
|
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
|
||||||
|
Loading…
Reference in New Issue
Block a user