Update
This commit is contained in:
parent
c067e31ecd
commit
fb76741e4c
@ -1141,12 +1141,37 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||||||
reflexivity. contradiction n8. reflexivity. reflexivity.
|
reflexivity. contradiction n8. reflexivity. reflexivity.
|
||||||
rewrite H10 in H.
|
rewrite H10 in H.
|
||||||
|
|
||||||
|
(* simplify notations *)
|
||||||
|
replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1
|
||||||
|
:: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b0 :: tl)
|
||||||
|
with (hd'' ++ [b0;b1;b0;b1;b1;b0;b1;b0;b0;b1;b0;b1;b1;b0;b1;b0] ++ tl) in H.
|
||||||
|
pose (s := [b0;b1;b0;b1;b1;b0;b1;b0;b0;b1;b0;b1;b1;b0;b1;b0]). fold s in H.
|
||||||
|
assert (even (length hd'') = true). unfold hd''.
|
||||||
|
|
||||||
|
rewrite removelast_firstn_len. rewrite Y''.
|
||||||
|
replace (pred (length (b10::hd))) with (length hd).
|
||||||
|
rewrite firstn_length_le. simpl in Q. rewrite Q. reflexivity.
|
||||||
|
rewrite Y''. apply Nat.le_succ_diag_r. reflexivity.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_morphism_app : forall (l1 l2 : list bool),
|
||||||
|
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
|
||||||
|
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
|
||||||
|
tm_morphism l = hd ++ tl
|
||||||
|
-> even (length hd) = true
|
||||||
|
-> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
|
||||||
|
Lemma tm_morphism_app3 : forall (l hd tl : list bool),
|
||||||
|
tm_morphism l = hd ++ tl
|
||||||
|
-> even (length hd) = true
|
||||||
|
-> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
False, True, True, False, True, False, False, True, True, False, False, True, False, True, True, False]'
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user