proposition: Lemma fixed_point_stopset_starFnext l : iSP_BEC0 H y l.+1 = iSP_BEC0 H y l -> stopset H (starFnext H y (iSP_BEC0 H y l.+1)).
proof: Proof. move=> Hstable. rewrite stopsetE; apply/'forall_forallP => m0 n0; apply/implyP => /andP[Hn0 Hm0]. move: Hn0. rewrite /starFnext inE => /andP[yn0 /forallP Hn0]. move: (Hn0 m0) => /implyP /(_ Hm0)/eqP. case/iSP_BEC0_star_inv => n1 [] n1n0 [] m0n1 bm0n1. apply/set0Pn; exists n1. rewrite FnextE in m0n1. rewrite in_setD1 in_setI n1n0 /= m0n1 /= /starFnext /=. have [H1 H2] : (forall m1, m1 \in `F n1 :\ m0 -> iSP_BEC0 H y l m1 n1 = Star) /\ y ``_ n1 = Star. apply Prod_erase_Star. - move=> ?; by apply all_starletter_iSP_BEC0D1. - rewrite /colFnextD1 (@PiSP_BEC0_Star_inv l _ _ m0n1) // Prod_cons_Star. apply/eqP. rewrite Prod_starblank_is_Star //. apply/allP => /= x. case/mapP => /= m1 Hm1 ->. rewrite mxE -Hstable (@PiSP_BEC0S_Star_inv _ _ m0) // /PiSP_BEC0 ?Hstable //; by rewrite mem_enum in Hm1. rewrite inE H2 eqxx /=. apply/forallP => m2. apply/implyP => Hm2. case/boolP : (m2 == m0) => [/eqP ?|m2m0]. subst m2. suff : (iSP_BEC0 H y l) m0 n1 = Star. by rewrite -{1}Hstable /= => ->. case: l => [|l] in Hstable Hn0 bm0n1 H1 *. - by rewrite !mxE Hm2. - apply: (@PiSP_BEC0_Star_inv_stable _ n0 m0 _ _ _ n1 m0n1 n1n0) => //. + by rewrite FnextE in Hm0. + rewrite FnextE in Hm0. rewrite /= /mxProd /colFnextD1 mxE FnextE Hm0 (eqP yn0) Prod_cons_Star. apply/Prod_starblank_is_Star/allP => y0. case/mapP => m1 Hm1 ->. apply/starblankP; apply/orP; left. suff <- : (iSP_BEC0 H y l.+2) m1 n0 = Star by rewrite mxE Hstable. apply/eqP. move: Hm1 (Hn0 m1). by rewrite mem_enum 2!inE => /andP[m1m0 ->]. move: (H1 m2). rewrite 2!inE m2m0 Hm2 => /(_ erefl) <-. by rewrite -{2}Hstable. 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