proposition: Lemma zextend_interp_main: forall bs1 bsres (n i: N), check_zextend bs1 bsres i = true -> @RAWBITVECTOR_LIST.bv_zextn n i (map (Lit.interp rho) bs1) = map (Lit.interp rho) bsres.
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1]. - intros. simpl. unfold check_zextend in H. simpl in H. case_eq (forallb2 eq_carry_lit (lit_to_carry (zextend_lit [] (N.to_nat i))) bsres). intros. apply prop_eq_carry_lit2 in H0. rewrite prop_interp_carry3 in H0. simpl in H0. unfold RAWBITVECTOR_LIST.bv_zextn. now rewrite zextend_interp_empty. intros. rewrite H0 in H. now contradict H0. - intros. unfold RAWBITVECTOR_LIST.bv_zextn, check_zextend in H. case_eq ( forallb2 eq_carry_lit (lit_to_carry (zextend_lit (xbs1 :: xsbs1) (N.to_nat i))) bsres); intros. apply prop_eq_carry_lit2 in H0. rewrite prop_interp_carry3 in H0. simpl in H0. simpl. unfold RAWBITVECTOR_LIST.bv_zextn in *. case_eq (N.to_nat i). intros. rewrite H1 in H0. now simpl in *. intros. rewrite H1 in H0. rewrite <- H0. rewrite <- zextend_interp_all. simpl. assert (Lit.interp rho Lit._false = false). { specialize (Lit.interp_false rho wf_rho). intros. rewrite <- not_true_iff_false. unfold not in *. intros. now apply H2. } reflexivity. 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