proposition: Lemma nfa_for_ltnP {X Y n} {v : seq (vec n)} : reflect (exists v1 v2, [/\ v = v1 ++ v2, {in v1,zero_at n Y} & {in v2,zero_at n X}]) (v \in nfa_lang (nfa_for_ltn n X Y)).
proof: Proof. move: v => v0. apply: (iffP (nfa_ofP _ _)). - rewrite /enfa_lang => [[[|_]]]; first by rewrite inE. suff S q v: enfa_accept (N := enfa_for_ltn n X Y) q v -> if q then {in v, zero_at n X} else (exists v1 v2, [/\ v = v1 ++ v2, {in v1,zero_at n Y} & {in v2,zero_at n X}]). { by move/S. } elim => // {v0 v} [||]. + case => // _. by do 2 exists nil. + move => [|] a [|] //= v. * move => A _ B u. case/predU1P => [->|]; by [rewrite (negbTE A)| apply: B]. * move => A _ [v1] [v2] [C D E]. exists (a :: v1); exists v2; split => //; first by rewrite C. apply/forall_cons. split => //. by rewrite (negbTE A). + move => [|] [|] // v. by exists nil; exists v. - move => [v1] [v2] [->] A B. exists false; first by rewrite inE. elim: v1 A => /= [_|a v1 IH A]. + (apply: EnfaNone; first instantiate (1 := true)) => //. elim: v2 B {v0} => [_|a s IH B]. * constructor. by rewrite inE. * (apply: EnfaSome; first instantiate (1 := true)) => //=. -- by rewrite B ?inE ?eqxx. -- apply: IH => u C. apply B. by rewrite inE C orbT. + apply: EnfaSome; first instantiate (1 := false). * by rewrite /= A ?inE ?eqxx. * apply IH => u C. apply A. by rewrite inE C orbT. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)