proposition: Theorem inpb_compute_ex : forall a p, inpb (pbleaf a) p -> exists l, In (a, l) (compute_pbcode p).
proof: Proof. intros a p; elim p; simpl in |- *; auto. intros a0 H; inversion H. exists []; auto. intros p0 H H0; case H; auto. inversion H0; auto. intros x1; elim (compute_pbcode p0); simpl in |- *; auto. intros HH; case HH. intros a0 l H1 [H2| H2]; auto. exists (false :: x1); left; rewrite H2; auto. case H1; auto. intros x H3; exists x; auto. intros p0 H H0; case H; auto. inversion H0; auto. intros x1; elim (compute_pbcode p0); simpl in |- *; auto. intros HH; case HH. intros a0 l H1 [H2| H2]; auto. exists (true :: x1); left; rewrite H2; auto. case H1; auto. intros x H3; exists x; auto. intros p0 H p1 H0 H1; inversion H1. case H; auto. intros x Hx; exists (false :: x). apply in_or_app; left; auto. change (In ((fun v => match v with | (a1, b1) => (a1, false :: b1) end) (a, x)) (map (fun v => match v with | (a1, b1) => (a1, false :: b1) end) (compute_pbcode p0))) in |- *; apply in_map; auto. case H0; auto. intros x Hx; exists (true :: x). apply in_or_app; right; auto. change (In ((fun v => match v with | (a1, b1) => (a1, true :: b1) end) (a, x)) (map (fun v => match v with | (a1, b1) => (a1, true :: b1) end) (compute_pbcode p1))) in |- *; apply in_map; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)