proposition: Lemma Invariant_t_O : BV_to_nat (appbv (stripbv (R1 0) size) (R2 0)) = BV_to_nat V2 * BV_to_nat (truncbv V1 0).
proof: Proof. intros. simpl in |- *. rewrite BV_to_nat_app2. rewrite (trunc_O bool). rewrite <- length_V1_size. rewrite (strip_all bool). rewrite length_V1_size. simpl in |- *. elim plus_n_O. elim mult_n_O. rewrite BV_null_nat. trivial with arith. Qed.
imports: Definitions LemPrelim AdderProof