proposition: Theorem pbadd_prop2 : forall a1 l1 l2, pbfree l1 l2 -> Permutation (compute_pbcode (pbadd a1 l2 l1)) ((a1, l1) :: compute_pbcode l2).
proof: Proof. intros a1 l1 l2 H; generalize a1; elim H; clear H a1 l1 l2; simpl in |- *; auto. intros b l a1; rewrite pbadd_prop1; simpl in |- *. apply Permutation_trans with (((a1, true :: l) :: []) ++ map (fun v => match v with | (a0, b1) => (a0, false :: b1) end) (compute_pbcode b)); auto. intros b l H H0 a1. apply Permutation_trans with (map (fun v => match v with | (a0, b1) => (a0, false :: b1) end) ((a1, l) :: compute_pbcode b)); auto. apply Permutation_map; auto. intros b l a1; rewrite pbadd_prop1; simpl in |- *; auto. intros b l H H0 a1. apply Permutation_trans with (map (fun v => match v with | (a0, b1) => (a0, true :: b1) end) ((a1, l) :: compute_pbcode b)); auto. apply Permutation_map; auto. intros b c l H H0 a1. apply Permutation_trans with (map (fun v => match v with | (a0, b1) => (a0, false :: b1) end) ((a1, l) :: compute_pbcode b) ++ map (fun v => match v with | (a0, b1) => (a0, true :: b1) end) (compute_pbcode c)); auto. apply Permutation_app; auto. apply Permutation_map; auto. intros b c l H H0 a1. apply Permutation_trans with (map (fun v => match v with | (a0, b1) => (a0, false :: b1) end) (compute_pbcode c) ++ map (fun v => match v with | (a0, b1) => (a0, true :: b1) end) ((a1, l) :: compute_pbcode b)); auto. apply Permutation_app; auto. apply Permutation_map; auto. apply Permutation_trans with (map (fun v => match v with | (a0, b1) => (a0, true :: b1) end) ((a1, l) :: compute_pbcode b) ++ map (fun v => match v with | (a0, b1) => (a0, false :: b1) end) (compute_pbcode c)); auto; simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)