proposition: Lemma prop_check_slt: forall bs1 bs2, length bs1 = length bs2 -> RAWBITVECTOR_LIST.slt_list_big_endian (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) = interp_carry (slt_big_endian_lit_list bs1 bs2).
proof: Proof. intros. case bs1 in *. simpl. specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H0; now rewrite not_true_iff_false in H0. case bs2 in *. now contradict H. rewrite !map_cons. case bs1 in *. simpl. case bs2 in *. simpl. now rewrite Lit.interp_neg. now contradict H. case bs2 in *. now contradict H. unfold slt_big_endian_lit_list. unfold RAWBITVECTOR_LIST.slt_list_big_endian. rewrite !map_cons. unfold interp_carry. fold interp_carry. rewrite <- !map_cons. rewrite Lit.interp_neg. rewrite prop_check_ult. now apply f_equal. simpl. now inversion 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