(** * The Thue-Morse sequence (part 4) TODO *) Require Import thue_morse. Require Import thue_morse2. Require Import thue_morse3. Require Import Coq.Lists.List. Require Import PeanoNat. Require Import Nat. Require Import Bool. Require Import Arith. Require Import Lia. Import ListNotations. Theorem tm_step_palindrome_power2_inverse : forall (m n k : nat) (hd tl : list bool), tm_step n = hd ++ tl -> length hd = S (Nat.double k) * 2^m -> odd m = true -> tl <> nil -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl). Proof. intros m n k hd tl. intros H I J K. assert (L: 2^m <= length hd). rewrite I. lia. assert (M: m < n). assert (length (tm_step n) = length (hd ++ tl)). rewrite H. reflexivity. rewrite tm_size_power2 in H0. rewrite app_length in H0. (* rewrite I in H0. *) assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H1. apply Nat.pow_le_mono_r with (a := 2) in H1. assert (2^n <= length hd). generalize L. generalize H1. apply Nat.le_trans. rewrite H0 in H2. rewrite <- Nat.add_0_r in H2. rewrite <- Nat.add_le_mono_l in H2. destruct tl. contradiction K. reflexivity. simpl in H2. apply Nat.nle_succ_0 in H2. contradiction. easy. assumption. assert (N: length (tm_step n) mod 2^m = 0). rewrite tm_size_power2. apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite <- Nat.pow_sub_r. rewrite <- Nat.pow_add_r. rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. apply Nat.lt_le_incl. assumption. easy. apply Nat.lt_le_incl. assumption. assert (O: length hd mod 2^m = 0). apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite I. rewrite Nat.div_mul. rewrite Nat.mul_comm. reflexivity. apply Nat.pow_nonzero. easy. assert (P: length tl mod 2 ^ m = 0). rewrite H in N. rewrite app_length in N. rewrite <- Nat.add_mod_idemp_l in N. rewrite O in N. assumption. apply Nat.pow_nonzero. easy. assert (Q: 2^m <= length tl). apply Nat.div_exact in P. rewrite P. destruct (length tl / 2^m). rewrite Nat.mul_0_r in P. apply length_zero_iff_nil in P. rewrite P in K. contradiction K. reflexivity. rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l. apply Nat.le_succ_l. apply Nat.lt_0_succ. apply Nat.pow_nonzero. easy. replace hd with (firstn (length hd - 2^m) hd ++ skipn (length hd - 2^m) hd) in H. replace tl with (firstn (2^m) tl ++ skipn (2^m) tl) in H. rewrite <- app_assoc in H. replace ( skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl ++ skipn (2 ^ m) tl ) with ( (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) ++ skipn (2 ^ m) tl ) in H. assert (length (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) = 2^(S m)). rewrite app_length. rewrite skipn_length. rewrite firstn_length_le. replace (length hd) with (length hd -2^m + 2^m) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. simpl. rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption. assumption. assert (length (firstn (length hd - 2^m) hd) mod 2^(S m) = 0). rewrite firstn_length_le. replace (2^m) with (2^m * 1). rewrite I. rewrite Nat.mul_comm. rewrite <- Nat.mul_sub_distr_l. rewrite Nat.sub_succ. rewrite Nat.sub_0_r. rewrite Nat.double_twice. rewrite Nat.mul_assoc. replace (2^m * 2) with (2^(S m)). rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity. apply Nat.pow_nonzero. easy. rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. reflexivity. apply Nat.le_0_l. apply Nat.mul_1_r. apply Nat.le_sub_l. assert ( skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = tm_step (S m) \/ skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = map negb (tm_step (S m))). generalize H1. generalize H0. generalize H. apply tm_step_repeating_patterns2. apply tm_step_palindromic_full in J. destruct H2; rewrite J in H2. - assert (skipn (length hd - 2^m) hd = tm_step m). apply app_eq_length_head in H2. assumption. rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite tm_size_power2. reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3. assert (firstn (2^m) tl = rev (tm_step m)). rewrite H3 in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity. rewrite H4. rewrite rev_involutive. reflexivity. - assert (skipn (length hd - 2^m) hd = map negb (tm_step m)). rewrite map_app in H2. apply app_eq_length_head in H2. assumption. rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite map_length. rewrite tm_size_power2. reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3. assert (firstn (2^m) tl = map negb (rev (tm_step m))). rewrite H3 in H2. rewrite map_app in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity. rewrite H4. rewrite map_rev. rewrite rev_involutive. reflexivity. - rewrite <- app_assoc. reflexivity. - rewrite firstn_skipn. reflexivity. - rewrite firstn_skipn. reflexivity. Qed. Theorem tm_step_palindrome_power2_inverse' : forall (m n k : nat) (hd tl : list bool), tm_step n = hd ++ tl -> length hd = S (Nat.double k) * 2^m -> odd m = true -> 0 < k -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl). Proof. intros m n k hd tl. intros H I J L. assert (K: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec. destruct K as [K|K]. rewrite K in H. rewrite app_nil_r in H. rewrite <- H in I. rewrite tm_size_power2 in I. assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H0. apply Nat.pow_le_mono_r with (a := 2) in H0. rewrite I in H0. rewrite <- Nat.mul_1_l in H0. rewrite <- Nat.mul_le_mono_pos_r in H0. rewrite <- Nat.succ_le_mono in H0. apply Nat.le_0_r in H0. rewrite Nat.double_twice in H0. apply Nat.mul_eq_0_r in H0. rewrite H0 in L. inversion L. easy. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. easy. replace n with (n-m+m) in I. rewrite Nat.pow_add_r in I. rewrite Nat.mul_cancel_r in I. assert (even (2^(n-m)) = true). apply Nat.sub_gt in H0. apply Nat.neq_0_lt_0 in H0. destruct (n-m). inversion H0. rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. rewrite I in H1. rewrite Nat.even_succ in H1. rewrite Nat.double_twice in H1. rewrite Nat.odd_mul in H1. inversion H1. apply Nat.pow_nonzero. easy. lia. generalize K. generalize J. generalize I. generalize H. apply tm_step_palindrome_power2_inverse. Qed. Lemma tm_step_square_even_rev : forall (j n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j) -> a = rev a. Proof. intro j. induction j; intros n hd a tl; intros H I. - destruct I. + destruct a. inversion H0. destruct a. reflexivity. inversion H0. + destruct a. inversion H0. destruct a. inversion H0. destruct a. inversion H0. destruct a. assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e. reflexivity. assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1. rewrite e in H. replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl) with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H. apply tm_step_consecutive_identical' in H. inversion H. rewrite <- app_assoc. reflexivity. assert (b = b0). destruct b; destruct b0; destruct b1; reflexivity || contradiction n0 || contradiction n1; reflexivity. rewrite H1 in H. replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl) with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H. apply tm_step_consecutive_identical' in H. inversion H. reflexivity. inversion H0. - assert (even (length a) = true). destruct I; rewrite H0; rewrite Nat.double_S; rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. assert (0 < length a). destruct I; rewrite H1. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. apply Nat.mul_pos_pos. lia. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert (even (length (hd ++ a)) = true). generalize H1. generalize H. apply tm_step_square_pos. assert (even (length hd) = true). rewrite app_length in H2. rewrite Nat.even_add in H2. rewrite H0 in H2. destruct (even (length hd)). reflexivity. inversion H2. assert (2 <= n). assert (length (tm_step n) = length (tm_step n)). reflexivity. rewrite H in H4 at 2. rewrite app_length in H4. rewrite Nat.add_comm in H4. rewrite app_length in H4. destruct I; rewrite H5 in H4; rewrite tm_size_power2 in H4; rewrite Nat.double_S in H4; symmetry in H4; apply Nat.eq_le_incl in H4. assert (2^(S (S (Nat.double j))) <= 2^n). assert (2^(S (S (Nat.double j))) <= 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd). rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4. generalize H6. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H6. assert (2 <= S (S (Nat.double j))). lia. generalize H6. generalize H7. apply Nat.le_trans. apply Nat.lt_1_2. assert (3 * 2^(S (S (Nat.double j))) <= 2^n). assert (3 * 2^(S (S (Nat.double j))) <= 3 * 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd). rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4. generalize H6. apply Nat.le_trans. assert (2^(S (S (Nat.double j))) <= 3 * 2^(S (S (Nat.double j)))). rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_pos_r. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. lia. assert (2^(S (S (Nat.double j))) <= 2^n). generalize H6. generalize H7. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H8. assert (2 <= S (S (Nat.double j))). lia. generalize H8. generalize H9. apply Nat.le_trans. apply Nat.lt_1_2. destruct n. inversion H4. destruct n. inversion H4. inversion H6. assert( tm_step (S (S n)) = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step (S n)) ++ firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step (S n))) ++ firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))) ++ skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n)))). generalize H0. generalize H0. generalize H3. generalize H. apply tm_step_morphism4. pose (hd' := firstn (Nat.div2 (length hd)) (tm_step (S n))). pose (a' := firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step (S n)))). pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n))). fold hd' in H5. fold a' in H5. fold tl' in H5. assert (length hd' = Nat.div2 (length hd)). unfold hd'. rewrite firstn_length_le. reflexivity. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length hd = length (tm_morphism hd')). rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. assert (length a' = Nat.div2 (length a)). unfold a'. rewrite firstn_length_le. reflexivity. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a = length (tm_morphism a')). rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite H in H5. rewrite tm_morphism_app in H5. assert (hd = tm_morphism hd'). generalize H7. generalize H5. apply app_eq_length_head. rewrite <- H10 in H5. apply app_inv_head in H5. rewrite tm_morphism_app in H5. assert (a = tm_morphism a'). generalize H9. generalize H5. apply app_eq_length_head. rewrite <- H11 in H5. apply app_inv_head in H5. rewrite tm_morphism_app in H5. assert (length a = length (tm_morphism ( firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n)))))). rewrite tm_morphism_length. rewrite firstn_length_le. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_assoc. rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite app_length. lia. apply Nat.le_refl. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (a = tm_morphism ( firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))))). generalize H12. generalize H5. apply app_eq_length_head. rewrite <- H13 in H5. apply app_inv_head in H5. assert (H' := H). rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'. assert (even (length a') = true). unfold a'. rewrite firstn_length_le. destruct I; rewrite H14; rewrite Nat.double_S. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite <- Nat.mul_assoc. rewrite Nat.div2_double. rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (0 < length a'). unfold a'. rewrite firstn_length_le. destruct (length a). destruct I. inversion H1. inversion H1. destruct n0. inversion H0. replace (S (S n0)) with (n0 + 1*2). rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia. easy. lia. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (even (length (hd' ++ a')) = true). generalize H15. generalize H'. apply tm_step_square_pos. assert (even (length hd') = true). rewrite app_length in H16. rewrite Nat.even_add in H16. rewrite H14 in H16. destruct (even (length hd')). reflexivity. inversion H16. assert ( tm_step (S n) = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n) ++ firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd')) (tm_step n)) ++ firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)) ++ skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n))). generalize H14. generalize H14. generalize H17. generalize H'. apply tm_step_morphism4. pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)). pose (a'' := firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd')) (tm_step n))). pose (tl'' := skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n)). fold hd'' in H18. fold a'' in H18. fold tl'' in H18. assert (length hd'' = Nat.div2 (length hd')). unfold hd''. rewrite firstn_length_le. reflexivity. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite H'. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length hd' = length (tm_morphism hd'')). rewrite tm_morphism_length. rewrite H19. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. assert (length a'' = Nat.div2 (length a')). unfold a''. rewrite firstn_length_le. reflexivity. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H'. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a' = length (tm_morphism a'')). rewrite tm_morphism_length. rewrite H21. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite H' in H18. rewrite tm_morphism_app in H18. assert (hd' = tm_morphism hd''). generalize H20. generalize H18. apply app_eq_length_head. rewrite <- H23 in H18. apply app_inv_head in H18. rewrite tm_morphism_app in H18. assert (a' = tm_morphism a''). generalize H22. generalize H18. apply app_eq_length_head. rewrite <- H24 in H18. apply app_inv_head in H18. rewrite tm_morphism_app in H18. assert (length a' = length (tm_morphism ( firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n))))). rewrite tm_morphism_length. rewrite firstn_length_le. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H'. rewrite app_assoc. rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite app_length. lia. apply Nat.le_refl. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (a' = tm_morphism ( firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)))). generalize H25. generalize H18. apply app_eq_length_head. rewrite <- H26 in H18. apply app_inv_head in H18. assert (H'' := H'). rewrite H23 in H''. rewrite H24 in H''. rewrite H18 in H''. rewrite <- tm_morphism_app in H''. rewrite <- tm_morphism_app in H''. rewrite <- tm_morphism_app in H''. rewrite <- tm_step_lemma in H''. rewrite <- tm_morphism_eq in H''. assert (0 < length a''). unfold a''. rewrite firstn_length_le. destruct (length a'). inversion H15. destruct n0. inversion H14. replace (S (S n0)) with (n0 + 1*2). rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia. easy. lia. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H'. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a = 4 * length a''). rewrite H9. rewrite H24. rewrite tm_morphism_length. rewrite tm_morphism_length. lia. assert ( length a'' = 2 ^ Nat.double j \/ length a'' = 3 * 2 ^ Nat.double j ). destruct I. left. rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28. replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r. rewrite <- Nat.double_S. assumption. lia. lia. lia. lia. right. rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28. rewrite Nat.mul_assoc. replace (4*3) with (3*2*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.double_S. assumption. lia. lia. lia. lia. assert (a'' = rev a''). generalize H29. generalize H''. apply IHj. assert (Z := H11). rewrite H24 in H11. rewrite H30 in H11. rewrite <- tm_morphism_twice_rev in H11. rewrite <- H24 in H11. rewrite <- Z in H11. assumption. Qed. Lemma tm_step_square_odd_rev : forall (j n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)) -> a = map negb (rev a). Proof. intros j n hd a tl. intros H I. assert (even (length a) = true). destruct I; rewrite H0; rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. assert (0 < length a). destruct I; rewrite H1. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. apply Nat.mul_pos_pos. lia. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert (even (length (hd ++ a)) = true). generalize H1. generalize H. apply tm_step_square_pos. assert (even (length hd) = true). rewrite app_length in H2. rewrite Nat.even_add in H2. rewrite H0 in H2. destruct (even (length hd)). reflexivity. inversion H2. assert (0 < n). assert (length (tm_step n) = length (tm_step n)). reflexivity. rewrite H in H4 at 2. rewrite app_length in H4. rewrite Nat.add_comm in H4. destruct a. inversion H1. simpl in H4. rewrite app_length in H4. simpl in H4. rewrite Nat.add_succ_r in H4. destruct n. inversion H4. lia. destruct n. inversion H4. assert( tm_step (S n) = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n) ++ firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step n)) ++ firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++ skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step n))). generalize H0. generalize H0. generalize H3. generalize H. apply tm_step_morphism4. pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)). pose (a' := firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step n))). pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step n)). fold hd' in H5. fold a' in H5. fold tl' in H5. assert (length hd' = Nat.div2 (length hd)). unfold hd'. rewrite firstn_length_le. reflexivity. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length hd = length (tm_morphism hd')). rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. assert (length a' = Nat.div2 (length a)). unfold a'. rewrite firstn_length_le. reflexivity. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a = length (tm_morphism a')). rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite H in H5. rewrite tm_morphism_app in H5. assert (hd = tm_morphism hd'). generalize H7. generalize H5. apply app_eq_length_head. rewrite <- H10 in H5. apply app_inv_head in H5. rewrite tm_morphism_app in H5. assert (a = tm_morphism a'). generalize H9. generalize H5. apply app_eq_length_head. rewrite <- H11 in H5. apply app_inv_head in H5. rewrite tm_morphism_app in H5. assert (length a = length (tm_morphism ( firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step n))))). rewrite tm_morphism_length. rewrite firstn_length_le. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_assoc. rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite app_length. lia. apply Nat.le_refl. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (a = tm_morphism ( firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))). generalize H12. generalize H5. apply app_eq_length_head. rewrite <- H13 in H5. apply app_inv_head in H5. assert (H' := H). rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'. assert (length a = 2 * length a'). rewrite tm_morphism_length in H9. assumption. assert (length a' = 2^(Nat.double j) \/ length a' = 3 * 2^(Nat.double j)). destruct I; [left | right]; rewrite <- Nat.mul_cancel_l with (p := 2). rewrite <- tm_morphism_length. rewrite <- H11. rewrite <- Nat.pow_succ_r. assumption. lia. lia. rewrite <- tm_morphism_length. rewrite <- H11. rewrite Nat.mul_assoc. replace (2*3) with (3*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. assumption. lia. lia. easy. assert (Z := H11). assert (a' = rev a'). generalize H15. generalize H'. apply tm_step_square_even_rev. rewrite H16 in H11. rewrite <- tm_morphism_rev2 in H11. rewrite <- Z in H11. assumption. Qed. Theorem tm_step_square_rev : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> ( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))). Proof. intros n hd a tl. intros H I. assert (exists k j, length a = S (Nat.double k) * 2^j). apply trailing_zeros; assumption. destruct H0. destruct H0. assert (0 < n). assert (length (tm_step n) = length (tm_step n)). reflexivity. rewrite H in H1 at 2. rewrite app_length in H1. rewrite Nat.add_comm in H1. destruct a. inversion I. simpl in H1. rewrite app_length in H1. simpl in H1. rewrite Nat.add_succ_r in H1. destruct n. inversion H1. lia. destruct n. inversion H1. assert (x = 0 \/ x = 1). generalize H0. generalize H. apply tm_step_square_size. assert (Nat.Even x0 \/ Nat.Odd x0). apply Nat.Even_or_Odd. destruct H3. apply Nat.Even_double in H3. rewrite H3 in H0. assert (length a = 2^(Nat.double (Nat.div2 x0)) \/ length a = 3 * 2^(Nat.double (Nat.div2 x0))). destruct H2; [left|right]; rewrite H2 in H0; rewrite H0. simpl. lia. reflexivity. left. split. generalize H4. generalize H. apply tm_step_square_even_rev. exists (Nat.div2 x0). assumption. apply Nat.Odd_double in H3. rewrite H3 in H0. assert (length a = 2^(S (Nat.double (Nat.div2 x0))) \/ length a = 3 * 2^(S (Nat.double (Nat.div2 x0)))). destruct H2; [left|right]; rewrite H2 in H0; rewrite H0. simpl. lia. reflexivity. right. split. generalize H4. generalize H. apply tm_step_square_odd_rev. exists (Nat.div2 x0). assumption. Qed. Lemma tm_step_square_rev_even : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> a = rev a -> even m = true. Proof. intros m n hd a tl. intros H I J. assert (0 < length a). rewrite I. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert ( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))). generalize H0. generalize H. apply tm_step_square_rev. destruct H1. destruct H1. destruct H2. destruct H2. rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2. rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia. rewrite I in H2. assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2. rewrite Nat.log2_pow2 in H3. rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3. rewrite H3 in H2. rewrite Nat.add_succ_r in H2. rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2. rewrite Nat.mul_cancel_r in H2. inversion H2. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. destruct H1. rewrite J in H1 at 1. destruct a. inversion H0. simpl in H1. rewrite map_app in H1. apply app_inj_tail in H1. destruct H1. destruct b. inversion H3. inversion H3. Qed. Lemma tm_step_square_rev_odd : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> a = map negb (rev a) -> odd m = true. Proof. intros m n hd a tl. intros H I J. assert (0 < length a). rewrite I. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert ( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))). generalize H0. generalize H. apply tm_step_square_rev. destruct H1. destruct H1. rewrite J in H1 at 1. destruct a. inversion H0. simpl in H1. rewrite map_app in H1. apply app_inj_tail in H1. destruct H1. destruct b. inversion H3. inversion H3. destruct H1. destruct H2. destruct H2. rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2. rewrite Nat.odd_succ. rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia. rewrite I in H2. assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2. rewrite Nat.log2_pow2 in H3. rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3. rewrite H3 in H2. rewrite Nat.add_succ_r in H2. rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2. rewrite Nat.mul_cancel_r in H2. inversion H2. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. Qed. Lemma tm_step_square_even_rev'_alpha : forall (j n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j) -> skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a) = rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl)) /\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a) /\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl). Proof. intro j. induction j; intros n hd a tl; intros H I. - destruct n. assert (length a = 0 \/ 0 < length a). apply Nat.eq_0_gt_0_cases. destruct H0. rewrite H0 in I. destruct I. symmetry in H1. apply Nat.pow_nonzero in H1. contradiction. easy. symmetry in H1. apply Nat.eq_mul_0 in H1. destruct H1. inversion H1. apply Nat.pow_nonzero in H1. contradiction. easy. assert (length (tm_step 0) = length (hd ++ a ++ a ++ tl)). rewrite H. reflexivity. rewrite app_length in H1. rewrite Nat.add_comm in H1. rewrite app_length in H1. rewrite app_length in H1. rewrite Nat.add_assoc in H1. symmetry in H1. apply Nat.eq_le_incl in H1. assert (2 <= length a + length a + length tl + length hd). assert (2 <= length a + length a). replace 2 with (1+1). rewrite <- Nat.le_succ_l in H0. apply Nat.add_le_mono; assumption. reflexivity. assert (length a + length a <= (length a + length a) + (length tl + length hd)). apply Nat.le_add_r. generalize H3. generalize H2. rewrite Nat.add_assoc. apply Nat.le_trans. assert (2 <= length (tm_step 0)). generalize H1. generalize H2. apply Nat.le_trans. inversion H3. apply Nat.nle_succ_0 in H5. contradiction. destruct I. + destruct a. inversion H0. destruct a. destruct hd. assert (nth_error (tm_step (S n)) 0 <> nth_error (tm_step (S (S n))) (S (2*0))). apply tm_step_succ_double_index. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. rewrite tm_step_stable with (n := S (S n)) (m := S n) in H1. rewrite H in H1. simpl in H1. contradiction H1. reflexivity. replace (S (2*0)) with (2^0). rewrite <- Nat.pow_lt_mono_r_iff. lia. lia. replace (S (2*0)) with (2^0). rewrite <- Nat.pow_lt_mono_r_iff. lia. lia. rewrite app_removelast_last with (l := b0::hd) (d := false) at 2. destruct tl. assert (tm_step (S n) = rev (tm_step (S n)) \/ tm_step (S n) = map negb (rev (tm_step (S n)))). apply tm_step_rev. rewrite H in H1 at 2. rewrite H in H1 at 3. rewrite rev_app_distr in H1. rewrite rev_app_distr in H1. rewrite <- app_nil_end in H1. assert (nth_error (tm_step (S n)) 0 <> nth_error (tm_step (S (S n))) (S (2*0))). apply tm_step_succ_double_index. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. rewrite tm_step_stable with (n := S (S n)) (m := S n) in H2. destruct H1. rewrite H1 in H2. simpl in H2. contradiction H2. reflexivity. rewrite H1 in H2. simpl in H2. contradiction H2. reflexivity. replace (S (2*0)) with (2^0). rewrite <- Nat.pow_lt_mono_r_iff. lia. lia. replace (S (2*0)) with (2^0). rewrite <- Nat.pow_lt_mono_r_iff. lia. lia. assert ({last (b0::hd) false=b} + {~ last (b0::hd) false=b}). apply bool_dec. destruct H1. rewrite app_removelast_last with (l := b0::hd) (d := false) in H. rewrite e in H. rewrite <- app_assoc in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. easy. assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite <- e in H. replace (b::tl) with ([b] ++ tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. easy. assert (last (b0::hd) false = b1). destruct (last (b0::hd) false); destruct b; destruct b1; reflexivity || contradiction n0 || contradiction n1; reflexivity. rewrite H1. rewrite app_length. replace (2 ^ S (Nat.log2 (length [b]))) with (1+1). rewrite Nat.sub_add_distr. rewrite <- Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_0_r. rewrite <- app_assoc. rewrite skipn_app. replace (length (b0::hd) - 1) with (length (removelast (b0::hd))). rewrite skipn_all. rewrite Nat.sub_diag. split. reflexivity. rewrite <- Nat.add_le_mono_r. split. simpl. rewrite <- Nat.succ_le_mono. lia. simpl. rewrite <- Nat.succ_le_mono. lia. rewrite app_removelast_last with (l := b0::hd) (d := false) at 2. rewrite app_length. rewrite Nat.add_sub. reflexivity. easy. apply Nat.le_refl. reflexivity. easy. inversion H0. + destruct a. inversion H0. destruct a. inversion H0. destruct a. inversion H0. destruct a. assert ({b=b0} + {~ b=b0}). apply bool_dec. destruct H1. rewrite e in H. replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl) with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ b1::tl) in H. apply tm_step_consecutive_identical' in H. inversion H. reflexivity. assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1. rewrite e in H. replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl) with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H. apply tm_step_consecutive_identical' in H. inversion H. rewrite <- app_assoc. reflexivity. assert (b = b1). destruct b; destruct b0; destruct b1; reflexivity || contradiction n0 || contradiction n1; reflexivity. rewrite H1 in H. rewrite H1. destruct n. assert (length (tm_step 1) = length (tm_step 1)). reflexivity. rewrite H in H2 at 2. rewrite app_length in H2. rewrite Nat.add_comm in H2. rewrite app_length in H2. inversion H2. destruct hd. assert (nth_error (tm_step (S n)) 1 = nth_error (tm_step (S (S n))) (2 * 1)). apply tm_step_double_index. rewrite tm_step_stable with (n := S n) (m := S (S n)) in H2. rewrite H in H2. simpl in H2. inversion H2. rewrite H4 in H. replace ([] ++ [b1; b1; b1] ++ [b1; b1; b1] ++ tl) with ([b1;b1;b1] ++ [b1] ++ [b1] ++ [b1] ++ tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. replace 1 with (2^0) at 1. apply Nat.pow_lt_mono_r. lia. lia. reflexivity. replace 1 with (2^0) at 1. apply Nat.pow_lt_mono_r. lia. lia. reflexivity. rewrite app_removelast_last with (l := b2::hd) (d := false) at 2. destruct tl. assert (tm_step (S (S n)) = rev (tm_step (S (S n))) \/ tm_step (S (S n)) = map negb (rev (tm_step (S (S n))))). apply tm_step_rev. rewrite H in H2 at 2. rewrite H in H2 at 3. destruct H2. rewrite rev_app_distr in H2. assert (nth_error (tm_step (S n)) 1 = nth_error (tm_step (S (S n))) (2 * 1)). apply tm_step_double_index. rewrite tm_step_stable with (n := S n) (m := S (S n)) in H3. rewrite H2 in H3. simpl in H3. inversion H3. rewrite H5 in H. replace ((b2 :: hd) ++ [b1; b1; b1] ++ [b1; b1; b1] ++ []) with ((b2::hd) ++ [b1] ++ [b1] ++ [b1] ++ [b1;b1;b1]) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. replace 1 with (2^0) at 1. apply Nat.pow_lt_mono_r. lia. lia. reflexivity. replace 1 with (2^0) at 1. apply Nat.pow_lt_mono_r. lia. lia. reflexivity. rewrite rev_app_distr in H2. assert (nth_error (tm_step (S n)) 1 = nth_error (tm_step (S (S n))) (2 * 1)). apply tm_step_double_index. rewrite tm_step_stable with (n := S n) (m := S (S n)) in H3. rewrite H2 in H3. simpl in H3. inversion H3. assert (b0=b1). destruct b0; destruct b1; reflexivity || inversion H5. rewrite H4 in H. replace ((b2 :: hd) ++ [b1; b1; b1] ++ [b1; b1; b1] ++ []) with ((b2::hd) ++ [b1] ++ [b1] ++ [b1] ++ [b1;b1;b1]) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. replace 1 with (2^0) at 1. apply Nat.pow_lt_mono_r. lia. lia. reflexivity. replace 1 with (2^0) at 1. apply Nat.pow_lt_mono_r. lia. lia. reflexivity. assert ({last (b2::hd) false=b1} + {~ last (b2::hd) false=b1}). apply bool_dec. destruct H2. rewrite app_removelast_last with (l := b2::hd) (d := false) in H. rewrite e in H. rewrite <- app_assoc in H. replace ( removelast (b2 :: hd) ++ [b1] ++ [b1; b0; b1] ++ [b1; b0; b1] ++ b3 :: tl) with (removelast (b2::hd) ++ [b1;b1] ++ [b0] ++ [b1;b1] ++ b0::b1::b3::tl) in H. apply tm_step_consecutive_identical' in H. inversion H. reflexivity. easy. assert ({b3=b1} + {~ b3=b1}). apply bool_dec. destruct H2. rewrite <- e in H. replace ((b2 :: hd) ++ [b3; b0; b3] ++ [b3; b0; b3] ++ b3 :: tl) with (((b2::hd) ++ [b3;b0]) ++ [b3;b3] ++ [b0] ++ [b3;b3] ++ tl) in H. apply tm_step_consecutive_identical' in H. inversion H. rewrite <- app_assoc. reflexivity. assert (last (b2::hd) false = b3). destruct (last (b2::hd) false); destruct b3; destruct b1; reflexivity || contradiction n2 || contradiction n3; reflexivity. rewrite H2. rewrite app_length. replace (2 ^ S (Nat.log2 (length [b1;b0;b1]))) with (3+1). rewrite Nat.sub_add_distr. rewrite <- Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_0_r. rewrite <- app_assoc. rewrite skipn_app. replace (length (b2::hd) - 1) with (length (removelast (b2::hd))). rewrite skipn_all. rewrite Nat.sub_diag. split. reflexivity. simpl. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. split. lia. lia. rewrite app_removelast_last with (l := b2::hd) (d := false) at 2. rewrite app_length. rewrite Nat.add_sub. reflexivity. easy. apply Nat.le_refl. reflexivity. easy. inversion H0. - assert (even (length a) = true). destruct I; rewrite H0; rewrite Nat.double_S; rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. assert (0 < length a). destruct I; rewrite H1. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. apply Nat.mul_pos_pos. lia. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert (even (length (hd ++ a)) = true). generalize H1. generalize H. apply tm_step_square_pos. assert (even (length hd) = true). rewrite app_length in H2. rewrite Nat.even_add in H2. rewrite H0 in H2. destruct (even (length hd)). reflexivity. inversion H2. assert (2 <= n). assert (length (tm_step n) = length (tm_step n)). reflexivity. rewrite H in H4 at 2. rewrite app_length in H4. rewrite Nat.add_comm in H4. rewrite app_length in H4. destruct I; rewrite H5 in H4; rewrite tm_size_power2 in H4; rewrite Nat.double_S in H4; symmetry in H4; apply Nat.eq_le_incl in H4. assert (2^(S (S (Nat.double j))) <= 2^n). assert (2^(S (S (Nat.double j))) <= 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd). rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4. generalize H6. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H6. assert (2 <= S (S (Nat.double j))). lia. generalize H6. generalize H7. apply Nat.le_trans. apply Nat.lt_1_2. assert (3 * 2^(S (S (Nat.double j))) <= 2^n). assert (3 * 2^(S (S (Nat.double j))) <= 3 * 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd). rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4. generalize H6. apply Nat.le_trans. assert (2^(S (S (Nat.double j))) <= 3 * 2^(S (S (Nat.double j)))). rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_pos_r. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. lia. assert (2^(S (S (Nat.double j))) <= 2^n). generalize H6. generalize H7. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H8. assert (2 <= S (S (Nat.double j))). lia. generalize H8. generalize H9. apply Nat.le_trans. apply Nat.lt_1_2. destruct n. inversion H4. destruct n. inversion H4. inversion H6. assert( tm_step (S (S n)) = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step (S n)) ++ firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step (S n))) ++ firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))) ++ skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n)))). generalize H0. generalize H0. generalize H3. generalize H. apply tm_step_morphism4. pose (hd' := firstn (Nat.div2 (length hd)) (tm_step (S n))). pose (a' := firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step (S n)))). pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n))). fold hd' in H5. fold a' in H5. fold tl' in H5. assert (length hd' = Nat.div2 (length hd)). unfold hd'. rewrite firstn_length_le. reflexivity. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length hd = length (tm_morphism hd')). rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. assert (length a' = Nat.div2 (length a)). unfold a'. rewrite firstn_length_le. reflexivity. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a = length (tm_morphism a')). rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite H in H5. rewrite tm_morphism_app in H5. assert (hd = tm_morphism hd'). generalize H7. generalize H5. apply app_eq_length_head. rewrite <- H10 in H5. apply app_inv_head in H5. rewrite tm_morphism_app in H5. assert (a = tm_morphism a'). generalize H9. generalize H5. apply app_eq_length_head. rewrite <- H11 in H5. apply app_inv_head in H5. rewrite tm_morphism_app in H5. assert (length a = length (tm_morphism ( firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n)))))). rewrite tm_morphism_length. rewrite firstn_length_le. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_assoc. rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite app_length. lia. apply Nat.le_refl. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (a = tm_morphism ( firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))))). generalize H12. generalize H5. apply app_eq_length_head. rewrite <- H13 in H5. apply app_inv_head in H5. assert (H' := H). rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_morphism_app in H'. rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'. assert (even (length a') = true). unfold a'. rewrite firstn_length_le. destruct I; rewrite H14; rewrite Nat.double_S. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite <- Nat.mul_assoc. rewrite Nat.div2_double. rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (0 < length a'). unfold a'. rewrite firstn_length_le. destruct (length a). destruct I. inversion H1. inversion H1. destruct n0. inversion H0. replace (S (S n0)) with (n0 + 1*2). rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia. easy. lia. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (even (length (hd' ++ a')) = true). generalize H15. generalize H'. apply tm_step_square_pos. assert (even (length hd') = true). rewrite app_length in H16. rewrite Nat.even_add in H16. rewrite H14 in H16. destruct (even (length hd')). reflexivity. inversion H16. assert ( tm_step (S n) = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n) ++ firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd')) (tm_step n)) ++ firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)) ++ skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n))). generalize H14. generalize H14. generalize H17. generalize H'. apply tm_step_morphism4. pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)). pose (a'' := firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd')) (tm_step n))). pose (tl'' := skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n)). fold hd'' in H18. fold a'' in H18. fold tl'' in H18. assert (length hd'' = Nat.div2 (length hd')). unfold hd''. rewrite firstn_length_le. reflexivity. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite H'. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length hd' = length (tm_morphism hd'')). rewrite tm_morphism_length. rewrite H19. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. assert (length a'' = Nat.div2 (length a')). unfold a''. rewrite firstn_length_le. reflexivity. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H'. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a' = length (tm_morphism a'')). rewrite tm_morphism_length. rewrite H21. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite H' in H18. rewrite tm_morphism_app in H18. assert (hd' = tm_morphism hd''). generalize H20. generalize H18. apply app_eq_length_head. rewrite <- H23 in H18. apply app_inv_head in H18. rewrite tm_morphism_app in H18. assert (a' = tm_morphism a''). generalize H22. generalize H18. apply app_eq_length_head. rewrite <- H24 in H18. apply app_inv_head in H18. rewrite tm_morphism_app in H18. assert (length a' = length (tm_morphism ( firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n))))). rewrite tm_morphism_length. rewrite firstn_length_le. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H'. rewrite app_assoc. rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite app_length. lia. apply Nat.le_refl. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (a' = tm_morphism ( firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)))). generalize H25. generalize H18. apply app_eq_length_head. rewrite <- H26 in H18. apply app_inv_head in H18. assert (H'' := H'). rewrite H23 in H''. rewrite H24 in H''. rewrite H18 in H''. rewrite <- tm_morphism_app in H''. rewrite <- tm_morphism_app in H''. rewrite <- tm_morphism_app in H''. rewrite <- tm_step_lemma in H''. rewrite <- tm_morphism_eq in H''. assert (0 < length a''). unfold a''. rewrite firstn_length_le. destruct (length a'). inversion H15. destruct n0. inversion H14. replace (S (S n0)) with (n0 + 1*2). rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia. easy. lia. rewrite skipn_length. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. rewrite H'. rewrite app_length. rewrite app_length. lia. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. assert (length a = 4 * length a''). rewrite H9. rewrite H24. rewrite tm_morphism_length. rewrite tm_morphism_length. lia. assert (G: length hd = 4 * length hd''). rewrite H7. rewrite H23. rewrite tm_morphism_length. rewrite tm_morphism_length. lia. assert (G': length tl = 4 * length tl''). rewrite H5. rewrite H18. rewrite tm_morphism_length. rewrite tm_morphism_length. lia. assert ( length a'' = 2 ^ Nat.double j \/ length a'' = 3 * 2 ^ Nat.double j ). destruct I. left. rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28. replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r. rewrite <- Nat.double_S. assumption. lia. lia. lia. lia. right. rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28. rewrite Nat.mul_assoc. replace (4*3) with (3*2*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.double_S. assumption. lia. lia. lia. lia. assert ( skipn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a'') = rev (firstn (2 ^ S (Nat.log2 (length a''))) (a'' ++ tl'')) /\ 2 ^ S (Nat.log2 (length a'')) <= length (hd'' ++ a'') /\ 2 ^ S (Nat.log2 (length a'')) <= length (a'' ++ tl'')). generalize H29. generalize H''. apply IHj. destruct H30 as [H30 H30']. destruct H30' as [H30' H30'']. rewrite app_assoc in H''. rewrite <- firstn_skipn with (l := hd'' ++ a'') (n := length (hd'' ++ a'') - 2^(S (Nat.log2 (length a'')))) in H''. rewrite <- firstn_skipn with (l := a'' ++ tl'') (n := 2^(S (Nat.log2 (length a'')))) in H''. assert (rev ( skipn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a'')) = firstn (2 ^ S (Nat.log2 (length a''))) (a'' ++ tl'')). rewrite H30. rewrite rev_involutive. reflexivity. rewrite <- H31 in H''. assert (tm_step (S n) = tm_step (S n)). reflexivity. rewrite <- tm_step_lemma in H32 at 2. rewrite H'' in H32. rewrite tm_morphism_app in H32. rewrite tm_morphism_app in H32. rewrite tm_morphism_app in H32. assert (tm_step (S (S n)) = tm_step (S (S n))). reflexivity. rewrite <- tm_step_lemma in H33 at 2. rewrite H32 in H33. rewrite tm_morphism_app in H33. rewrite tm_morphism_app in H33. rewrite tm_morphism_app in H33. rewrite <- tm_morphism_twice_rev in H33. rewrite <- app_assoc in H33. rewrite app_assoc in H. rewrite <- firstn_skipn with (l := hd ++ a) (n := length (hd++a) - 2^(S (Nat.log2 (length a)))) in H. rewrite <- firstn_skipn with (l := a ++ tl) (n := 2^(S (Nat.log2 (length a)))) in H. rewrite <- app_assoc in H. rewrite H in H33. assert (length ( firstn (length (hd ++ a) - 2 ^ S (Nat.log2 (length a))) (hd ++ a)) = length (tm_morphism (tm_morphism (firstn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a''))))). rewrite tm_morphism_length. rewrite tm_morphism_length. rewrite firstn_length_le. rewrite firstn_length_le. rewrite app_length. rewrite H28. rewrite G. rewrite <- Nat.mul_add_distr_l. rewrite <- app_length. replace (4 * length a'') with (length a'' * 2^2). rewrite Nat.log2_mul_pow2. rewrite Nat.add_succ_l. rewrite Nat.add_succ_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. rewrite Nat.add_0_l. replace (2*2) with 4. rewrite <- Nat.mul_sub_distr_l. rewrite Nat.mul_assoc. reflexivity. reflexivity. lia. lia. destruct a''. rewrite H28 in H1. inversion H1. simpl. apply Nat.lt_0_succ. lia. rewrite Nat.mul_comm. reflexivity. apply Nat.le_sub_l. apply Nat.le_sub_l. assert (length ( skipn (length (hd ++ a) - 2 ^ S (Nat.log2 (length a))) (hd ++ a)) = length ( tm_morphism (tm_morphism (skipn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a''))))). rewrite tm_morphism_length. rewrite tm_morphism_length. rewrite skipn_length. rewrite skipn_length. replace (length (hd++a)) with ((length (hd++a) - 2^S (Nat.log2 (length a))) + 2^S (Nat.log2 (length a))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. replace (length (hd''++a'')) with ((length (hd''++a'') - 2^S (Nat.log2 (length a''))) + 2^S (Nat.log2 (length a''))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite H28. replace 4 with (2^2). rewrite Nat.mul_comm. rewrite Nat.log2_mul_pow2. rewrite Nat.add_0_l. rewrite Nat.add_0_l. rewrite Nat.add_succ_l. rewrite Nat.add_succ_l. rewrite Nat.add_0_l. reflexivity. destruct a''. rewrite H28 in H1. inversion H1. simpl. apply Nat.lt_0_succ. lia. reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption. apply Nat.le_refl. apply Nat.sub_add. rewrite app_length. rewrite H28. rewrite G. rewrite <- Nat.mul_add_distr_l. rewrite <- app_length. rewrite Nat.mul_comm. replace 4 with (2^2) at 1. rewrite Nat.log2_mul_pow2. rewrite Nat.add_succ_l. rewrite Nat.add_succ_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. rewrite Nat.add_0_l. replace (2*2) with 4. apply Nat.mul_le_mono_l. assumption. reflexivity. lia. lia. destruct a''. rewrite H28 in H1. inversion H1. simpl. apply Nat.lt_0_succ. lia. reflexivity. assert ( firstn (length (hd ++ a) - 2 ^ S (Nat.log2 (length a))) (hd ++ a) = tm_morphism (tm_morphism (firstn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a'')))). generalize H34. generalize H33. apply app_eq_length_head. rewrite H36 in H33. rewrite app_inv_head_iff in H33. assert ( skipn (length (hd ++ a) - 2 ^ S (Nat.log2 (length a))) (hd ++ a) = (tm_morphism (tm_morphism (skipn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a''))))). generalize H35. generalize H33. apply app_eq_length_head. rewrite H37 in H33. rewrite app_inv_head_iff in H33. rewrite H37. assert (length (firstn (2 ^ S (Nat.log2 (length a))) (a ++ tl)) = length (rev (tm_morphism (tm_morphism (skipn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a'')))))). rewrite rev_length. rewrite tm_morphism_length. rewrite tm_morphism_length. rewrite firstn_length_le. rewrite skipn_length. replace (length (hd''++a'')) with ((length (hd''++a'') - 2^S (Nat.log2 (length a''))) + 2^S (Nat.log2 (length a''))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite H28. rewrite Nat.mul_comm. replace 4 with (2^2). rewrite Nat.log2_mul_pow2. rewrite Nat.add_succ_l. rewrite Nat.add_succ_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.add_0_l. rewrite Nat.add_0_l. reflexivity. lia. lia. destruct a''. rewrite H28 in H1. inversion H1. simpl. apply Nat.lt_0_succ. lia. reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption. rewrite H28. rewrite Nat.mul_comm. replace 4 with (2^2). rewrite Nat.log2_mul_pow2. rewrite Nat.add_succ_l. rewrite Nat.add_succ_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.add_0_l. rewrite app_length. rewrite H28. rewrite G'. rewrite <- Nat.mul_add_distr_l. rewrite <- app_length. rewrite Nat.mul_assoc. apply Nat.mul_le_mono_l. assumption. lia. lia. destruct a''. rewrite H28 in H1. inversion H1. simpl. apply Nat.lt_0_succ. lia. reflexivity. assert (firstn (2 ^ S (Nat.log2 (length a))) (a ++ tl) = rev (tm_morphism (tm_morphism (skipn (length (hd'' ++ a'') - 2 ^ S (Nat.log2 (length a''))) (hd'' ++ a''))))). generalize H38. generalize H33. apply app_eq_length_head. rewrite H39. rewrite rev_involutive. split. reflexivity. split; rewrite app_length; rewrite H28; [rewrite G | rewrite G']; rewrite <- Nat.mul_add_distr_l; rewrite <- app_length; replace 4 with (2^2) at 1; rewrite Nat.mul_comm || reflexivity; rewrite Nat.log2_mul_pow2; lia || rewrite Nat.add_succ_l; rewrite Nat.add_succ_l; rewrite Nat.add_0_l; rewrite Nat.pow_succ_r; lia || rewrite Nat.pow_succ_r; lia. Qed. Lemma tm_step_square2_rev_even : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> a = rev a -> length (hd ++ a) mod 2^(S m) = 0. Proof. intros m n hd a tl. intros H I J. assert (K: even m = true). generalize J. generalize I. generalize H. apply tm_step_square_rev_even. assert (length a = 2^m \/ length a = 3*2^m). left. assumption. assert (K' := K). apply Nat.even_EvenT in K. apply Nat.EvenT_Even in K. apply Nat.Even_double in K. rewrite K in H0. assert ( skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a) = rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl)) /\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a) /\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl)). generalize H0. generalize H. apply tm_step_square_even_rev'_alpha. destruct H1. rewrite I in H1. rewrite Nat.log2_pow2 in H1. rewrite I in H2. rewrite Nat.log2_pow2 in H2. (* cas : length a = 1 *) destruct m. assert (0 < length a). rewrite I. apply Nat.lt_0_1. assert (even (length (hd ++ a)) = true). generalize H3. generalize H. apply tm_step_square_pos. apply Nat.even_EvenT in H4. apply Nat.EvenT_Even in H4. apply Nat.Even_double in H4. rewrite Nat.double_twice in H4. rewrite H4. rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity. easy. rewrite app_assoc in H. rewrite <- firstn_skipn with (l := hd ++ a) (n := length (hd++a) - 2^(S (S m))) in H. rewrite <- firstn_skipn with (l := a ++ tl) (n := 2^(S (S m))) in H. rewrite <- app_assoc in H. assert (firstn (2^(S (S m))) (a ++ tl) = rev (skipn (length (hd ++ a) - 2 ^ (S (S m))) (hd ++ a))). rewrite H1. rewrite rev_involutive. reflexivity. rewrite H3 in H. destruct m. inversion K'. assert (6 < length (skipn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a))). rewrite skipn_length. replace (length (hd++a)) with ((length (hd++a) - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite Nat.add_0_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. rewrite Nat.mul_assoc. assert (8*1 <= 8*2^m). apply Nat.mul_le_mono_l. apply Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert (6 < 8). lia. generalize H4. generalize H5. apply Nat.lt_le_trans. lia. lia. lia. lia. lia. assert (length (skipn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a)) = 2^(S (Nat.double (Nat.div2 (S (S m)))))). rewrite skipn_length. replace (length (hd++a)) with ((length (hd++a) - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite K at 1. reflexivity. lia. apply Nat.sub_add. destruct H2. assumption. assert (length ( firstn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a) ++ skipn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a)) mod (2^ (S (Nat.double (Nat.div2 (S (S m)))))) = 0). generalize H5. generalize H4. generalize H. apply tm_step_palindromic_power2_odd. rewrite firstn_skipn in H6. rewrite <- Nat.Even_double in H6. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. Qed. Lemma tm_step_square2_rev_even_swap : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> (even m = true <-> a = rev a). Proof. intros m n hd a tl. intros H I. split. intro J. assert (( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j))))). assert (0 < length a). destruct a. symmetry in I. apply Nat.pow_nonzero in I. contradiction. easy. simpl. lia. generalize H0. generalize H. apply tm_step_square_rev. destruct H0. destruct H0. assumption. destruct H0. destruct H1. destruct H1. rewrite I in H1. apply Nat.pow_inj_r in H1. rewrite H1 in J. rewrite Nat.even_succ in J. rewrite Nat.double_twice in J. rewrite Nat.odd_mul in J. inversion J. lia. rewrite I in H1. assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H1 in H2 at 2. rewrite Nat.log2_pow2 in H2. rewrite Nat.log2_mul_pow2 in H2. replace (Nat.log2 3) with 1 in H2. rewrite H2 in H1. rewrite Nat.add_succ_r in H1. rewrite Nat.add_0_r in H1. rewrite Nat.pow_succ_r in H1. rewrite Nat.mul_cancel_r in H1. inversion H1. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. intro J. generalize J. generalize I. generalize H. apply tm_step_square_rev_even. Qed. Lemma tm_step_square2_rev_even' : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> even m = true -> length (hd ++ a) mod 2^(S m) = 0. Proof. intros m n hd a tl. intros H I J. assert (a = rev a). rewrite tm_step_square2_rev_even_swap with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption. generalize H0. generalize I. generalize H. apply tm_step_square2_rev_even. Qed. Lemma tm_step_square3_rev_even_swap : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 3*2^m -> (even m = true <-> a = rev a). Proof. intros m n hd a tl. intros H I. split. intro J. assert (( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j))))). assert (0 < length a). destruct a. symmetry in I. rewrite Nat.eq_mul_0 in I. destruct I. inversion H0. apply Nat.pow_nonzero in H0. contradiction. easy. simpl. lia. generalize H0. generalize H. apply tm_step_square_rev. destruct H0. destruct H0. assumption. destruct H0. destruct H1. destruct H1. assert (Nat.log2 (3*2^m) = Nat.log2 (3*2^m)). reflexivity. rewrite <- I in H2 at 1. rewrite H1 in H2. rewrite Nat.log2_pow2 in H2. rewrite Nat.log2_mul_pow2 in H2. replace (Nat.log2 3) with 1 in H2. rewrite H2 in H1. rewrite Nat.add_succ_r in H1. rewrite Nat.add_0_r in H1. rewrite Nat.pow_succ_r in H1. rewrite I in H1. apply Nat.mul_cancel_r in H1. inversion H1. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. rewrite I in H1. apply Nat.mul_cancel_l in H1. apply Nat.pow_inj_r in H1. rewrite H1 in J. rewrite Nat.even_succ in J. rewrite Nat.double_twice in J. rewrite Nat.odd_mul in J. inversion J. lia. easy. intro J. assert (( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j))))). assert (0 < length a). destruct a. symmetry in I. rewrite Nat.eq_mul_0 in I. destruct I. inversion H0. apply Nat.pow_nonzero in H0. contradiction. easy. simpl. lia. generalize H0. generalize H. apply tm_step_square_rev. destruct H0. destruct H0. destruct H1. destruct H1. assert (Nat.log2 (3*2^m) = Nat.log2 (3*2^m)). reflexivity. rewrite <- I in H2 at 1. rewrite H1 in H2. rewrite Nat.log2_pow2 in H2. rewrite Nat.log2_mul_pow2 in H2. replace (Nat.log2 3) with 1 in H2. rewrite H2 in H1. rewrite Nat.add_succ_r in H1. rewrite Nat.add_0_r in H1. rewrite Nat.pow_succ_r in H1. rewrite I in H1. apply Nat.mul_cancel_r in H1. inversion H1. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. rewrite I in H1. apply Nat.mul_cancel_l in H1. apply Nat.pow_inj_r in H1. rewrite H1. rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia. easy. destruct H0. rewrite <- J in H0. destruct a. symmetry in I. rewrite Nat.eq_mul_0 in I. destruct I. inversion H2. apply Nat.pow_nonzero in H2. contradiction. easy. simpl in H0. inversion H0. destruct b; inversion H3. Qed. Lemma tm_step_square3_rev_even : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 3 * 2^m -> a = rev a -> length (hd ++ a) mod 2^(S m) = 0. Proof. intros m n hd a tl. intros H I J. assert (even m = true). rewrite <- tm_step_square3_rev_even_swap with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption. destruct m. assert (even (length (hd ++ a)) = true). assert (0 < length a). destruct a. inversion I. simpl. lia. generalize H1. generalize H. apply tm_step_square_pos. apply Nat.even_EvenT in H1. apply Nat.EvenT_Even in H1. apply Nat.Even_double in H1. rewrite H1. rewrite Nat.double_twice. rewrite Nat.mul_comm. apply Nat.mod_mul. easy. destruct m. inversion H0. rewrite app_assoc in H. rewrite <- firstn_skipn with (l := hd ++ a) (n := length (hd++a) - 2^(S (S (S m)))) in H. rewrite <- firstn_skipn with (l := a ++ tl) (n := 2^(S (S (S m)))) in H. rewrite <- firstn_skipn with (l := a) (n := length (a) - 2^(S (S (S m)))) in J at 1. rewrite <- firstn_skipn with (l := a) (n := 2^(S (S (S m)))) in J at 5. rewrite skipn_app in H. rewrite skipn_all2 in H. replace (firstn (2^(S (S (S m)))) (a++tl)) with (firstn (2^(S (S (S m)))) a ++ firstn (2^(S (S (S m))) - length a) tl) in H. rewrite rev_app_distr in J. assert (J' := J). apply app_eq_length_head in J. rewrite J in J'. apply app_inv_head in J'. rewrite app_nil_l in H. replace (length (hd ++ a) - 2 ^ (S (S (S m))) - length hd) with (length a - 2^(S (S (S m)))) in H. assert (firstn (2^(S (S (S m)))) a = rev (skipn (length a - 2^(S (S (S m)))) a)). rewrite J'. rewrite rev_involutive. reflexivity. rewrite H1 in H. assert (length (skipn (length a - 2^(S (S (S m)))) a) = 2^(S (Nat.double (Nat.div2 (S (S m)))))). rewrite skipn_length. replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.le_refl. apply Nat.sub_add. rewrite I. rewrite Nat.pow_succ_r. apply Nat.mul_le_mono_r. lia. lia. assert (6 < length (skipn (length a - 2^(S (S (S m)))) a)). rewrite skipn_length. replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite Nat.add_0_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. rewrite Nat.mul_assoc. replace (2*2*2) with 8. assert (6 < 8). lia. assert (8 <= 8*2^m). rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_pos_l. lia. apply Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. generalize H4. generalize H3. apply Nat.lt_le_trans. reflexivity. lia. lia. lia. lia. apply Nat.sub_add. rewrite I. rewrite Nat.pow_succ_r. apply Nat.mul_le_mono_r. lia. lia. assert (length (firstn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a) ++ skipn (length a - 2 ^ S (S (S m))) a) mod (2 ^ S (Nat.double (Nat.div2 (S (S m))))) = 0). generalize H2. generalize H3. rewrite <- app_assoc in H. rewrite <- app_assoc in H. generalize H. apply tm_step_palindromic_power2_odd. rewrite <- Nat.Even_double in H4. rewrite app_length in H4. rewrite <- Nat.add_mod_idemp_r in H4. replace ( length (skipn (length a - 2 ^ S (S (S m))) a) mod 2 ^ S (S (S m)) ) with (2^(S (S (S m))) mod (2^(S (S (S m))))) in H4. rewrite Nat.add_mod_idemp_r in H4. rewrite firstn_length_le in H4. rewrite Nat.sub_add in H4. assumption. rewrite app_length. rewrite I. replace 3 with (1+2). rewrite Nat.mul_add_distr_r. rewrite Nat.add_assoc. rewrite <- Nat.pow_succ_r. apply Nat.le_add_l. lia. reflexivity. lia. apply Nat.pow_nonzero. easy. rewrite Nat.mod_same. rewrite skipn_length. replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite Nat.mod_same. reflexivity. apply Nat.pow_nonzero. easy. apply Nat.le_refl. rewrite Nat.sub_add. reflexivity. rewrite I. replace 3 with (1+2). rewrite Nat.mul_add_distr_r. rewrite <- Nat.pow_succ_r. apply Nat.le_add_l. lia. reflexivity. apply Nat.pow_nonzero. easy. apply Nat.pow_nonzero. easy. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite <- Nat.sub_add_distr. rewrite Nat.add_comm. rewrite Nat.sub_add_distr. rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. reflexivity. apply Nat.le_refl. rewrite rev_length. rewrite firstn_length_le. rewrite skipn_length. reflexivity. apply Nat.le_sub_l. rewrite <- firstn_app. reflexivity. rewrite app_length. rewrite Nat.pow_succ_r. rewrite I. rewrite <- Nat.add_sub_assoc. rewrite <- Nat.mul_sub_distr_r. apply Nat.le_add_r. apply Nat.mul_le_mono_r. lia. lia. Qed. Lemma tm_step_square3_rev_even' : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 3 * 2^m -> even m = true -> length (hd ++ a) mod 2^(S m) = 0. Proof. intros m n hd a tl. intros H I J. assert (a = rev a). rewrite tm_step_square3_rev_even_swap with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption. generalize H0. generalize I. generalize H. apply tm_step_square3_rev_even. Qed.