Update
This commit is contained in:
parent
a3e8c15627
commit
790cd92748
@ -2100,7 +2100,7 @@ Lemma tm_step_non_proper_palindrome_16 :
|
|||||||
forall (n : nat) (hd a tl : list bool),
|
forall (n : nat) (hd a tl : list bool),
|
||||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
-> length a = 8
|
-> length a = 8
|
||||||
-> skipn (length hd - 8) hd = rev (firstn 8 tl).
|
-> exists x, a = [x; negb x; negb x; x; negb x; x; x; negb x].
|
||||||
Proof.
|
Proof.
|
||||||
intros n hd a tl. intros H I.
|
intros n hd a tl. intros H I.
|
||||||
|
|
||||||
@ -2223,6 +2223,16 @@ Proof.
|
|||||||
contradiction n1. reflexivity. reflexivity. reflexivity.
|
contradiction n1. reflexivity. reflexivity. reflexivity.
|
||||||
rewrite H8 in H.
|
rewrite H8 in H.
|
||||||
|
|
||||||
|
assert (b6 = negb b5). destruct b5; destruct b6.
|
||||||
|
contradiction H1. reflexivity. reflexivity. reflexivity.
|
||||||
|
contradiction H1. reflexivity. rewrite H9 in H.
|
||||||
|
|
||||||
|
exists b5. rewrite H4. rewrite H3. rewrite H8. rewrite H7. rewrite H5.
|
||||||
|
rewrite H0. rewrite H9. reflexivity.
|
||||||
|
reflexivity. inversion I. assumption. rewrite I.
|
||||||
|
rewrite <- Nat.le_succ_l. apply Nat.le_succ_diag_r.
|
||||||
|
Qed.
|
||||||
|
|
||||||
(*
|
(*
|
||||||
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