proposition: Lemma runL (i j : pos x) p q : connect (srel (size x).+1 x) (p,i) (q,j) = connect (srel (size x).+1 (x++z)) (p,inord i) (q,inord j).
proof: Proof. pose f (c : nfa2_config M x) : nfa2_config M (x ++ z) := (c.1, inord c.2). rewrite -[(p,inord i)]/(f (p,i)) -[(q,inord j)]/(f (q,j)). apply: connect_transfer => //. - move => {p q i j} [p i] [q j] /= [->] /inord_inj. case/(_ _)/Wrap => [|->//]. ssrlia. - move => [? ?] [? ?]. rewrite /f /=. exact: srelL. - move => {p q i j} [p i] [q j] step. exists (q,inord j). rewrite /f /= inordK ?inord_val //. move: (srel1 step) => /= Hs. case/andP : step => /= _ Hi. rewrite (leqRW Hs) ltn_neqAle eq_sym Hi /=. by rewrite inordK ltnS ?leq_ord // (leqRW (leq_ord i)) ltnS size_cat leq_addr. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)