proposition: Lemma select_children_def k j s i : let a := id_of_kind k i in let inj := id_of_kind (negk k) in uniq_path (tanner_rel H) a s -> prec_node s = Some (inj j) -> select_children H s k i = enum ([set x | tanner_rel H a (inj x)] :\ j).
proof: Proof. move=> a inj Hun Hj. destruct s as [|b s]; first by []. move: Hj Hun => /= [] => -> {b}Hun. rewrite -enum_select_children. rewrite /enum_mem. apply eq_filter => x. rewrite /= !inE /=. rewrite select_children_spec. rewrite !in_cons. rewrite (inj_eq (@id_of_kind_inj _ _ _)). rewrite (eq_sym (id_of_kind _ x)) id_of_kind_neq /=. symmetry. rewrite andbC sym_tanner_rel. case Hix: (tanner_rel _ _ _) => //=. by rewrite negb_or (ext_uniq_path tanner_acyclic Hun) // andbT. 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