Update
This commit is contained in:
parent
dd2bd9d4f5
commit
39b4aa0626
@ -1264,7 +1264,7 @@ Proof.
|
|||||||
apply H1 in H2. rewrite H2 at 1. easy. easy.
|
apply H1 in H2. rewrite H2 at 1. easy. easy.
|
||||||
rewrite nth_error_nth' with (d := false). easy.
|
rewrite nth_error_nth' with (d := false). easy.
|
||||||
rewrite tm_size_power2. apply lt_split_bits.
|
rewrite tm_size_power2. apply lt_split_bits.
|
||||||
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
|
assumption. assumption. assumption.
|
||||||
|
|
||||||
apply tm_step_stable. apply lt_split_bits.
|
apply tm_step_stable. apply lt_split_bits.
|
||||||
assumption. assumption. assumption.
|
assumption. assumption. assumption.
|
||||||
|
Loading…
Reference in New Issue
Block a user