Update
This commit is contained in:
parent
25a6956538
commit
c7bad77004
|
@ -1617,11 +1617,6 @@ Proof.
|
||||||
rewrite app_length. rewrite Nat.even_add.
|
rewrite app_length. rewrite Nat.even_add.
|
||||||
rewrite I'. rewrite J'. reflexivity.
|
rewrite I'. rewrite J'. reflexivity.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
destruct n. inversion V. inversion H10.
|
destruct n. inversion V. inversion H10.
|
||||||
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
|
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
|
||||||
|
|
||||||
|
@ -1675,6 +1670,40 @@ Proof.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)).
|
||||||
|
pose (a'' := firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd'))
|
||||||
|
(tm_step n))).
|
||||||
|
pose (tl'' := skipn (Nat.div2 (length hd') + length a') (tm_step n)).
|
||||||
|
fold hd'' in H. fold a'' in H. fold tl'' in H.
|
||||||
|
|
||||||
|
assert (length hd'' = Nat.div2 (length hd')). unfold hd''. rewrite H4'.
|
||||||
|
rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
|
||||||
|
replace (min (Nat.div2 (length hd')) (length (tm_step n)))
|
||||||
|
with (min (length (tm_step n)) (Nat.div2 (length hd'))).
|
||||||
|
rewrite Nat.min_comm. rewrite Nat.min_assoc. rewrite Nat.min_id.
|
||||||
|
reflexivity. rewrite Nat.min_comm. reflexivity.
|
||||||
|
|
||||||
|
assert (length a'' = Nat.div2 (length a')). unfold a''. rewrite H5'.
|
||||||
|
rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
|
||||||
|
rewrite Nat.min_comm. rewrite <- H9.
|
||||||
|
replace
|
||||||
|
(min (Nat.div2 (length a')) (length (skipn (length hd'') (tm_step n))))
|
||||||
|
with
|
||||||
|
(min (length (skipn (length hd'') (tm_step n))) (Nat.div2 (length a'))).
|
||||||
|
rewrite Nat.min_assoc. rewrite Nat.min_id. reflexivity.
|
||||||
|
rewrite Nat.min_comm. reflexivity.
|
||||||
|
|
||||||
|
assert (length tl'' = Nat.div2 (length tl')). unfold tl''. rewrite H3'.
|
||||||
|
rewrite tm_morphism_length_half. rewrite app_length.
|
||||||
|
symmetry. rewrite Nat.div2_div.
|
||||||
|
rewrite app_length. rewrite map_length. rewrite rev_length.
|
||||||
|
replace (length a' + length a') with (length a' * 2).
|
||||||
|
rewrite Nat.div_add. rewrite <- Nat.div2_div. reflexivity. easy.
|
||||||
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue