proposition: Lemma estimation_alpha n0 h (s : seq id') k (i : ord_of_kind m n' k) : let t := build_computed_tree h s i in (#|id'| - #|s| <= h)%nat -> uniq_path (tanner_rel H) (id_of_kind k i) s -> inr n0 \in labels t -> get_esti n0 (estimation t) = [:: normalize (beta (rW n0) [seq (p01 (alpha' m1 n0) n0) | m1 in 'F n0])].
proof: Proof. elim: h => [|h IH] in s k i *. move=> t Ht. have His: id_of_kind k i \in s by apply seq_full. by rewrite /uniq_path /= His andbF. move=> t Hh Hun Hn0. have Hh': (#|id'| - #|id_of_kind k i :: s| <= h)%nat. move/andP/proj2: Hun => Hun. by apply card_uniq_seq_decr. case Hid: (node_id t == inr n0). destruct k; rewrite //= Hid /=. congr (_ :: _). congr normalize. case/eqP: Hid => Hid; subst n0. destruct s as [|s s0]. rewrite -/set0 -(imset0 (id_of_kind (negk kv))) kind_filter /=. rewrite setD0 Monoid.mulm1. congr beta. rewrite /image_mem /enum_mem. apply eq_in_map_seqs => //. have ->: Finite.enum [finType of 'I_m] = ord_enum m. by rewrite unlock. apply eq_filter => x; by rewrite /= !inE /= -VnextE -FnextE. destruct s; [ | ]; last first. by rewrite tanner_relE in Hun. rewrite set1F -imset_set1 (kind_filter (k:=kv)). rewrite !beta_map -Monoid.mulmA; congr beta_op. rewrite big_filter (eq_bigr (fun j => msg_spec' (inl j) (inr i))) //. rewrite Monoid.mulmC -big_filter. rewrite -msg_spec_alpha_beta; last first. rewrite sym_tanner_rel. by move/andP/proj1: Hun => /= /andP/proj1. rewrite -(big_seq1 beta_op_monoid_law o (fun j => msg_spec' (inl j) (inr i))). rewrite -big_cat. apply/perm_big/uniq_perm. - rewrite /= filter_uniq. by rewrite mem_filter /= !inE /= eqxx. by rewrite -enumT enum_uniq. - by rewrite enum_uniq. move=> j /=. rewrite in_cons mem_filter /= mem_enum !inE /= -VnextE. case Hjo: (j == o). rewrite (eqP Hjo). by move/andP/proj1/andP/proj1 : Hun => /=; rewrite -VnextE -FnextE. case Hji: (i \in 'V j) => /=. by rewrite -enumT mem_enum FnextE Hji. by rewrite FnextE Hji. rewrite get_esti_flatten. apply/nilP. rewrite /nilp size_flatten sumnE big_seq/= big1// => e. rewrite /shape -!map_comp => /mapP[x Hx] -> /=. apply get_esti_nil. have Hunx : uniq_path (tanner_rel H) (inl x) [:: id_of_kind kv i & s]. rewrite mem_filter in Hx. move/andP/proj1/andP: Hx => [Hx Hx']. rewrite /=. move: Hun. rewrite tanner_relE. exact: cons_uniq_path. rewrite -tree_ok // labels_sumprod_down labels_sumprod_up. apply/negP => Hi. have Hl := uniq_labels_build_tree_rec tanner_acyclic rW h.+1 Hun. rewrite /= in Hl. move/andP/proj1: Hl. apply/negP. rewrite negbK. apply/flattenP. exists (labels (build_tree_rec H rW h [:: inr i & s] kf x)). by apply/map_f/map_f. by move/eqP: Hid Hi => [] ->. rewrite /= in_cons in Hn0 Hid. rewrite eq_sym Hid /= -!map_comp in Hn0. move/flattenP: Hn0 => [l Hl Hn0l]. move/mapP: Hl => [j Hj] /= Hjl. subst l. have Hti: node_id t = id_of_kind k i by []. have Hget: get_esti n0 (estimation t) = get_esti n0 (flatten (map (@estimation _ _) (children t))). destruct t; simpl. destruct node_tag; rewrite //=. rewrite /= in Hti. by rewrite Hti Hid. rewrite Hget get_esti_flatten -map_comp. rewrite select_children_spec in Hj. have Hunj : uniq_path (tanner_rel H) (id_of_kind (negk k) j) (id_of_kind k i :: s). move/andP: Hj => [Hij Hun']. apply: cons_uniq_path => //. by rewrite sym_tanner_rel. rewrite -(IH [:: id_of_kind k i & s] (negk k) j Hh') //. rewrite /= -map_comp. rewrite (flatten_single (x:=j)) => //. by rewrite uniq_select_children. by rewrite select_children_spec. move=> y Hy Hyj /=. apply/nilP/eqP. apply get_esti_nil. have Huny: uniq_path (tanner_rel H) (id_of_kind (negk k) y) (id_of_kind k i :: s). rewrite select_children_spec in Hy. move/andP: Hy => [Hiy Hun']. apply: cons_uniq_path => //. by rewrite sym_tanner_rel. rewrite -tree_ok // labels_sumprod_down labels_sumprod_up. have Hun':= uniq_labels_build_tree_rec tanner_acyclic rW h.+1 Hun. move: Hun' => /= /andP/proj2. rewrite -map_comp => Hun'. case Hn0: (inr n0 \in _); last by []. rewrite -select_children_spec in Hj. rewrite (uniq_flatten_map (x:=y) (y:=j) _ Hun') ?eqxx // in Hyj. apply/hasP. rewrite -tree_ok // labels_sumprod_down labels_sumprod_up in Hn0l. by exists (inr n0). 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