proposition: Theorem pbfree_pbadd_prop2 : forall a l1 l2 l3, pbfree l1 l3 -> ~ is_prefix l2 l1 -> ~ is_prefix l1 l2 -> pbfree l1 (pbadd a l3 l2).
proof: Proof. intros a l1 l2; generalize a l1; elim l2; simpl in |- *; auto. intros a0 l0 l3 H H0; case H0; auto. intros a0; case a0. intros l H a1 l0; case l0. intros l3 H0; inversion H0. intros b; case b; simpl in |- *; auto. intros l3 l4; case l4; simpl in |- *; auto. intros a2 H0 H1 H2; apply pbfree_right2. apply pbfree_pbadd_prop1; auto. intros p H0 H1 H2; apply pbfree_node2. apply pbfree_pbadd_prop1; auto. intros a2 H0 H1 H2; apply pbfree_right2. apply H; auto. inversion H0; auto. intros p p0 H0 H1 H2; apply pbfree_node2. apply H; auto. inversion H0; auto. intros l3 l4; case l4; simpl in |- *; auto. intros p H0 H1 H2; apply pbfree_node1. inversion H0; auto. intros p p0 H0 H1 H2; apply pbfree_node1. inversion H0; auto. intros l H a1 l0; case l0. intros l3 H0; inversion H0. intros b; case b; simpl in |- *; auto. intros l3 l4; case l4; simpl in |- *; auto. intros p H0 H1 H2; apply pbfree_node2. inversion H0; auto. intros p p0 H0 H1 H2; apply pbfree_node2. inversion H0; auto. intros l3 l4; case l4; simpl in |- *; auto. intros a2 H0 H1 H2; apply pbfree_left2. apply pbfree_pbadd_prop1; auto. intros a2 H0 H1 H2; apply pbfree_left2. apply H; auto. inversion H0; auto. intros p H0 H1 H2; apply pbfree_node1. apply pbfree_pbadd_prop1; auto. intros p p0 H0 H1 H2; apply pbfree_node1. apply H; auto. inversion H0; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)