diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 7eb5e4c..b7d32c0 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2535,7 +2535,26 @@ Proof. Qed. +Lemma tm_step_palindromic_power2_odd_beta : + forall (m n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(S (Nat.double m)) + -> length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0 + \/ 2^5 <= length a. +Proof. + intros m n hd a tl. intros H I J. + destruct m. rewrite J in I. inversion I. inversion H1. inversion H3. + + destruct m. left. + apply tm_step_palindrome_mod8 with (n := n) (tl := tl); assumption. + right. rewrite J. apply Nat.pow_le_mono_r. easy. + rewrite Nat.double_S. rewrite Nat.double_S. + rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. + rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. + rewrite <- Nat.succ_le_mono. apply le_0_n. +Qed. (*