Update
This commit is contained in:
parent
e946fefe47
commit
e845183004
@ -1324,11 +1324,9 @@ Lemma tm_step_cube7 : forall (n : nat),
|
||||
/\ 0 < length b.
|
||||
Proof.
|
||||
intros n. intro H.
|
||||
induction n.
|
||||
- destruct H. destruct H. destruct H. destruct H.
|
||||
exists x. exists x0. exists x1. split; assumption.
|
||||
- destruct H. destruct H. destruct H. destruct H.
|
||||
assert (J: exists (hd2 b2 tl2 : list bool),
|
||||
induction n; destruct H; destruct H; destruct H; destruct H.
|
||||
- exists x. exists x0. exists x1. split; assumption.
|
||||
- assert (J: exists (hd2 b2 tl2 : list bool),
|
||||
tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2
|
||||
/\ 0 < length b2).
|
||||
generalize H0. generalize H. apply tm_step_cube6.
|
||||
|
Loading…
Reference in New Issue
Block a user