proposition: Lemma id_of_kind_select_children x s k i : x \in [seq id_of_kind (negk k) j | j <- select_children H s k i] = tanner_rel H (id_of_kind k i) x && (x \notin s).
proof: Proof. case Hx: (x \in _). move/mapP: Hx => [y Hy] ->. rewrite select_children_spec in Hy. move/andP: Hy => [] ->. by rewrite in_cons /= => /norP [_] ->. symmetry. apply/contraFF: Hx => Hex. apply/mapP. destruct k; destruct x as [x|x]. - by rewrite tanner_relE in Hex. - exists x => //; by rewrite select_children_spec Hex. - exists x => //; by rewrite select_children_spec Hex. - by rewrite tanner_relE in Hex. 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