proposition: Lemma tree_of_trace_graph (l : nat) k c seqs p : p \in border (nodes c) -> seqs \in dest_ports_seqs def_port c l.*2 -> let c' := switch_step_it c seqs in tree_like c' -> partial_connected c -> tree_of_trace k p seqs = tree_of_graph l.*2 k c' p.
proof: Proof. elim: l k c seqs p => // l IHl k c /= seqs p Hp. rewrite dest_ports_seqs_step. move/bigcupP => /= [t Ht]. move/imsetP => /= [ts Hts ->]. set c' := switch_step_it _ _. move=> Htl Hpc. rewrite theadE /=. move: (Hp). rewrite -mem_enum -index_mem -cardE => Hidx. move: (memt_nth (def_port,set0) t Hidx). set epn := nth _ _ _. case_eq epn => ep en def Hin. rewrite {}/epn in def. have [Hpc' Hepc'] : p \in edom c' /\ edges c' p = ep. rewrite /c' /=. rewrite tuple_to_partial_enumK. have [Hctd Hct] := add_edge_step_it Hidx Ht def. split. by apply/subsetP: Hctd; apply monotonic_switch_step_it_odd. by rewrite (proj2 (monotonic_switch_step_it_odd _ _)). rewrite Hepc'. destruct (conodes_step_it Ht) as [Hct Hbt]. + rewrite -tree_like_switch. move: Htl; rewrite /c' /= tuple_to_partial_enumK. apply tree_like_rev_switch_step_it. + by []. rewrite (@node_of_hemi_comp_graph ep en) //. rewrite ffunE def. rewrite /image_mem. congr Node. apply eq_in_map => s Hs. have Hsb : s \in border (conodes (step_it c t)). rewrite Hbt inE big_tuple. apply/orP/or_intror/bigcupP. move/tnthP: (Hin) => [i Hi]. exists i => //. by rewrite -Hi /= -mem_enum. move: Hts. rewrite dest_ports_seqs_step => /bigcupP [t' Ht']. move/imsetP => /= [ts' Hts' eqts]. subst ts. rewrite !tbeheadE theadE. move: (Hsb). rewrite -mem_enum -index_mem -cardE => Hidx'. move: (memt_nth (def_port,set0) t' Hidx'). set epn' := nth _ _ _. case_eq epn' => ep' en' def' Hin'. rewrite {}/epn' in def'. destruct (conodes_step_it Ht') as [Hct' Hbt']. + rewrite -tree_like_switch. move: Htl; rewrite /c' /= !tuple_to_partial_enumK. apply tree_like_rev_switch_step_it. + by apply connected_switch, connected_step_it. destruct (@add_edge_step_it (switch (step_it c t)) s t' ep' en') as [Hsd Hse] => //. rewrite -switchK_edges // in Hse. have Hs' : ep' = switch_edges c' s. rewrite -Hse /c' /= !tuple_to_partial_enumK. rewrite -(proj2 (@monotonic_switch_progress (fun c => switch_step_it c ts') _ _ _)) //. apply (proj1 (monotonic_switch_step_it _ _)). apply (proj2 (monotonic_switch_step_it _ _)). rewrite ffunE def' Hs' /c'. rewrite (@node_of_hemi_comp_graph _ en'). congr Node. apply eq_in_map => q. rewrite mem_enum -Hs' => Hq. rewrite negk_involution switchK. rewrite (IHl k (switch (step_it (switch (step_it c t)) t'))). + by rewrite /= !tuple_to_partial_enumK. + rewrite Hbt' inE big_tuple. apply/orP/or_intror/bigcupP. exists (Ordinal Hidx') => //. move: Hq. by rewrite (tnth_nth (def_port,set0)) def'. + by []. + by rewrite /c' /= !tuple_to_partial_enumK in Htl. + by apply connected_switch, connected_step_it, connected_switch, connected_step_it. rewrite -Hs'. move: Ht'; rewrite inE => /and3P[] /allP /(_ _ Hin') /=. by rewrite inE => /andP []. rewrite /= !tuple_to_partial_enumK. apply (subsetP (monotone_nodes_switch_step_it _ _)). rewrite /= -Hct'. rewrite inE; apply/orP/or_introl. rewrite inE. apply (map_f snd Hin'). move: Ht; rewrite inE => /and3P[] /allP /(_ _ Hin) /=. by rewrite inE => /andP []. destruct ts as [ts Hsz]. destruct ts as [|t' ts'] => //. move/eqP: (Hsz) => [] /eqP Hsz'. rewrite /c' /=. eapply (subsetP (monotone_conodes_switch_step_it _ (Tuple Hsz'))). rewrite /= part_nodes_step_it /= tuple_to_partial_enumK -Hct inE. apply/orP/or_introl. rewrite inE. apply (map_f snd Hin). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner