proposition: Lemma msg_nil i1 i2 (i : option id') {k} t : (i1 \notin i ++ labels t) || (i2 \notin i ++ labels t) -> size (@msg _ _ i1 i2 i k t) = 0.
proof: Proof. move: k t i. refine (children_ind _). move=> k [id0 tag0 ch0 up0 down0] /= IH i. rewrite !mem_cat !in_cons. case: ifP => Hi1 /=. rewrite -(eqP Hi1) !in_cons eqxx /=. case: ifP => Hi2' //. by rewrite orbT. case: ifP => Hi2 /=. rewrite -(eqP Hi2) !in_cons eqxx /=. rewrite !orbF => Hi1'. case: ifP => {}Hi1 //. by rewrite Hi1 orbT in Hi1'. rewrite size_flatten. move=> Hch. rewrite /shape. rewrite -map_comp. rewrite sumnE. rewrite big_seq big1 //= => i' /mapP[l Hl] -> /=. apply/IH => //. case Hi1l: (i1 \notin _); first by []. case Hi2l: (i2 \notin _); first by []. simpl; symmetry. move /orP: Hch => [Hch | Hch]; apply/contraNF: Hch => _. move: Hi1l; rewrite mem_cat in_cons. case Hi1i: (i1 \in (i : seq id')) => //=. case Hi10: (i1 == id0) => //= Hi1l. apply/flattenP. exists (labels l). by apply (map_f labels). by apply (negbFE Hi1l). move: Hi2l; rewrite mem_cat in_cons. case Hi2i: (i2 \in (i : seq id')) => //=. have [//|/= Hi20 Hi2l] := eqVneq i2 id0. apply/flattenP. exists (labels l). exact: (map_f labels). exact: (negbFE Hi2l). 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