proposition: Lemma tree'_of_trace_graph l pn (seqs : l.*2.+1.-tuple _) : seqs \in dest_ports_seqs def_port (start_graph pn) l.*2.+1 -> let c' := switch_step_it (start_graph pn) seqs in tree_like c' -> tree'_of_trace pn seqs = tree'_of_graph l c' pn.
proof: Proof. rewrite dest_ports_seqs_step => /bigcupP /= [t Ht]. move=> /imsetP /= [ts Hts ->]. move=> Htl. have Hpc := @connected_start pn. rewrite /tree'_of_trace /tree'_of_graph. congr Node. apply eq_in_map => p. rewrite mem_enum => /= Hp. rewrite /= !tbeheadE !theadE !tuple_to_partial_enumK in Htl *. set c' := switch_step_it _ _. move: (Hp). rewrite -mem_enum -index_mem -cardE => Hidx. move: (memt_nth (def_port,set0) t Hidx). rewrite ffunE. move Heqn : (nth _ _ _) => eqn Hin. case: eqn Heqn Hin => ep en Heqn Hin. destruct (@conodes_step_it (start_graph pn) t Ht) as [Hct Hbt]. + rewrite -tree_like_switch. by apply (tree_like_rev_switch_step_it Htl). + by apply connected_start. destruct (@add_edge_step_it (start_graph pn) p t ep en) as [Hpd Hpe] => //. rewrite -switchK_edges // in Hpe. have Hp' : ep = switch_edges c' p. rewrite -Hpe /c'. rewrite (proj2 (@monotonic_switch_progress (switch_step_it ^~ ts) _ _ _)) //. + by apply (proj1 (monotonic_switch_step_it _ _)). + by apply (proj2 (monotonic_switch_step_it _ _)). rewrite -Hp'. rewrite (@node_of_hemi_comp_graph _ en). + congr Node. apply eq_in_map => q. rewrite mem_enum switchK => /= Hq. apply tree_of_trace_graph => //. - rewrite /= Hbt inE big_tuple. apply/orP/or_intror/bigcupP => /=. exists (Ordinal Hidx) => //. by rewrite (tnth_nth (def_port,set0)) Heqn. - by apply connected_switch, connected_step_it. + move: Ht; rewrite inE => /and3P[] /allP /= /(_ _ Hin). by rewrite /= !inE /= => /andP []. + rewrite /c'. apply (subsetP (monotone_nodes_switch_step_it _ _)). rewrite /= -Hct. rewrite inE; apply/orP/or_introl. rewrite inE. by apply/mapP; exists (ep,en). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner