proposition: Lemma prop_check_ult: forall bs1 bs2, length bs1 = length bs2 -> RAWBITVECTOR_LIST.ult_list_big_endian (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) = interp_carry (ult_big_endian_lit_list bs1 bs2).
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1 ]. - intros. simpl in *. symmetry in H; rewrite empty_list_length in H. specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H0; now rewrite not_true_iff_false in H0. - intros. case_eq bs2. intros. rewrite H0 in *. now contradict H. intros. rewrite H0 in *. inversion H. rewrite !map_cons. simpl. case xsbs1 in *. simpl. case l in *. simpl. now rewrite Lit.interp_neg. now contradict H2. case l in *. simpl. now contradict H2. rewrite !map_cons. unfold interp_carry. fold interp_carry. specialize (@IHbs1 (i1 :: l)). rewrite !map_cons in IHbs1. rewrite Lit.interp_neg. now rewrite IHbs1. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance