proposition: Lemma prop_check_slt2: forall bs1 bs2 bsres, length bs1 = length bs2 -> check_slt bs1 bs2 bsres = true -> interp_carry (slt_big_endian_lit_list (rev bs1) (rev bs2)) = Lit.interp rho bsres.
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1]. - intros. case bs2 in *. unfold check_slt in H0. simpl in *. case_eq (Lit.is_pos bsres). intros Hbsres. rewrite Hbsres in H0. case (Lit.is_pos bsres) in H0; rewrite eqb_spec in H0; now rewrite H0. intros. rewrite H1 in H0. now contradict H0. now contradict H. - intros. case bs2 in *. now contradict H. simpl. unfold check_slt, slt_lit_list in H0. simpl in H0. case_eq (Lit.is_pos bsres). intros Hbsres. rewrite Hbsres in H0. now apply prop_eq_carry_lit. intros. rewrite H1 in H0. now contradict H0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance