diff --git a/src/thue_morse3.v b/src/thue_morse3.v index d1c3f26..b28dc9c 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2669,6 +2669,45 @@ Proof. Qed. +Theorem tm_step_palindrome_power2 : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> length a = 2^m + -> 2 < m + -> length (hd ++ a) mod 2^ (pred (Nat.double (Nat.div2 (S m)))) = 0. +Proof. + intros m n hd a tl. intros H I J. + + assert (L: 6 < length a). rewrite I. + assert (2^3 <= 2^m). apply Nat.pow_le_mono_r_iff. + apply Nat.lt_1_2. rewrite Nat.le_succ_l. assumption. + assert (6 < 2^3). simpl. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + apply Nat.lt_0_2. + generalize H0. generalize H1. apply Nat.lt_le_trans. + + assert (E: Nat.Even m \/ Nat.Odd m). apply Nat.Even_or_Odd. + destruct E as [E|E]. + + assert (E' := E). rewrite <- Nat.Odd_succ in E. + apply Nat.Even_Odd_double in E. + apply eq_add_S in E. apply f_equal_pred in E. + rewrite <- E. + apply Nat.Even_Odd_double in E'. rewrite E'. + apply tm_step_palindromic_power2_even with (n := n) (tl := tl). + assumption. assumption. rewrite <- E'. assumption. + + assert (E' := E). rewrite <- Nat.Even_succ in E. + apply Nat.Even_Odd_double in E. + apply f_equal_pred in E. rewrite <- pred_Sn in E. + rewrite <- E. + apply Nat.Even_Odd_double in E'. rewrite E'. + apply tm_step_palindromic_power2_odd with (n := n) (tl := tl). + assumption. assumption. rewrite <- E'. assumption. +Qed. + (* Lemma tm_step_proper_palindrome_center :