fact: Fixpoint try_just_one (bs : seq bool) (p : pos) (z : nat) (g : grid) (st : state) (f : seq nat -> state -> jRes) : jRes := if bs is b :: bs1 then if b then let g1 := update p z g in let st1 := update_anti_literals p z st in match f g1 st1 with | jNone => try_just_one bs1 p z.+1 g st f | jOne s2 => match try_just_one bs1 p z.+1 g st f with | jNone => jOne s2 | jOne s3 => if s2 == s3 then jOne s2 else jMore s2 s3 | jMore s1 s2 => jMore s1 s2 end | jMore s1 s2 => jMore s1 s2 end else try_just_one bs1 p z.+1 g st f else jNone.
imports: mathcomp(all_ssreflect) mathcomp(zify)