fact: Fixpoint sumprod_up {k} (n : tn_tree' k unit unit) : tn_tree' k R2 unit := let children' := map sumprod_up (children n) in let up' := alpha_beta (node_tag n) (map up children') in Node (node_id n) (node_tag n) children' up' tt.
imports: Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext f2 subgraph_partition tanner fdist channel pproba linearcode ssralg_ext tanner_partition summary ldpc checksum