proposition: Lemma check_concat_bvconcat: forall bs1 bs2 bsres , check_concat bs1 bs2 bsres = true -> (RAWBITVECTOR_LIST.bv_concat (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) = (map (Lit.interp rho) bsres)).
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1 ]. - intros. simpl. unfold check_concat in H. simpl in H. case_eq (forallb2 eq_carry_lit (lit_to_carry bs2) bsres); intros. rewrite concat_nil in H. apply prop_eq_carry_lit2 in H0. unfold RAWBITVECTOR_LIST.bv_concat. rewrite concat_nil. now rewrite prop_interp_carry3 in H0. unfold RAWBITVECTOR_LIST.bv_concat. rewrite concat_nil. rewrite concat_nil in H. rewrite H0 in H. now contradict H. - intros. unfold check_concat in H. case_eq (forallb2 eq_carry_lit (lit_to_carry (bs2 ++ xbs1 :: xsbs1)) bsres); intros. apply prop_eq_carry_lit2 in H0. rewrite prop_interp_carry3 in H0. simpl in H0. simpl. unfold RAWBITVECTOR_LIST.bv_concat. specialize (concat_map (Lit.interp rho)). intros. rewrite <- H0. simpl. rewrite <- !check_concat_map. apply f_equal. now simpl. 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