fact: Fixpoint estimation {k} (n : tn_tree' k R2 R2) := let l := flatten (map estimation (children n)) in if node_tag n is Var _ then (node_id n, normalize (beta_op (up n) (down n))) :: l else l .
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