Update
This commit is contained in:
parent
09b3f8f05c
commit
a3e8c15627
|
@ -2209,6 +2209,20 @@ Proof.
|
||||||
reflexivity. contradiction H6. reflexivity. reflexivity.
|
reflexivity. contradiction H6. reflexivity. reflexivity.
|
||||||
rewrite H7 in H.
|
rewrite H7 in H.
|
||||||
|
|
||||||
|
assert ({b=b6} + {~ b=b6}). apply bool_dec. destruct H8. rewrite e in H.
|
||||||
|
replace (hd ++ [b6; b6; b6; b5; b6; b5; b5; b6]
|
||||||
|
++ [b6; b5; b5; b6; b5; b6; b6; b6] ++ tl)
|
||||||
|
with (hd ++ [b6] ++ [b6] ++ [b6]
|
||||||
|
++ [b5; b6;b5;b5;b6;b6; b5; b5; b6; b5; b6; b6; b6] ++ tl) in H.
|
||||||
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
||||||
|
apply Nat.lt_0_1. reflexivity.
|
||||||
|
|
||||||
|
assert (b = b5). destruct b; destruct b5; destruct b6.
|
||||||
|
reflexivity. reflexivity. contradiction n1. reflexivity.
|
||||||
|
contradiction H1. reflexivity. contradiction H1. reflexivity.
|
||||||
|
contradiction n1. reflexivity. reflexivity. reflexivity.
|
||||||
|
rewrite H8 in H.
|
||||||
|
|
||||||
(*
|
(*
|
||||||
Lemma tm_step_proper_palindrome_center :
|
Lemma tm_step_proper_palindrome_center :
|
||||||
forall (m n k : nat) (hd a tl : list bool),
|
forall (m n k : nat) (hd a tl : list bool),
|
||||||
|
|
Loading…
Reference in New Issue
Block a user