Update
This commit is contained in:
parent
bba694fa47
commit
e274d2789b
@ -1888,13 +1888,33 @@ Proof.
|
|||||||
|
|
||||||
assert (V: 3 < n). generalize I. generalize H.
|
assert (V: 3 < n). generalize I. generalize H.
|
||||||
apply tm_step_palindromic_length_12_n.
|
apply tm_step_palindromic_length_12_n.
|
||||||
|
destruct n. inversion V. destruct n. inversion V. inversion H1.
|
||||||
|
|
||||||
|
rewrite K in H. rewrite L in H. rewrite M in H.
|
||||||
|
rewrite tm_morphism_twice_rev in H.
|
||||||
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||||
|
rewrite <- tm_morphism_app 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_step_lemma in H.
|
||||||
|
rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
|
||||||
|
rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
|
||||||
|
|
||||||
|
pose (hd' := (firstn (length hd / 4) (tm_step n))).
|
||||||
|
pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
|
||||||
|
pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
|
||||||
|
fold hd' in H. fold a' in H. fold tl' in H.
|
||||||
|
|
||||||
|
rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
|
||||||
|
assert (N: length a = length a). reflexivity.
|
||||||
|
rewrite L in N at 2. fold a' in N.
|
||||||
|
rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
|
||||||
|
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
|
||||||
|
|
||||||
induction m.
|
induction m.
|
||||||
- rewrite K in H. rewrite L in H. rewrite M in H.
|
- assert (even (length (hd' ++ a')) = true).
|
||||||
rewrite tm_morphism_twice_rev in H.
|
|
||||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
||||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
||||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user