proposition: Lemma check_shl_bvshl: forall bs1 bs2 bsres , check_shl bs1 bs2 bsres = true -> (RAWBITVECTOR_LIST.bv_shl (map (Lit.interp rho) bs1) bs2 = (map (Lit.interp rho) bsres)).
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1 ]. - intros. simpl. unfold check_shl, shl_lit_be in H. case_eq (Nat.eqb (@length int []) (length bs2)); intros. rewrite Nat.eqb_eq in H0. rewrite <- H0 in H. simpl in H. rewrite nshl_lit_empty in H. case_eq bsres; intros. simpl. now rewrite bv_shl_empty. subst; now contradict H. rewrite H0 in H; now contradict H. - intros. unfold check_shl in H. case_eq (Nat.eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros. rewrite H0 in H. case_eq ( forallb2 eq_carry_lit (lit_to_carry (shl_lit_be (xbs1 :: xsbs1) bs2)) bsres); intros. apply prop_eq_carry_lit2 in H1. rewrite prop_interp_carry3 in H1. unfold RAWBITVECTOR_LIST.bv_shl. rewrite Nat.eqb_eq in H0. unfold RAWBITVECTOR_LIST.size. rewrite !map_length. rewrite H0, N.eqb_refl. now rewrite <- H1, shl_interp. rewrite H1 in H; now contradict H. rewrite H0 in H; now contradict H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance