proposition: Lemma starFnext_iter_mxSumProdS (Hc : syndrome H c = 0) l : starFnext H y (iSP_BEC0 H y l) = erasures (Esti H y (iSP_BEC0 H y l)).
proof: Proof. apply/setP => /= n0. case/boolP : (n0 \in erasures (Esti H y (iSP_BEC0 H y l))) => H0. rewrite !inE mxE /Esti /colFnext in H0. rewrite inE. move: H0. rewrite /y mxE. case: ifPn => [n0E |n0E H0]. rewrite Prod_cons_Star => H0. rewrite eqxx andTb. apply/forallP => /= m0. apply/implyP => Hm0. set tmp := [seq _ | _ in _] in H0. case/boolP : (Bit c ``_ n0 \in tmp) => [abs | Hn0]. have {abs} : Bit (F2_of_bool (negb (bool_of_F2 (c ``_ n0)))) \in tmp. apply: contraLR abs => abs. rewrite notin_num_occ_0 -{1}(bool_of_F2K (c ``_ n0)). move: H0; rewrite Prod_StarE => /forallP/(_ (bool_of_F2 c ``_ n0))/eqP ->. by rewrite -notin_num_occ_0. case/mapP => m1 Hm1. rewrite mxE => m1n0. move: (all_starletter_iSP_BEC0 Hc E l n0) => /allP/(_ _ Hm1) /=. rewrite mxE -m1n0. by case: (F2P (c ``_ n0)). move: (all_starletter_iSP_BEC0 Hc E l n0) => /allP/(_ m0). rewrite mem_enum => /(_ Hm0); rewrite inE. rewrite /starletter => /orP[|]. by rewrite mxE. rewrite mxE => /eqP abs. exfalso. move/negP : Hn0; apply. apply/mapP; exists m0. by rewrite mem_enum. by rewrite mxE abs. exfalso. move: H0; rewrite Prod_StarE => /forallP/(_ (bool_of_F2 (c ``_ n0)))/eqP. rewrite num_occ_cons /= bool_of_F2K eqxx /= (_ : _ == _ = false) /=; last by case/F2P : (c ``_ n0). rewrite add1n add0n. rewrite (_ : N(Bit (F2_of_bool (~~ bool_of_F2 c ``_ n0)) | _) = O) //. apply/eqP; rewrite -notin_num_occ_0. apply/mapP; case => m1 Hm1 abs. move: (all_starletter_iSP_BEC0 Hc E l n0) => /allP/(_ _ Hm1). rewrite /= -abs. by case/F2P : (c ``_ n0). rewrite !inE mxE /Esti in H0. rewrite inE. apply/negbTE. rewrite negb_and negb_forall. case/boolP : (y ``_ n0 != Star) => //=. rewrite negbK. move: H0. rewrite /y mxE. case: ifP => // n0E. rewrite /colFnext Prod_cons_Star. case/Prod_map_not_Star => [b [m1 [H0 H1]]] _. apply/existsP; exists m1. rewrite mxE in H1. by rewrite negb_imply H0 /= H1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) f2 ssr_ext ssralg_ext max_subset num_occ hamming ldpc_erasure tanner linearcode