proposition: Lemma apply_seqs_but1 {I U V : eqType} {k} {D} (f : tn_tree I k U V -> seq R2 -> D) g in0 cl : uniq (map node_id cl) -> apply_seq (map f cl) (seqs_but1 in0 (map g cl)) = [seq (f c (in0 ++ [seq g d | d <- cl & node_id d != node_id c])) | c <- cl].
proof: Proof. rewrite {1}(_ : in0 = in0 ++ map g [::]); last by rewrite cats0. set inl := [::]. rewrite {1 4}(_ : cl = inl ++ cl) //. elim: cl inl => [|c cl IH] inl //= Hun. rewrite /apply_seq /=. congr (f c _ :: _). rewrite -catA -map_cat; congr (_ ++ map _ _). rewrite filter_cat /= eqxx /= -filter_cat. apply/esym/all_filterP/allP => i. rewrite map_cat cat_uniq /= in Hun. case/and4P : Hun => _ /norP [] Hinl _ Hcl _. case/boolP : (node_id i == node_id c) => //= /eqP Hic. rewrite mem_cat => /orP [] /(map_f node_id). - by rewrite Hic (negbTE Hinl). - by rewrite Hic (negbTE Hcl). rewrite (_ : inl ++ (c :: cl) = (inl ++ [:: c]) ++ cl); last by rewrite -catA. rewrite -IH; last by rewrite -catA. by rewrite rcons_cat -cats1 map_cat. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo