Require Import List.

Notation string X := (list X).

Notation str := (string bool).

Module RuleNotation.
Notation "x / y" := (x, y).
End RuleNotation.
Import RuleNotation.

Notation SRS X := (list (string X * string X)).

Inductive rew {X : Type} (R : SRS X) : string X -> string X -> Prop :=
  rewB x y u v : In (u / v) R -> rew R (x ++ u ++ y) (x ++ v ++ y).
Inductive rewt {X : Type} (R : SRS X) : string X -> string X -> Prop :=
  rewR z : rewt R z z
| rewS x y z : rewt R x y -> rew R y z -> rewt R x z.

Definition SR R : str * str -> Prop :=
  fun '(x, y) => rewt R x y.

Definition swap {X Y} : X * Y -> Y * X := fun '(x,y) => (y,x).

Definition TSR : SRS nat * string nat * string nat -> Prop :=
    fun '(R, x, y) => rewt (R ++ map swap R) x y.