fact: Definition reject_cert x (T : pos x -> {set M}) := [/\ nfa2_s M \in T ord1, [disjoint (nfa2_f M) & (T ord_max)] & forall i p j q, p \in T i -> step M x (p,i) (q,j) -> q \in T j ].
imports: mathcomp(all_ssreflect) RegLang(misc languages nfa two_way)