Update
This commit is contained in:
parent
fb76741e4c
commit
acdc1a613c
@ -1153,6 +1153,28 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
||||
rewrite firstn_length_le. simpl in Q. rewrite Q. reflexivity.
|
||||
rewrite Y''. apply Nat.le_succ_diag_r. reflexivity.
|
||||
|
||||
(* destructuring n *)
|
||||
destruct n. inversion H0. rewrite <- tm_step_lemma in H.
|
||||
|
||||
(* inverting tm_morphism in tm_step n *)
|
||||
assert (hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))).
|
||||
generalize H11. generalize H. apply tm_morphism_app2.
|
||||
|
||||
assert (s ++ tl = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))).
|
||||
generalize H11. generalize H. apply tm_morphism_app3. symmetry in H13.
|
||||
|
||||
assert (even (length s) = true). unfold s. reflexivity.
|
||||
assert (s = tm_morphism (firstn (Nat.div2 (length s))
|
||||
(skipn (Nat.div2 (length hd'')) (tm_step n)))).
|
||||
generalize H14. generalize H13. apply tm_morphism_app2.
|
||||
|
||||
assert (tl = tm_morphism (skipn (Nat.div2 (length s))
|
||||
(skipn (Nat.div2 (length hd'')) (tm_step n)))).
|
||||
generalize H14. generalize H13. apply tm_morphism_app3.
|
||||
|
||||
rewrite H12 in H. rewrite H15 in H. rewrite H16 in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_eq in H.
|
||||
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user