proposition: Lemma normal_steps s: forall H : tgraph2 , steps (tgraph_of_nterm s) H -> tgraph_of_nterm s ≃2p H.
proof: Proof. suff E: forall G H, steps G H -> G ≃2p tgraph_of_nterm s -> G ≃2p H. by intros; apply E=>//; reflexivity. destruct 1 as [G H I|G' G H H' I S _]=>//L. - exfalso. setoid_rewrite (inhabits I: _ ≃2p _) in L. clear -S L. destruct L as [[L Li Lo]]. generalize (card_bij (iso_e L)). destruct s; destruct S; simpl in *; (try by rewrite !card_option ?card_sum ?card_unit ?card_void); rewrite /unl in Li, Lo; move=>_. * generalize (card_bij (iso_v L)). rewrite card_sum !card_unit addnC. have H: 0 < #|G|. apply /card_gt0P. by exists input. revert H. case #|G|; discriminate. * revert Li Lo. suff E: input=output :>G by congruence. apply/(card_le1_eqP (A := predT)) => //. apply iso_v, card_bij in L. rewrite !card_sum !card_unit addnC in L. by injection L=>->. * have E: forall y, L (inr tt) <> L (inl y) by intros y H; generalize (bij_injective (f:=L) H). case_eq (L (inr tt)); case. generalize (E input). simpl in *. congruence. generalize (E output). simpl in *. congruence. * generalize (endpoint_iso L false None). generalize (endpoint_iso L true None). have H: L.e None = None by case (L.e None)=>//; repeat case. rewrite H. case L.d; simpl; congruence. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) GraphTheory(setoid_bigop structures mgraph pttdom mgraph2) GraphTheory(rewriting reduction open_confluence transfer)