proposition: Lemma R1_lem : forall t : nat, t <= size -> truncbv (R1 t) (size - t) = stripbv V1 t.
proof: Proof. simple induction t. elim minus_n_O. rewrite <- (length_R1 0). intro. rewrite (trunc_all bool). rewrite (strip_O bool). auto with arith. auto with arith. intros. rewrite R1_eq2. rewrite highs_is_strip. rewrite (trunc_app bool). rewrite (trunc_strip bool). rewrite (length_strip bool). rewrite length_R1. replace (size - S n - (size - 1)) with 0. rewrite (trunc_O bool). replace (1 + (size - S n)) with (size - n). rewrite (app_v_nil bool). unfold truncbv in H. rewrite H. rewrite (strip_strip bool). rewrite plus_comm. simpl in |- *. auto with arith. apply le_Sn_le; exact H0. simpl in |- *. rewrite minus_Sn_m. simpl in |- *. trivial with arith. exact H0. symmetry in |- *. apply minus_le_O. apply le_minus_minus. auto with arith. apply le_Sn_le; exact H0. rewrite length_R1. apply le_SO_size. apply le_Sn_le; exact H0. Qed.
imports: Definitions