proposition: Proposition reduce (u: term): steps (tgraph_of_term u) (tgraph_of_nterm (nt u)).
proof: Proof. induction u=>//=. - etransitivity. apply dot_steps; [apply IHu1|apply IHu2]. case (nt u1)=>[a|a u b]; case (nt u2)=>[c|c v d]=>/=. * apply iso_step. etransitivity. apply dot2unit_r. apply add_vlabel2_unit. * apply iso_step. etransitivity. apply dot2unit_l. etransitivity. apply add_vlabel2_edge. apply edge_graph2_iso=>//=. by apply: monC. * apply iso_step. etransitivity. apply dot2unit_r. apply add_vlabel2_edge. * etransitivity. apply isop_step. 2: etransitivity. 2: apply one_step, (step_v2 (G:=two_graph2 a d) (inl tt) (inr tt) u [elem_of b·elem_of c] v). exists. apply: dot_edges. apply isop_step. exists. apply: (add_edge2_iso' iso2_id). by rewrite !dotA. - etransitivity. apply par_steps; [apply IHu1|apply IHu2]. case (nt u1)=>[a|a u b]; case (nt u2)=>[c|c v d]=>/=. * apply isop_step. exists. apply par2unitunit. * etransitivity. apply isop_step. 2: etransitivity. 2: apply one_step, (step_e0 (G:=unit_graph2 (c⊗(d⊗a))%CM) tt v). rewrite parC. exists. apply: par2edgeunit. apply isop_step. exists. etransitivity. apply add_vlabel2_unit. apply unit_graph2_iso. exact: reduce_shuffle. * etransitivity. apply isop_step. 2: etransitivity. 2: apply one_step, (step_e0 (G:=unit_graph2 (a⊗(b⊗c))%CM) tt u). exists. apply: par2edgeunit. apply isop_step. exists. etransitivity. apply add_vlabel2_unit. apply unit_graph2_iso. exact: reduce_shuffle. * etransitivity. apply isop_step. 2: etransitivity. 2: apply one_step, (step_e2 (G:=two_graph2 (a⊗c)%CM (b⊗d)%CM) (inl tt) (inr tt) u v). 2: reflexivity. exists. apply: par_edges. - etransitivity. apply cnv_steps, IHu. case (nt u)=>[a|a v b]=>//=. apply isop_step. exists. etransitivity. refine (iso_iso2 (add_edge_rev _ _ _) _ _). rewrite eqvEcnv. symmetry. apply cnvI. simpl. symmetry. etransitivity. apply: (add_edge2_iso (iso_iso2 (union_C _ _) _ _)). reflexivity. - etransitivity. apply dom_steps, IHu. case (nt u)=>[a|a v b]=>//=. etransitivity. apply one_step, (@step_v1 _ (unit_graph2 a) tt v b). apply isop_step. exists. etransitivity. apply add_vlabel2_unit. apply unit_graph2_iso. done. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)