proposition: Lemma graph_sumprod_down k (t : tn_tree id' k R2 unit) dn : graph t =2 graph (sumprod_down t dn).
proof: Proof. move=> a b. move: k t dn; refine (children_ind _); move=> k t IH dn. destruct t as [id0 tag0 ch0 up0 down0]; simpl in *. destruct (push_init dn); simpl. case Ha: (id0 == a). rewrite -(map_apply_seq_eq (g:=node_id)) //. move=> c x Hc. by destruct c. by rewrite size_seqs_but1 size_map eqxx. case Hb: (id0 == b). rewrite -(map_apply_seq_eq (g:=node_id)) //. move=> c x Hc. by destruct c. by rewrite size_seqs_but1 size_map eqxx. elim: ch0 => [|c cl IHc] in IH l * => //=. rewrite -IHc; last first. by move=> t' Ht'; apply IH; rewrite in_cons Ht' orbT. by rewrite -IH // in_cons eqxx. 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