proposition: Lemma nfa_ofP x : reflect (exists T, @reject_cert x T) (x \in nfa_lang nfa_of).
proof: Proof. apply: (iffP nfaP). - move => [s] [r] [Hp Hr]. pose T (i : pos x) := if i:nat is i'.+1 then (nth s (s::r) i').2 else (nth s (s::r) 0).1. have T_comp (j : 'I_(size x)) : comp (tnth (tape x) j) (T (inord j)) (T (inord j.+1)) (T (inord j.+2)). case: j => /= m Hm. move: (run_trans Hm Hr) => /andP [_]. have -> : (nth s (s :: r) m).1 = T (inord m). case: m Hm => [|m] Hm; first by rewrite -inord0. rewrite /T inordK ?ltnS // 2?ltnW //. move/ltnW : Hm => Hm. by case/andP : (run_trans Hm Hr) => /eqP-> ?. have -> : (nth s (s :: r) m).2 = T (inord m.+1) by rewrite /T inordK // ltnS ltnW. have -> // : (nth s r m).2 = T (inord m.+2). by rewrite /T inordK // ltnS. exists T. split => //. + rewrite /T /=. move: Hp. rewrite inE. by case/andP. + rewrite /T /= (run_size Hr) -last_nth. move/run_last : (Hr). rewrite inE. by case/andP. + move => i p j q H. rewrite /step /read. case: (ord2P _) => [/eqP ?|/eqP ?|i' Hi']; subst => //=. * rewrite [_ == 0]eqn_leq ltn0 !bsimp => /andP [q1 q2]. rewrite /T (eqP q2) /= in H *. move: Hp. rewrite !inE => /andP [_ /forall_inP /(_ _ H) /forall_inP]. apply. by rewrite !inE eqxx andbT /= in q1. * rewrite [_ == _.+2](ltn_eqF) // !bsimp eqSS => /andP [q1 q2]. rewrite /T /= (run_size Hr) -[size r]/((size (s :: r)).-1) nth_last in H. move: (run_last Hr). rewrite inE. rewrite !inE eqxx andbT /= in q1. move => /andP [_ /forall_inP /(_ p H) /forall_inP /(_ q q1)]. rewrite /T (eqP q2) (run_size Hr). case e : (size r) => [|m] ; first by rewrite (size0nil e). have Hm : m < size x by rewrite -e (run_size Hr). rewrite -nth_last e /=. by case/andP: (run_trans Hm Hr) => /eqP ->. - move: (T_comp i') => /= /forall_inP /(_ p). rewrite Hi' inord_val => /(_ H) /forallP /(_ q). case/andP => q1 q2. case/orP; case/andP => Ht e; rewrite ?Ht /= in q1 q2. -- move: q2. by rewrite /T (eqP e) inordK // -Hi' ?ltnS. -- move: q1. rewrite -Hi' eqSS in e. by rewrite -(eqP e) -{2}[j]inord_val. - move => [T] [T1 T2 T3]. set s := (T ord0, T ord1). exists s. set r := [tuple (T (inord i.+1), T (inord i.+2)) | i < (size x)]. exists r. have E m : m <= size x -> nth s (s :: r) m = (T (inord m), T (inord m.+1)). case: m => m; first by rewrite nth0 /= -inord0 -inord1. move => H. by rewrite [r]lock /= -lock -[m]/(val (Ordinal H)) -tnth_nth tnth_mktuple. split. + rewrite inE /= T1 /=. apply/forall_inP => p /T3 H. apply/forall_inP => q Hq. apply: H. by rewrite /step /read ord2P0 !inE Hq eqxx. + apply: runI. * by rewrite size_map size_enum_ord. * rewrite -nth_last [nth _ _ _](_ : _ = nth s (s::r) (size r)); last by case: (tval r). rewrite size_tuple E // -inord_max inE /= T2 /=. apply/forall_inP => p /T3 H. apply/forall_inP => q Hq. apply H. by rewrite /step /read ord2PM !inE Hq inordK // eqxx !bsimp. * move => i. rewrite unfold_in. rewrite !E //= 1?ltnW // eqxx /=. apply/forall_inP => p /T3 H. apply/forallP => q. have Hi : i.+1 = (inord i.+1 : pos x). by rewrite inordK // !ltnS 1?ltnW //. apply/andP ; split; apply/implyP => Ht; apply H; rewrite /step /read /= (ord2PC Hi) Ht. - by rewrite !inordK ?eqxx ?bsimp // !(ltn_ord,ltnS,ltnW). - by rewrite !inordK ?eqxx ?bsimp // !(ltn_ord,ltnS,ltnW). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages nfa two_way)