Update
This commit is contained in:
parent
a74abadbc6
commit
f3aa7478fb
@ -1344,15 +1344,13 @@ Proof.
|
|||||||
assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
|
assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
|
||||||
destruct J.
|
destruct J.
|
||||||
- rewrite <- e in H.
|
- rewrite <- e in H.
|
||||||
assert (exists (hd a tl : list bool),
|
assert (J: exists (hd a tl : list bool),
|
||||||
tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a).
|
tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a).
|
||||||
exists hd. exists a. exists tl. split; assumption.
|
exists hd. exists a. exists tl. split; assumption.
|
||||||
assert (exists (hd2 b tl2 : list bool),
|
apply tm_step_cube7 in J.
|
||||||
tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b).
|
destruct J. destruct H0. destruct H0. destruct H0.
|
||||||
generalize H0. apply tm_step_cube7.
|
assert (0 < 0). generalize H1. generalize H0. apply tm_step_cube2.
|
||||||
destruct H1. destruct H1. destruct H1. destruct H1.
|
apply Nat.lt_irrefl in H2. contradiction H2.
|
||||||
assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2.
|
|
||||||
apply Nat.lt_irrefl in H3. contradiction H3.
|
|
||||||
- assumption.
|
- assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user