proposition: Lemma runR x y z p q (i j: nat) k : Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 -> connect (srel ((size x).+1 + k) (x++z)) (p,inord (size x + i)) (q,inord (size x + j)) -> connect (srel ((size y).+1 + k) (y++z)) (p,inord (size y + i)) (q,inord (size y + j)).
proof: Proof. move => Tab_eq Hi /andP [Hj0 Hj]. case/connectP => cs. move: cs i Hi p. apply: (size_induction (measure := size)) => /= cs IH i Hi p. case: (boolP (i == 0)) => Hi0. - rewrite (eqP Hi0) !addn0 => p1 p2. case: (srel_mid_path (k := (size x).+1) _ p1 p2); try solve [rewrite inordI; ssrlia]. apply/andP; split; rewrite !inordK; ssrlia. move => p' [cl] [cr] [Ecs Lcl Pcl]. apply/(@srel_mid (size y).+1) ; try solve [rewrite !inordK; ssrlia|rewrite -addn1; ssrlia]. + exists p'. apply/Tab2P. rewrite -Tab_eq. apply/Tab2P. by apply/connectP; exists cl. + subst cs. rewrite -[_.+1 as X in inord X]addn1. apply: (IH cr) => {IH} //; ssrlia. * destruct cl as [|c cs]; simpl in *. case: Lcl => _. -- move/(f_equal (@nat_of_ord _)); rewrite ?inordK; intros; ssrlia. -- by rewrite[size (cs ++ cr)]size_cat -addnS leq_addl. * rewrite cat_path -Lcl addn1 in p1 *. by case/andP : p1. * by rewrite p2 last_cat -Lcl addn1. - destruct cs as [|c cs]; simpl in *. + move => _ [-> /(f_equal (@nat_of_ord _))/eqP]. rewrite !inordK ?eqn_add2l ?size_cat -?addnS ?leq_add2l // => /eqP ->. exact: connect0. + case/andP => P1 P2 L. case/srelRE: (P1) => // p' [ip] [Hip ?]; subst. rewrite srelR // -(@srelR y z) // in P1. apply: connect_trans (connect1 P1) _. exact: (IH cs). Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)