proposition: Lemma check_form_correct : forall t_form, check_form t_form -> ((PArray.default t_form = Ftrue /\ wf t_form) /\ Valuation.wf (interp_state_var t_form)).
proof: Proof. unfold is_true, check_form;intros t;rewrite !andb_true_iff. intros H;decompose [and] H;clear H; assert (PArray.default t = Ftrue) by (apply is_Ftrue_correct;trivial). repeat split;trivial. rewrite wf_interp_form;trivial. apply is_Ftrue_correct in H4;trivial;rewrite H4;reflexivity. rewrite wf_interp_form;trivial. apply is_Ffalse_correct in H3;trivial;rewrite H3;discriminate. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList