proposition: Theorem clauses_update_valid: forall p z c cs s, valid_lit (L p z) s -> ordered cs -> ordered_clause c -> (forall z1, In z1 ref_list -> z1 <> z -> In (L p z1) c) -> valid cs s -> valid (clauses_update (L p z) c cs) (update p z s).
proof: Proof. Proof with auto with datatypes. intros p z c cs s (H1, (H2, H3)) H4 H5 H6; generalize H4; elim cs; simpl; auto; clear cs H4. intros _ _ n1 c1 H7; case H7. intros (n1, c1) cs Rec H4 H7. generalize (lit_is_in_correct (L p z) c1); case (lit_is_in (L p z) c1); intros H. apply Rec... intros n2 c2 HH; apply (H4 n2 c2)... intros n2 c2 H8; apply (H7 n2 c2)... assert (E1: ordered_clause c1). apply (H4 n1 c1)... assert (E2: valid_clause c1 s). apply (H7 n1 c1)... apply clause_insert_valid... apply valid_update... apply lit_rm_valid... intros z1 HH; case (eq_nat z z1); intros H8; subst... intros H8; case H... case (lit_rm_in (L p z1) c c1)... intros tmp _; case tmp... intros H9; case (lit_rm_in (L p z1) c c1)... intros tmp _; case tmp... apply Rec... intros n2 c2 H8; apply (H4 n2 c2)... intros n2 c2 H8; apply (H7 n2 c2)... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia