proposition: Lemma prop_check_bbc: forall bv bs, (check_bbc bv bs = true) -> (forall i, (i < (length bs) )%nat -> (Lit.interp rho (nth i bs 1)) = nth i bv false).
proof: Proof. intro bv. induction bv. intros bs. case bs. intros. do 2 rewrite nth_nil. easy. simpl. easy. intros bs. case bs. simpl. easy. intros b l Hc i Hlen. case i in *. simpl. simpl in Hc. case_eq (Lit.is_pos b). intro Hposb. rewrite Hposb in Hc. case_eq (t_form .[ Lit.blit b]); try (intros; rewrite H in Hc; now contradict Hc). intros Hb. rewrite Hb in Hc. generalize (rho_interp (Lit.blit b)). rewrite Hb. simpl. intro Hbb. unfold Lit.interp, Var.interp. rewrite Hbb, Hposb. case a in *. trivial. now contradict Hc. intro Hb. rewrite Hb in Hc. generalize (rho_interp (Lit.blit b)). rewrite Hb. simpl. intro Hbb. unfold Lit.interp, Var.interp. rewrite Hbb, Hposb. case a in *. now contradict Hc. trivial. intro Hposb. rewrite Hposb in Hc. now contradict Hc. simpl. apply IHbv. simpl in Hc. case (Lit.is_pos b) in Hc; try now contradict Hc. case (t_form .[ Lit.blit b]) in Hc; try now contradict Hc. case a in Hc; try now contradict Hc. exact Hc. case a in Hc; try now contradict Hc. exact Hc. simpl in Hlen. lia. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance