proposition: Lemma labels_build_tree_rec h s k i : forall a, a \in labels (build_tree_rec H rW h s k i) -> uniq_path (tanner_rel H) (id_of_kind k i) s -> exists p, uniq_path (tanner_rel H) a (p ++ s) /\ last a p = id_of_kind k i /\ forall b, b \in p -> b \in labels (build_tree_rec H rW h s k i).
proof: Proof. move: s k i. elim: h => [|h Hh] s k i a. rewrite /= mem_seq1 => /eqP -> Hi; by exists [::]. rewrite [a \in _]/= in_cons -map_comp => Ha Hi. case Hai: (a == id_of_kind k i) => /= in Ha. rewrite (eqP Hai) in Hi *; by exists [::]. move /flattenP: Ha => [l] /mapP [x Hx ->] Ha. have Hsc := Hx. rewrite select_children_spec /= in Hx. move /andP: Hx => [Hx Hxs]. have Hi': uniq_path (tanner_rel H) (id_of_kind (negk k) x) (id_of_kind k i ::s). rewrite /uniq_path /= Hxs. move /andP: Hi => /= [-> ->]. by rewrite sym_tanner_rel Hx. have [p [Hp [Hal Hl]]] := Hh _ _ _ _ Ha Hi'. exists (rcons p (id_of_kind k i)). split. by rewrite cat_rcons. split. by rewrite last_rcons. move=> b /=. rewrite mem_rcons !in_cons -map_comp. set f := labels \o build_tree_rec H rW h (id_of_kind k i :: s) (negk k). case: (b == id_of_kind k i) => //= Hb. apply/flattenP => /=. exists (f x); by [apply (map_f f) | apply Hl]. 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