fact: Fixpoint sumprod_down {k} (n : tn_tree' k R2 unit) (from_above : option R2) : tn_tree' k R2 R2 := let (arg0, down') := push_init from_above in let args := seqs_but1 arg0 (map up (children n)) in let funs := map (fun n' l => sumprod_down n' (Some (alpha_beta (node_tag n) l))) (children n) in let children' := apply_seq funs args in Node (node_id n) (node_tag n) children' (up n) down'.
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