proposition: Lemma msg_spec_alpha_beta a b : tanner_rel H a b -> msg_spec' a b = alpha_beta (tag_of_id rW a) [seq msg_spec' c a | c in finset (tanner_rel H a) :\ b].
proof: Proof. destruct a, b; rewrite //= => Hij. - by rewrite tanner_relE in Hij. - rewrite -alpha_def; last by rewrite VnextE sym_tanner_rel. rewrite -imset_set1 (@kind_filter _ kf). set x := [set x | _]. suff : 'V o = x by move=> ->. by apply/setP => i; rewrite inE /= -VnextE. - rewrite -beta_def -imset_set1 (@kind_filter _ kv) /=. congr beta. rewrite /image_mem /enum_mem. congr map. apply eq_filter => x. by rewrite !inE /= -VnextE -FnextE. - by rewrite tanner_relE in Hij. 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