Update
This commit is contained in:
parent
f73fe61b34
commit
98843bb92d
|
@ -15,6 +15,8 @@
|
|||
parity than the length of the factor being squared)
|
||||
- tm_step_square_prefix_not_nil (no square at the beginning
|
||||
of the sequence)
|
||||
- tm_step_square_tail_not_nil (no square at the end
|
||||
of the partial sequence)
|
||||
*)
|
||||
|
||||
Require Import thue_morse.
|
||||
|
|
|
@ -2096,6 +2096,52 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
Lemma tm_step_non_proper_palindrome_16 :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> length a = 8
|
||||
-> skipn (length hd - 8) hd = rev (firstn 8 tl).
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
|
||||
assert (J: length a mod 4 = 0). rewrite I. reflexivity.
|
||||
assert (K := J).
|
||||
rewrite tm_step_palindromic_length_12_prefix
|
||||
with (n := n) (hd := hd) (tl := tl) in K.
|
||||
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
|
||||
destruct a.
|
||||
replace (rev [b; b0; b1; b2; b3; b4; b5; b6])
|
||||
with ([b6; b5; b4; b3; b2; b1; b0; b]) in H.
|
||||
|
||||
assert (b4 = b5).
|
||||
replace (hd ++ [b; b0; b1; b2; b3; b4; b5; b6]
|
||||
++ [b6; b5; b4; b3; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1]) ++ [b2; b3; b4; b5]
|
||||
++ [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl) in H.
|
||||
assert (length (hd ++ [b; b0; b1]) mod 4 = 3).
|
||||
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K.
|
||||
reflexivity. easy.
|
||||
assert (exists x, skipn 2 [b2; b3; b4; b5] = [x; x]).
|
||||
generalize H0.
|
||||
apply tm_step_factor4_3mod4 with (n' := n)
|
||||
(y := [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption.
|
||||
reflexivity. destruct H1. inversion H1. reflexivity.
|
||||
rewrite <- app_assoc. reflexivity. rewrite H0 in H.
|
||||
|
||||
assert (b5 <> b3).
|
||||
replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6]
|
||||
++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1; b2; b3; b5; b5; b6; b6])
|
||||
++ [b5] ++ [b5] ++ [b3] ++ [b2;b1;b0;b] ++ tl) in H.
|
||||
apply tm_step_cubefree in H.
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
Lemma tm_step_proper_palindrome_center :
|
||||
|
|
Loading…
Reference in New Issue