proposition: Lemma push_init_spec s i : push_init (down_msg s i) = ((omap (msg_spec' ^~ i) (prec_node s) : seq R2), oapp (msg_spec' ^~ i) (R1,R1) (prec_node s)).
proof: Proof. by destruct s. 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