diff --git a/bin/gen/ExtractRomanWheel.v b/bin/gen/ExtractRomanWheel.v
index d31543a..bb51984 100644
--- a/bin/gen/ExtractRomanWheel.v
+++ b/bin/gen/ExtractRomanWheel.v
@@ -13,6 +13,7 @@ Require Import TBGen.Util.OMap.
 Require Import TBGen.Bear.Sort.
 Require Import TBGen.Bear.BearGame.
 Require Import TBGen.Bear.RomanWheel.
+Require Import TBGen.Bear.RomanWheelSym.
 Require Import TBGen.TB.TB.
 
 Set Warnings "-extraction-default-directory".
diff --git a/bin/gen/dune b/bin/gen/dune
index 526359f..680069b 100644
--- a/bin/gen/dune
+++ b/bin/gen/dune
@@ -29,4 +29,4 @@
 (rule
   (targets tb_w.json tb_b.json)
   (deps gen_file.exe)
-  (action (run ./gen_file.exe)))
+  (action (run time ./gen_file.exe)))
diff --git a/bin/query/ExtractQuery.v b/bin/query/ExtractQuery.v
index bf0d038..8b82bcf 100644
--- a/bin/query/ExtractQuery.v
+++ b/bin/query/ExtractQuery.v
@@ -17,8 +17,9 @@ Require Import TBGen.Bear.Sort.
 Require Import TBGen.Bear.BearGame.
 Require Import TBGen.Bear.RomanWheelExtras.
 Require Import TBGen.Bear.RomanWheel.
-Require Import TBGen.TB.TB.
-Require Import TBGen.TB.OCamlTB.
+Require Import TBGen.Bear.RomanWheelSym.
+Require Import TBGen.SymTB.TB.
+Require Import TBGen.SymTB.OCamlTB.
 
 Definition make_BG_State {G} (pl : Player.Player)
   (b h1 h2 h3 : Graph.Vert G) : option (BG_State G).
diff --git a/bin/query/dune b/bin/query/dune
index 960b9ee..9907cc0 100644
--- a/bin/query/dune
+++ b/bin/query/dune
@@ -3,20 +3,25 @@
   (extracted_modules
     Ascii
     BearGame
+    Bisim
     Compare_dec
     Datatypes
     Dec
     ExtractQuery
     Game
     Graph
+    GroupAction
     IntHash
     IntMap
     List0
+    Nat
     OCamlTB
     OMap
+    PeanoNat
     Player
     PrimInt63
     RomanWheel
+    RomanWheelSym
     Show
     Sort
     Specif
@@ -36,20 +41,25 @@
     ;; Extracted code
     Ascii
     BearGame
+    Bisim
     Compare_dec
     Datatypes
     Dec
     ExtractQuery
     Game
     Graph
+    GroupAction
     IntHash
     IntMap
     List0
+    Nat
     OCamlTB
     OMap
+    PeanoNat
     Player
     PrimInt63
     RomanWheel
+    RomanWheelSym
     Show
     Sort
     Specif
diff --git a/theory/Bear/BearGame.v b/theory/Bear/BearGame.v
index 7c545a1..6cd2123 100644
--- a/theory/Bear/BearGame.v
+++ b/theory/Bear/BearGame.v
@@ -9,14 +9,16 @@ Require Import Games.Game.Game.
 Require Import Games.Game.Game.
 Require Import TBGen.Bear.Graph.
 Require Import TBGen.Bear.Sort.
-Require Import TBGen.TB.TB.
+Require Import TBGen.SymTB.TB.
 Require Import Games.Game.Player.
 Require Import TBGen.Util.IntHash.
 Require Import Games.Util.Dec.
 Require Import TBGen.Util.AssocList.
 Require Import TBGen.Util.IntMap.
 Require Import TBGen.Util.OMap.
-Require Import TBGen.TB.OCamlTB.
+Require Import TBGen.SymTB.OCamlTB.
+Require Import TBGen.Bear.GroupAction.
+Require Import TBGen.Util.Bisim.
 
 Definition NoDup_dec {X} `{Discrete X} (xs : list X) :
   { NoDup xs } + { ~ NoDup xs }.
@@ -1074,5 +1076,442 @@ Proof.
       congruence.
 Defined.
 
-Definition Bear_TB (G : Graph) `{hsh : IntHash (GameState (BearGame G))}
+Definition BG_State_act {G} {H} `{GroupAction G H}
+  (x : carrier H) (s : BG_State G) : BG_State G.
+Proof.
+  refine {|
+    to_play := to_play s;
+    bear := x # (bear s);
+    hunters := insertion_sort (map (act x) (hunters s));
+    hunters_sort := _;
+    hunters_3 := _;
+    hunters_distinct := _;
+    bear_not_hunter := _;
+  |}.
+  - apply insertion_sort_sorts.
+  - rewrite insertion_sort_length.
+    rewrite map_length.
+    apply s.
+  - apply insertion_sort_NoDup.
+    apply FinFun.Injective_map_NoDup.
+    + cbv; apply act_inj.
+    + apply s.
+  - intro pf.
+    apply insertion_sort_In_1 in pf.
+    rewrite in_map_iff in pf.
+    destruct pf as [v [Hv1 Hv2]].
+    apply act_inj in Hv1; subst.
+    exact (bear_not_hunter s Hv2).
+Defined.
+
+Lemma sorted_list_eq {X} `{Ord X} (xs : list X) : forall xs',
+  sorted xs -> sorted xs' ->
+  (forall x, In x xs <-> In x xs') ->
+  NoDup xs ->
+  NoDup xs' ->
+  xs = xs'.
+Proof.
+  induction xs; intros.
+  - destruct xs'; auto.
+    assert (In x (x :: xs')) as pf by now left.
+    rewrite <- H2 in pf.
+    destruct pf.
+  - destruct xs'.
+    + assert (In a (a :: xs)) as pf by now left.
+      rewrite H2 in pf.
+      destruct pf.
+    + assert (a = x).
+      { assert (In a (a :: xs)) by now left.
+        rewrite H2 in H5.
+        destruct H5; [congruence|].
+        assert (In x (x :: xs')) by now left.
+        rewrite <- H2 in H6.
+        destruct H6; [congruence|].
+        apply ord_le_antisym.
+        * inversion H0.
+          rewrite Forall_forall in H10.
+          now apply H10.
+        * inversion H1.
+          rewrite Forall_forall in H10.
+          now apply H10.
+      }
+      subst; f_equal.
+      * apply IHxs.
+        -- now inversion H0.
+        -- now inversion H1.
+        -- intro y; split; intro pf.
+           ++ assert (In y (x :: xs)) by now right.
+              rewrite H2 in H5.
+              destruct H5; auto.
+              subst.
+              inversion H3; contradiction.
+           ++ assert (In y (x :: xs')) by now right.
+              rewrite <- H2 in H5.
+              destruct H5; auto.
+              subst.
+              inversion H4; contradiction.
+        -- now inversion H3.
+        -- now inversion H4.
+Qed.
+
+Lemma BG_State_act_comp {G} {H} `{GroupAction G H}
+  (x y : carrier H) (s : BG_State G) :
+  BG_State_act (x ** y) s =
+  BG_State_act x (BG_State_act y s).
+Proof.
+  apply BG_State_ext.
+  - reflexivity.
+  - simpl.
+    apply act_comp.
+  - simpl.
+    apply sorted_list_eq.
+    + apply insertion_sort_sorts.
+    + apply insertion_sort_sorts.
+    + intro v; split; intro pf.
+      * rewrite insertion_sort_In in *.
+        rewrite in_map_iff in *.
+        destruct pf as [v' [Hv'1 Hv'2]].
+        exists (y # v'); split.
+        -- now rewrite <- act_comp.
+        -- rewrite insertion_sort_In.
+           now apply in_map.
+      * rewrite insertion_sort_In in *.
+        rewrite in_map_iff in *.
+        destruct pf as [v' [Hv'1 Hv'2]].
+        rewrite insertion_sort_In in Hv'2.
+        rewrite in_map_iff in Hv'2.
+        destruct Hv'2 as [v'' [Hv''1 Hv''2]].
+        exists v''; split; auto.
+        rewrite act_comp; congruence.
+    + apply insertion_sort_NoDup.
+      apply FinFun.Injective_map_NoDup.
+      * cbv; apply act_inj.
+      * apply s.
+    + apply insertion_sort_NoDup.
+      apply FinFun.Injective_map_NoDup.
+      * cbv; apply act_inj.
+      * apply insertion_sort_NoDup.
+        apply FinFun.Injective_map_NoDup.
+        -- cbv; apply act_inj.
+        -- apply s.
+Qed.
+
+Lemma map_id {X} (f : X -> X) : (forall x, f x = x) -> forall l,
+  map f l = l.
+Proof.
+  intros Hf l.
+  induction l.
+  - reflexivity.
+  - simpl.
+    rewrite Hf.
+    rewrite IHl; auto.
+Qed.
+
+Lemma BG_State_act_id {G} {H} `{GroupAction G H}
+  (s : BG_State G) :
+  BG_State_act id s = s.
+Proof.
+  apply BG_State_ext.
+  - reflexivity.
+  - apply act_id.
+  - simpl.
+    rewrite map_id.
+    + apply sorted_list_eq.
+      * apply insertion_sort_sorts.
+      * apply s.
+      * apply insertion_sort_In.
+      * apply insertion_sort_NoDup; apply s.
+      * apply s.
+    + intro; apply act_id.
+Qed.
+
+Definition BearMv_act {G} {H} `{GroupAction G H}
+  (x : carrier H) (s : BG_State G) (m : BearMv s) :
+  BearMv (BG_State_act x s).
+Proof.
+  unshelve econstructor.
+  - exact (x # (b_dest m)).
+  - apply act_edge.
+    apply m.
+  - simpl; intro pf.
+    apply (b_dest_empty m).
+    rewrite insertion_sort_In in pf.
+    rewrite in_map_iff in pf.
+    destruct pf as [v [Hv1 Hv2]].
+    apply act_inj in Hv1; congruence.
+Defined.
+
+Definition HunterMv_act {G} {H} `{GroupAction G H}
+  (x : carrier H) (s : BG_State G) (m : HunterMv s) :
+  HunterMv (BG_State_act x s).
+Proof.
+  unshelve econstructor.
+  - exact (x # (h_orig m)).
+  - exact (x # (h_dest m)).
+  - simpl hunters.
+    rewrite insertion_sort_In.
+    rewrite in_map_iff.
+    exists (h_orig m); split; auto.
+    apply m.
+  - apply act_edge.
+    apply m.
+  - simpl; intro pf.
+    apply m.
+    apply act_inj with (x := x); auto.
+  - simpl; intro pf.
+    rewrite insertion_sort_In in pf.
+    rewrite in_map_iff in pf.
+    destruct pf as [v [Hv1 Hv2]].
+    apply act_inj in Hv1; subst.
+    f_equal.
+    apply m; auto.
+Defined.
+
+Definition BG_Move_act {G} {H} `{GroupAction G H}
+  (x : carrier H) (s : BG_State G) (m : BG_Move s) :
+  BG_Move (BG_State_act x s).
+Proof.
+  destruct m.
+  - apply BearMove.
+    + auto.
+    + apply BearMv_act; auto.
+  - apply HunterMove.
+    + auto.
+    + apply HunterMv_act; auto.
+Defined.
+
+Lemma BG_Move_act_exec {G} {H} `{GroupAction G H}
+  (x : carrier H) (s : BG_State G) (m : BG_Move s) :
+  BG_State_act x (exec_move m) =
+  exec_move (BG_Move_act x s m).
+Proof.
+  apply BG_State_ext.
+  - destruct m; reflexivity.
+  - destruct m; reflexivity.
+  - destruct m; simpl.
+    + reflexivity.
+    + admit.
+Admitted.
+
+Axiom cheat : forall {X}, X.
+
+Definition Bear_Bisim {G} {H} `{GroupAction G H} :
+  InvertibleBisim (BearGame G) (BearGame G).
+Proof.
+  unshelve econstructor.
+  - exact (fun s s' => { x : carrier H & BG_State_act x s = s' }).
+  - simpl.
+    intros s s' [x Hx] m.
+    rewrite <- Hx.
+    apply BG_Move_act.
+    exact m.
+  - simpl; intros s s' [x Hx] m.
+    destruct m.
+    + apply BearMove.
+      * rewrite <- Hx in e; auto.
+      * unshelve econstructor.
+        -- exact (act (inv x) (b_dest b)).
+        -- apply f_equal with (f := BG_State_act (inv x)) in Hx.
+           rewrite <- BG_State_act_comp in Hx.
+           rewrite inv_left in Hx.
+           rewrite BG_State_act_id in Hx.
+           rewrite Hx.
+           apply act_edge.
+           apply b.
+        -- apply cheat.
+    + apply HunterMove.
+      * rewrite <- Hx in e; auto.
+      * unshelve econstructor.
+        -- exact (act (inv x) (h_orig h)).
+        -- exact (act (inv x) (h_dest h)).
+        -- apply cheat.
+        -- apply act_edge.
+           apply h.
+        -- apply cheat.
+        -- apply cheat.
+  - simpl; intros s m s' [x Hx].
+    exists (BG_State_act x s).
+    apply BG_Move_act.
+    exact m.
+  - simpl; intros s m s' [x Hx].
+    exists (BG_State_act (inv x) s).
+    apply BG_Move_act.
+    exact m.
+  - simpl; intros s s' [x Hx].
+    rewrite <- Hx; auto.
+  - intros s s' [x Hx]; simpl.
+    unfold atomic_res.
+    rewrite <- Hx.
+    simpl.
+    destruct (to_play s).
+    + destruct (enum_moves s) eqn:?.
+      * destruct (enum_moves (BG_State_act x s)); auto.
+        apply BG_Move_act with (x := inv x) in b.
+        rewrite <- BG_State_act_comp in b.
+        rewrite inv_left in b.
+        rewrite BG_State_act_id in b.
+        pose proof (@enum_all (BearGame G) s b).
+        simpl in H1.
+        rewrite Heql in H1.
+        destruct H1.
+      * destruct (enum_moves (BG_State_act x s)) eqn:?; auto.
+        clear Heql.
+        apply BG_Move_act with (x := x) in b.
+        pose proof (@enum_all (BearGame G) (BG_State_act x s) b).
+        simpl in H1.
+        rewrite Heql0 in H1.
+        destruct H1.
+    + destruct (enum_moves s) eqn:?.
+      * destruct (enum_moves (BG_State_act x s)); auto.
+        apply BG_Move_act with (x := inv x) in b.
+        rewrite <- BG_State_act_comp in b.
+        rewrite inv_left in b.
+        rewrite BG_State_act_id in b.
+        pose proof (@enum_all (BearGame G) s b).
+        simpl in H1.
+        rewrite Heql in H1.
+        destruct H1.
+      * destruct (enum_moves (BG_State_act x s)) eqn:?; auto.
+        clear Heql.
+        apply BG_Move_act with (x := x) in b.
+        pose proof (@enum_all (BearGame G) (BG_State_act x s) b).
+        simpl in H1.
+        rewrite Heql0 in H1.
+        destruct H1.
+  - simpl; intros s s' m [x Hx].
+    destruct Hx; simpl.
+    exists x.
+    apply BG_Move_act_exec.
+  - simpl; intros s s' m [x Hx].
+    exists x.
+    destruct Hx.
+    simpl.
+    apply BG_State_ext.
+    + destruct m; reflexivity.
+    + destruct m; simpl; auto.
+      rewrite <- act_comp.
+      rewrite inv_right.
+      apply act_id.
+    + destruct m; simpl; auto.
+      apply sorted_list_eq.
+      * apply insertion_sort_sorts.
+      * apply insert_sorted.
+        apply insertion_sort_sorts.
+      * apply cheat.
+      * apply insertion_sort_NoDup.
+        apply FinFun.Injective_map_NoDup.
+        -- cbv; apply act_inj.
+        -- apply insert_NoDup.
+           ++ apply insertion_sort_NoDup.
+              apply NoDup_remove.
+              apply s.
+           ++ rewrite insertion_sort_In.
+              rewrite In_remove_iff.
+              intros [pf1 pf2].
+              apply pf1.
+              f_equal.
+              apply h; simpl.
+              rewrite insertion_sort_In.
+              rewrite in_map_iff.
+              exists ((inv x) # (h_dest h)); split; auto.
+              rewrite <- act_comp.
+              rewrite inv_right.
+              apply act_id.
+      * apply insert_NoDup.
+        -- apply insertion_sort_NoDup.
+           apply NoDup_remove.
+           apply insertion_sort_NoDup.
+           apply FinFun.Injective_map_NoDup.
+           ++ cbv; apply act_inj.
+           ++ apply s.
+        -- rewrite insertion_sort_In.
+           rewrite In_remove_iff.
+           intros [pf1 pf2].
+           apply pf1.
+           apply h; auto.
+  - simpl; intros s s' m [x Hx].
+    destruct Hx; simpl.
+    destruct m; simpl.
+    + f_equal.
+      apply BearMv_ext.
+      simpl.
+      rewrite <- act_comp.
+      rewrite inv_right.
+      apply act_id.
+    + f_equal.
+      apply HunterMv_ext.
+      * simpl.
+        rewrite <- act_comp.
+        rewrite inv_right.
+        apply act_id.
+      * simpl.
+        rewrite <- act_comp.
+        rewrite inv_right.
+        apply act_id.
+  - intros s s' m [x Hx]; simpl.
+    destruct Hx; simpl.
+    destruct m; simpl.
+    + f_equal.
+      apply BearMv_ext; simpl.
+      rewrite <- act_comp.
+      rewrite inv_left.
+      apply act_id.
+    + f_equal.
+      apply HunterMv_ext; simpl.
+      * rewrite <- act_comp.
+        rewrite inv_left.
+        apply act_id.
+      * rewrite <- act_comp.
+        rewrite inv_left.
+        apply act_id.
+  - intros s m s' [x Hx].
+    simpl in *.
+    rewrite BG_Move_act_exec in Hx.
+    auto.
+  - intros s m s' [x Hx].
+    exists x; reflexivity.
+  - intros s m s' [x Hx].
+    simpl in *.
+    rewrite <- BG_Move_act_exec.
+    rewrite <- Hx.
+    rewrite <- BG_State_act_comp.
+    rewrite inv_left.
+    apply BG_State_act_id.
+  - intros s m s' [x Hx].
+    exists x; simpl.
+    rewrite <- BG_State_act_comp.
+    rewrite inv_right.
+    apply BG_State_act_id.
+Defined.
+
+Class OrbitSelector G H `{GroupAction G H} : Type := {
+  select : GameState (BearGame G) -> GameState (BearGame G);
+  select_act : forall s, { x : carrier H & BG_State_act x s = select s };
+  select_functional : forall s x, select (BG_State_act x s) = select s;
+  }.
+
+Global Instance Bear_Sym {G} {H} `{OrbitSelector G H} : Symmetry (BearGame G).
+Proof.
+  unshelve econstructor.
+  - exact Bear_Bisim.
+  - exact select.
+  - intro s; exists id.
+    apply BG_State_act_id.
+  - intros s s' [x Hx].
+    exists (inv x).
+    rewrite <- Hx.
+    rewrite <- BG_State_act_comp.
+    rewrite inv_left.
+    apply BG_State_act_id.
+  - intros s1 s2 s3 [x Hx] [y Hy].
+    exists (y ** x).
+    rewrite BG_State_act_comp.
+    congruence.
+  - apply select_act.
+  - intros s s' [x Hx].
+    rewrite <- Hx.
+    symmetry; apply select_functional.
+Defined.
+
+Definition Bear_TB (G : Graph) (H : Group) `{OrbitSelector G H} `{hsh : IntHash (GameState (BearGame G))}
   : OCamlTablebase (BearGame G) := certified_TB.
diff --git a/theory/Bear/GroupAction.v b/theory/Bear/GroupAction.v
new file mode 100644
index 0000000..9b66b67
--- /dev/null
+++ b/theory/Bear/GroupAction.v
@@ -0,0 +1,46 @@
+Require Import TBGen.Bear.Graph.
+
+Record Group : Type := {
+  carrier : Type;
+
+  id : carrier;
+  mult : carrier -> carrier -> carrier;
+  inv : carrier -> carrier;
+
+  assoc : forall x y z, mult x (mult y z) = mult (mult x y) z;
+  id_left : forall x, mult id x = x;
+  id_right : forall x, mult x id = x;
+
+  inv_left : forall x, mult (inv x) x = id;
+  inv_right : forall x, mult x (inv x) = id;
+  }.
+
+Arguments id {_}.
+Arguments mult {_} _ _.
+Arguments inv {_} _.
+
+Infix "**" := mult (at level 10).
+
+Class GroupAction (G : Graph) (H : Group) : Type := {
+  act : carrier H -> Vert G -> Vert G;
+  act_id : forall v, act id v = v;
+  act_comp : forall v x y, act (x ** y) v = act x (act y v);
+  act_edge : forall (x : carrier H) (v v' : Vert G),
+    List.In v' (successors v) ->
+    List.In (act x v') (successors (act x v));
+  }.
+
+Arguments act {_} {_} {_} _ _.
+
+Infix "#" := act (at level 5).
+
+Lemma act_inj {G} {H} `{GroupAction G H} :
+  forall x v v', x # v = x # v' -> v = v'.
+Proof.
+  intros x v v' pf.
+  apply f_equal with (f := act (inv x)) in pf.
+  repeat rewrite <- act_comp in pf.
+  rewrite inv_left in pf.
+  repeat rewrite act_id in pf.
+  auto.
+Qed.
diff --git a/theory/Bear/RomanWheel.v b/theory/Bear/RomanWheel.v
index ab9e2e9..2935fad 100644
--- a/theory/Bear/RomanWheel.v
+++ b/theory/Bear/RomanWheel.v
@@ -698,5 +698,3 @@ Global Instance IntHash_RW : IntHash (Game.GameState (BearGame RomanWheel)) := {
   hash := hash_RW_State;
   hash_inj := hash_RW_State_inj;
   |}.
-
-Definition RW_TB := Bear_TB RomanWheel.
diff --git a/theory/Bear/RomanWheelSym.v b/theory/Bear/RomanWheelSym.v
new file mode 100644
index 0000000..dbd643a
--- /dev/null
+++ b/theory/Bear/RomanWheelSym.v
@@ -0,0 +1,240 @@
+Require Import List.
+Import ListNotations.
+
+Require Import PrimInt63.
+Require Import Uint63.
+Require Import ZArith.
+Require Import Lia.
+
+Require Import TBGen.Util.IntHash.
+Require Import TBGen.Bear.Graph.
+Require Import TBGen.Bear.BearGame.
+Require Import TBGen.TB.TB.
+Require Import TBGen.Bear.RomanWheel.
+
+Require Import TBGen.Bear.GroupAction.
+
+Definition Fin n : Type :=
+  { i : nat & i < n }.
+
+Definition val {n} (i : Fin n) : nat :=
+  projT1 i.
+
+(* technically doesn't need proof irrel. *)
+Lemma val_inj {n} (i j : Fin n) :
+  val i = val j -> i = j.
+Proof.
+  destruct i as [x x_pf].
+  destruct j as [y y_pf]; simpl.
+  intro pf; subst.
+  assert (x_pf = y_pf) by
+    apply ProofIrrelevance.proof_irrelevance.
+  subst; reflexivity.
+Qed.
+
+Definition Fin_zero {n} : Fin (S n).
+Proof.
+  exists 0; lia.
+Defined.
+
+Definition Fin_plus {n} : Fin n -> Fin n -> Fin n.
+Proof.
+  intros [x x_pf] [y y_pf].
+  exists ((x + y) mod n).
+  apply Nat.mod_upper_bound; lia.
+Defined.
+
+Lemma val_plus {n} (i j : Fin n) :
+  val (Fin_plus i j) = (val i + val j) mod n.
+Proof.
+  destruct i,j; simpl.
+  reflexivity.
+Qed.
+
+Definition Fin_inv {n} : Fin n -> Fin n.
+Proof.
+  intros [x x_pf].
+  exists (
+    match x with
+    | 0 => 0
+    | _ => n - x
+    end).
+  destruct x; lia.
+Defined.
+
+Lemma val_inv {n} (i : Fin n) :
+  val (Fin_inv i) =
+  match val i with
+  | 0 => 0
+  | _ => n - val i
+  end.
+Proof.
+  destruct i; reflexivity.
+Qed.
+
+Definition Z_8 : Group.
+Proof.
+  refine {|
+    carrier := Fin 8;
+    id := Fin_zero;
+    mult := Fin_plus;
+    inv := Fin_inv;
+    assoc := _;
+    id_left := _;
+    id_right := _;
+    inv_left := _;
+    inv_right := _;
+  |}.
+  - intros.
+    apply val_inj.
+    repeat rewrite val_plus.
+    rewrite Nat.Div0.add_mod_idemp_r.
+    rewrite Nat.Div0.add_mod_idemp_l.
+    now rewrite Nat.add_assoc.
+  - intros [x x_small].
+    apply val_inj.
+    rewrite val_plus.
+    simpl val.
+    rewrite Nat.mod_small; auto.
+  - intros [x x_small].
+    apply val_inj.
+    rewrite val_plus.
+    simpl val.
+    rewrite Nat.mod_small; auto; lia.
+  - intros [x x_small].
+    apply val_inj.
+    rewrite val_plus.
+    rewrite val_inv.
+    simpl val.
+    destruct x.
+    + reflexivity.
+    + assert (8 - S x + S x = 8) by lia.
+      rewrite H; reflexivity.
+  - intros [x x_small].
+    apply val_inj.
+    rewrite val_plus.
+    rewrite val_inv.
+    simpl val.
+    destruct x.
+    + reflexivity.
+    + assert (S x + (8 - S x) = 8) by lia.
+      rewrite H; reflexivity.
+Defined.
+
+Fixpoint rotate_spoke (n : nat) (s : Spoke) : Spoke :=
+  match n with
+  | 0 => s
+  | S m => clockwise (rotate_spoke m s)
+  end.
+
+Lemma rotate_spoke_plus (m n : nat) : forall (s : Spoke),
+  rotate_spoke (m + n) s =
+  rotate_spoke m (rotate_spoke n s).
+Proof.
+  induction m; intro.
+  - reflexivity.
+  - simpl.
+    now rewrite IHm.
+Qed.
+
+Lemma rotate_8 : forall s,
+  rotate_spoke 8 s = s.
+Proof.
+  intros []; reflexivity.
+Qed.
+
+Lemma rotate_mult_8 (n : nat) : forall (s : Spoke),
+  rotate_spoke (8 * n) s = s.
+Proof.
+  induction n; intro.
+  - reflexivity.
+  - rewrite <- mult_n_Sm.
+    rewrite rotate_spoke_plus.
+    rewrite rotate_8.
+    apply IHn.
+Qed.
+
+Lemma rotate_mod_8 (n : nat) : forall (s : Spoke),
+  rotate_spoke n s = rotate_spoke (n mod 8) s.
+Proof.
+  intro s.
+  rewrite (Nat.Div0.div_mod n 8) at 1.
+  rewrite rotate_spoke_plus.
+  now rewrite rotate_mult_8.
+Qed.
+
+Definition rotate_vert (n : nat) (v : RWVert) : RWVert :=
+  match v with
+  | Center => Center
+  | SpokeVert s l => SpokeVert (rotate_spoke n s) l
+  end.
+
+Global Instance RW_Z_8 : GroupAction RomanWheel Z_8.
+Proof.
+  refine {|
+    act := fun (x : carrier Z_8) (v : Vert RomanWheel) =>
+      rotate_vert (val x) v;
+    act_id := _;
+    act_comp := _;
+    act_edge := _;
+  |}.
+  - intros []; reflexivity.
+  - intros [] x y.
+    + reflexivity.
+    + simpl; f_equal.
+      rewrite val_plus.
+      rewrite <- rotate_mod_8.
+      now rewrite rotate_spoke_plus.
+  - intros x v v' pf.
+    destruct v.
+    + simpl rotate_vert.
+      apply cheat.
+    + apply cheat.
+Defined.
+
+Definition spoke_nat (s : Spoke) : nat :=
+  match s with
+  | S1 => 0
+  | S2 => 7
+  | S3 => 6
+  | S4 => 5
+  | S5 => 4
+  | S6 => 3
+  | S7 => 2
+  | S8 => 1
+  end.
+
+Lemma spoke_nat_small s : spoke_nat s < 8.
+Proof.
+  destruct s; simpl; lia.
+Qed.
+
+Definition spoke_Fin (s : Spoke) : Fin 8 :=
+  existT _ (spoke_nat s) (spoke_nat_small s).
+
+Definition compute_rotation (s : BG_State RomanWheel) : Fin 8.
+Proof.
+  destruct (bear s) eqn:?.
+  - destruct s; simpl in *.
+    destruct hunters.
+    + discriminate.
+    + destruct r.
+      * elim bear_not_hunter; now left.
+      * exact (spoke_Fin s).
+  - exact (spoke_Fin s0).
+Defined.
+
+Global Instance RW_OrbitSelector : OrbitSelector RomanWheel Z_8.
+Proof.
+  refine {|
+    select := fun s => BG_State_act (compute_rotation s) s
+  |}.
+  - intro s.
+    exists (compute_rotation s).
+    reflexivity.
+  - apply cheat.
+Defined.
+
+Definition RW_TB :=
+  Bear_TB RomanWheel Z_8.
+
diff --git a/theory/SymTB/OCamlTB.v b/theory/SymTB/OCamlTB.v
index 4ede8cf..47059ae 100644
--- a/theory/SymTB/OCamlTB.v
+++ b/theory/SymTB/OCamlTB.v
@@ -3,7 +3,7 @@ Import ListNotations.
 Require Import Compare_dec.
 
 Require Import Games.Game.Game.
-Require Import TBGen.TB.TB.
+Require Import TBGen.SymTB.TB.
 Require Import TBGen.Util.OMap.
 Require Import TBGen.Util.IntHash.
 Require Import Games.Game.Player.
@@ -21,15 +21,15 @@ Record OCamlTablebase (G : Game) `{IntHash (GameState G)} : Type := {
 Arguments tb_whites {_} {_} _.
 Arguments tb_blacks {_} {_} _.
 
-Definition query_TB {G} `{IntHash (GameState G)}
+Definition query_TB {G} `{IntHash (GameState G)} `{Symmetry G}
   (tb : OCamlTablebase G) (s : GameState G) : option (Player * nat) :=
   match to_play s with
-  | White => hash_lookup s (tb_whites tb)
-  | Black => hash_lookup s (tb_blacks tb)
+  | White => hash_lookup (normalize s) (tb_whites tb)
+  | Black => hash_lookup (normalize s) (tb_blacks tb)
   end.
 
 Record CorrectTablebase {M} `{IntMap M}
-  {G} `{IntHash (GameState G)} (tb : OCamlTablebase G) := {
+  {G} `{IntHash (GameState G)} `{Symmetry G} (tb : OCamlTablebase G) := {
 
   query_mate : forall s pl n,
     query_TB tb s = Some (pl, n) ->
@@ -54,7 +54,7 @@ Arguments query_draw {_} {_} {_} {_}.
 
 Definition certified_TB {M} `{IntMap M}
   {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G}
-  `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} :
+  `{NiceGame G} `{Symmetry G} `{forall s : GameState G, Discrete (Move s)} :
   OCamlTablebase G :=
   match TB_final with
   | Build_TB _ _ wps bps _ _ =>
@@ -66,7 +66,7 @@ Definition certified_TB {M} `{IntMap M}
 
 Lemma certified_TB_whites {M} `{IntMap M}
   {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G}
-  `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} :
+  `{NiceGame G} `{Symmetry G} `{forall s : GameState G, Discrete (Move s)} :
   tb_whites certified_TB = white_positions TB_final.
 Proof.
   unfold certified_TB.
@@ -75,7 +75,7 @@ Qed.
 
 Lemma certified_TB_blacks {M} `{IntMap M}
   {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G}
-  `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} :
+  `{NiceGame G} `{Symmetry G} `{forall s : GameState G, Discrete (Move s)} :
   tb_blacks certified_TB = black_positions TB_final.
 Proof.
   unfold certified_TB.
@@ -84,7 +84,7 @@ Qed.
 
 Lemma certified_TB_correct {M} `{IntMap M}
   {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G}
-  `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} :
+  `{NiceGame G} `{Symmetry G} `{forall s : GameState G, Discrete (Move s)} :
   CorrectTablebase certified_TB.
 Proof.
   constructor;
@@ -153,7 +153,7 @@ Qed.
 
 CoFixpoint tb_strat {M} {G} (s : GameState G) pl
   `{IntMap M}
-  `{IntHash (GameState G)}
+  `{IntHash (GameState G)} `{Symmetry G}
   (tb : OCamlTablebase G) : strategy pl s.
 Proof.
   - destruct (atomic_res s) eqn:s_res.
@@ -164,7 +164,7 @@ Proof.
              (query_TB tb (exec_move s m1))
              (query_TB tb (exec_move s m2))
           ) (enum_moves s) (move_enum_all_ne s_res)).
-        exact (eloise_strategy s_res s_play m (@tb_strat _ _ _ pl _ _ tb)).
+        exact (eloise_strategy s_res s_play m (@tb_strat _ _ _ pl _ _ _ tb)).
       * exact (abelard_strategy s_res s_play (fun m =>
-          @tb_strat _ _ _ pl _ _ tb)).
+          @tb_strat _ _ _ pl _ _ _ tb)).
 Defined.
diff --git a/theory/SymTB/TB.v b/theory/SymTB/TB.v
index 1906727..08a1928 100644
--- a/theory/SymTB/TB.v
+++ b/theory/SymTB/TB.v
@@ -46,7 +46,7 @@ Class Reversible (G : Game) : Type := {
   }.
 
 Class Symmetry (G : Game) : Type := {
-  auto : Bisim G G;
+  auto : InvertibleBisim G G;
   auto_refl : forall s, bisim G G auto s s;
   auto_sym : forall s s', bisim G G auto s s' -> bisim G G auto s' s;
   auto_trans : forall s1 s2 s3, bisim G G auto s1 s2 -> bisim G G auto s2 s3 -> bisim G G auto s1 s3;
@@ -143,18 +143,13 @@ Proof.
   apply normalize_bisim.
 Qed.
 
-Definition inv_forward s m s' :
-  bisim G G auto (exec_move s m) s' ->
-  { s'' : GameState G & Move s'' }.
-Admitted.
-
-Lemma inv_forward_correct s m s' (b : bisim G G auto (exec_move s m) s') :
-  exec_move (projT1 (inv_forward s m s' b)) (projT2 (inv_forward s m s' b)) = s'.
-Admitted.
-
-Lemma exec_inv_forward s m s' (b : bisim G G auto (exec_move s m) s') :
-  bisim G G auto s (projT1 (inv_forward s m s' b)).
-Admitted.
+Lemma normalize_idem s :
+  normalize (normalize s) = normalize s.
+Proof.
+  symmetry.
+  apply normalize_functional.
+  apply normalize_bisim.
+Qed.
 
 Variant Step :=
   | Eloise : Step
@@ -851,9 +846,9 @@ Proof.
         -- destruct (mate_S_lemma _ v sm) as [m smm].
            apply (mate_lbp _ v) in smm; [|now rewrite 
              to_play_exec_move, s_play].
-           pose proof (inv_forward_correct s m _
+           pose proof (inv_forward_correct G G _ s m _
              (normalize_bisim (exec_move s m))) as pf.
-           pose proof (exec_inv_forward s m _
+           pose proof (exec_inv_forward _ _ _ s m _
              (normalize_bisim (exec_move s m))) as pf'.
            destruct inv_forward; simpl in *.
            rewrite (normalize_functional _ _ pf').
@@ -966,10 +961,10 @@ Proof.
            specialize (m pf).
            pose (mate_eq sm m); lia.
       * destruct (mate_S_lemma _ v sm) as [m smm].
-        pose proof (inv_forward_correct s m _ (normalize_bisim _)).
-        pose proof (exec_inv_forward s m _ (normalize_bisim _)).
+        pose proof (inv_forward_correct _ _ _ s m _ (normalize_bisim _)).
+        pose proof (exec_inv_forward _ _ _ s m _ (normalize_bisim _)).
         destruct inv_forward; simpl in *.
-        rewrite (normalize_functional _ _ H7).
+        rewrite (normalize_functional _ _ X).
         apply in_map.
         rewrite in_concat.
         exists (enum_preds (exec_move x m0)).
@@ -1019,26 +1014,38 @@ Proof.
                  (exec_move (normalize t)
                     (forward G G auto (normalize_bisim t) m')))
               (add_positions (black_positions tb) Black
-                 (curr tb) (last_black_positions tb))) eqn:Hsm; try congruence.
+                 (curr tb) (last_black_positions tb))) as [[[|] n]|] eqn:Hsm; try congruence.
         clear Hforall.
         destruct (hash_lookup_adds_invert _ _ _ _ Hsm) as [HIn|tb_sm].
         + destruct (in_map_sig HIn) as [s' [G1 G2]]; inversion G1; subst.
           pose (lbp_mate _ v G2) as sm.
           rewrite tb_step in sm; simpl in sm.
-          destruct sm as [w' [w'_d w'_m]].
+          apply mate_of_normal_mate in sm.
+          apply bisim_mate with (B := auto) (s' := exec_move t m') in sm;
+            [|apply auto_sym; apply exec_forward].
+          destruct sm as [w' []].
           exists w'; split; [lia|auto].
-        + pose (@tb_mate _ v (exec_move s m') Black n) as sm.
+        + pose (@tb_mate _ v (normalize (exec_move (normalize t) (forward G G auto (normalize_bisim t) m'))) Black n) as sm.
           unfold tb_lookup in sm.
+          rewrite to_play_normalize in sm.
           rewrite to_play_exec_move in sm.
-          rewrite s_play in sm; simpl in sm.
-          destruct (sm tb_sm) as [w' [w'_d w'_m]].
+          rewrite to_play_normalize in sm.
+          rewrite t_play in sm; simpl in sm.
+          rewrite normalize_idem in sm.
+          pose (sm tb_sm) as sm'.
+          apply mate_of_normal_mate in sm'.
+          apply bisim_mate with (B := auto) (s' := exec_move t m') in sm';
+            [| apply auto_sym; apply exec_forward].
+          destruct sm' as [w' [w'_d w'_m]].
           exists w'; split; auto.
-          pose (@tb_small _ v (exec_move s m') Black n).
+          pose (@tb_small _ v (exec_move (normalize t) (forward G G auto (normalize_bisim t) m')) Black n).
           unfold tb_lookup in l.
           rewrite to_play_exec_move in l.
-          rewrite s_play in l; specialize (l tb_sm); lia.
+          rewrite to_play_normalize in l.
+          rewrite t_play in l; specialize (l tb_sm); lia.
       }
-      pose (w' := @abelard_win _ Black _ s_res s_play (fun m => projT1 (X m))).
+      pose (w' := @abelard_win _ Black _ t_res t_play (fun m => projT1 (X m))).
+      apply mate_to_normal_mate.
       exists w'; simpl; split.
       * f_equal.
         apply PeanoNat.Nat.le_antisymm.
@@ -1066,23 +1073,26 @@ Proof.
       rewrite nodup_In in HIn.
       rewrite In_filter_Nones_iff in HIn.
       destruct HIn as [Hs1 Hs2].
-      destruct (in_concat_sig _ _ Hs2) as [xs [Hxs1 Hxs2]].
+      apply in_map_sig in Hs2.
+      destruct Hs2 as [t [Ht1 Ht2]].
+      destruct (in_concat_sig _ _ Ht2) as [xs [Hxs1 Hxs2]].
       destruct (in_map_sig Hxs1) as [s' [Hs'1 Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hxs2) as [m Hm]; subst.
       pose (lbp_mate _ v Hs'2) as sm.
       rewrite tb_step in sm; simpl in sm.
-      assert (to_play s = White) as s_play.
+      assert (to_play t = White) as s_play.
       { apply opp_inj.
         rewrite <- (to_play_exec_move m).
         apply (lbp_black _ v); auto.
       }
       destruct sm as [w [w_d w_m]].
-      destruct (atomic_res s) eqn:s_res.
+      destruct (atomic_res t) eqn:s_res.
       { exfalso.
         pose proof (enum_all m) as pf.
         rewrite (atomic_res_nil s_res) in pf.
         exact pf.
       }
+      apply mate_to_normal_mate.
       (* can this be cleaned up? *)
       exists (eloise_win s_res s_play m w).
       split; [simpl; congruence|].
@@ -1123,7 +1133,8 @@ Proof.
            ++ rewrite in_map_iff in pf.
               destruct pf as [s' [Hs'1 Hs'2]].
               inversion Hs'1; subst.
-              pose (lbp_mate _ v Hs'2).
+              pose (lbp_mate _ v Hs'2) as m.
+              apply mate_of_normal_mate in m.
               pose (mate_eq sm m); lia.
            ++ epose (tb_small _ v).
               unfold tb_lookup in l.
@@ -1134,15 +1145,21 @@ Proof.
               rewrite s_play in m.
               specialize (m pf).
               pose (mate_eq sm m); lia.
-        -- rewrite in_concat.
-           destruct (mate_S_lemma _ v sm) as [m smm].
-           exists (enum_preds (exec_move s m)).
+        -- destruct (mate_S_lemma _ v sm) as [m smm].
+           apply (mate_lwp _ v) in smm; [|now rewrite 
+             to_play_exec_move, s_play].
+           pose proof (inv_forward_correct _ _ _ s m _
+             (normalize_bisim (exec_move s m))) as pf.
+           pose proof (exec_inv_forward _ _ _ s m _
+             (normalize_bisim (exec_move s m))) as pf'.
+           destruct inv_forward; simpl in *.
+           rewrite (normalize_functional _ _ pf').
+           apply in_map.
+           rewrite in_concat.
+           exists (enum_preds (normalize (exec_move s m))).
            split.
-           ++ apply in_map.
-              eapply (mate_lwp _ v).
-              rewrite to_play_exec_move, s_play; reflexivity.
-              exact smm.
-           ++ apply enum_preds_correct2.
+           ++ apply in_map; auto.
+           ++ rewrite <- pf; apply enum_preds_correct2.
       * rewrite forallb_forall.
         intros m _.
         destruct (mate_S_lemma _ v sm) as [m' smm'].
@@ -1161,14 +1178,19 @@ Proof.
               apply (unique_winner _ _ s).
               ** rewrite Hpl in sm.
                  now destruct sm.
-              ** eapply eloise_win; auto.
-                 { destruct (atomic_res s) eqn:s_res; auto.
+              ** apply win_of_normal_win.
+                 apply eloise_win with (m := m); auto.
+                 { rewrite atomic_res_normalize.
+                   destruct (atomic_res s) eqn:s_res; auto.
                    pose proof (enum_all m) as HIn.
+                   rewrite <- atomic_res_normalize in s_res.
                    rewrite (atomic_res_nil s_res) in HIn; destruct HIn.
                  }
-                 epose (@tb_mate _ v (exec_move s m)).
+                 { rewrite to_play_normalize; auto. }
+                 epose (@tb_mate _ v (exec_move (normalize s) m)).
                  unfold tb_lookup in m0.
                  rewrite to_play_exec_move in m0.
+                 rewrite to_play_normalize in m0.
                  rewrite s_play in m0; simpl in m0.
                  destruct (m0 _ _ pf); eauto.
         -- subst.
@@ -1176,39 +1198,49 @@ Proof.
            destruct (hash_lookup_adds_None_invert tb_sm).
            destruct sm as [w [w_d wm]].
            destruct w; [simpl in w_d; lia|congruence|].
-           pose (tb_None _ v (w m)).
+           pose (tb_None _ v (w (back G G auto (normalize_bisim b) m))).
            unfold tb_lookup in l.
            rewrite to_play_exec_move in l.
            rewrite s_play in l; simpl in l.
+           assert (normalize (exec_move b (back G G auto (normalize_bisim b) m)) = normalize (exec_move (normalize b) m)).
+           { apply normalize_functional;
+             apply exec_back.
+           }
+           rewrite H8 in l.
            specialize (l H7).
            simpl in w_d.
            inversion w_d as [w_d']; clear w_d.
-           assert (depth (w m) <= curr tb).
+           assert (depth (w (back G G auto (normalize_bisim b) m)) <= curr tb).
            { rewrite <- w_d'.
              apply list_max_is_max.
              rewrite in_map_iff.
-             exists m; split; auto.
+             eexists; split; auto.
              apply enum_all.
            }
-           assert (mate White (exec_move b m) (curr tb)).
-           { exists (w m).
+           assert (mate White (exec_move b (back G G auto (normalize_bisim b) m)) (curr tb)).
+           { exists (w _).
              split; [lia|].
              intro w'.
-             assert (depth (w m) = curr tb) by lia.
-             rewrite H8.
+             assert (depth (w (back G G auto (normalize_bisim b) m)) = curr tb) by lia.
+             rewrite H10.
              apply (tb_None _ v w').
              unfold tb_lookup.
-             rewrite to_play_exec_move, s_play; simpl; auto.
+             rewrite to_play_exec_move. rewrite s_play. simpl; auto.
+             rewrite H8; auto.
            }
            elim H6.
            rewrite in_map_iff.
-           exists (exec_move b m, (White, curr tb)).
+           exists (normalize (exec_move (normalize b) m) , (White, curr tb)).
            simpl; split; [reflexivity|].
            rewrite in_map_iff.
-           exists (exec_move b m); split; [reflexivity|].
+           exists (normalize (exec_move (normalize b) m)); split; [reflexivity|].
            eapply (mate_lwp _ v).
-           rewrite to_play_exec_move, s_play; reflexivity.
+           rewrite to_play_exec_move.
+           rewrite to_play_normalize.
+           rewrite s_play; reflexivity.
+           apply bisim_mate with (B := auto) (s' := exec_move (normalize b) m) in X.
            exact X.
+           apply exec_back.
     + unfold eloise_step.
       rewrite nodup_In.
       rewrite In_filter_Nones_iff; split.
@@ -1219,6 +1251,7 @@ Proof.
            destruct pf as [s' [Hs'1 Hs'2]].
            inversion Hs'1; subst.
            pose (lbp_mate _ v Hs'2).
+           apply mate_of_normal_mate in m.
            pose (mate_eq sm m); lia.
         -- epose (tb_small _ v).
            unfold tb_lookup in l.
@@ -1229,11 +1262,17 @@ Proof.
            rewrite s_play in m.
            specialize (m pf).
            pose (mate_eq sm m); lia.
-      * rewrite in_concat.
-        destruct (mate_S_lemma _ v sm) as [m smm].
-        exists (enum_preds (exec_move s m)).
+      * destruct (mate_S_lemma _ v sm) as [m smm].
+        pose proof (inv_forward_correct _ _ _ s m _ (normalize_bisim _)).
+        pose proof (exec_inv_forward _ _ _ s m _ (normalize_bisim _)).
+        destruct inv_forward; simpl in *.
+        rewrite (normalize_functional _ _ X).
+        apply in_map.
+        rewrite in_concat.
+        exists (enum_preds (exec_move x m0)).
         split.
         -- apply in_map.
+           rewrite H6.
            eapply (mate_lwp _ v).
            rewrite to_play_exec_move, s_play; reflexivity.
            exact smm.
@@ -1247,51 +1286,68 @@ Proof.
       destruct HIn as [HIn' Hforall].
       rewrite In_filter_Nones_iff in HIn'.
       destruct HIn' as [Hs1 Hs2].
-      destruct (in_concat_sig _ _ Hs2) as [xs [Hxs1 Hxs2]].
+      apply in_map_sig in Hs2.
+      destruct Hs2 as [t [Ht1 Ht2]].
+      destruct (in_concat_sig _ _ Ht2) as [xs [Hxs1 Hxs2]].
       destruct (in_map_sig Hxs1) as [s' [Hs'1 Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hxs2) as [m Hm]; subst.
       pose (lwp_mate _ v Hs'2) as sm.
       rewrite tb_step in sm; simpl in sm.
-      assert (to_play s = Black) as s_play.
+      assert (to_play t = Black) as t_play.
       { apply opp_inj.
         rewrite <- (to_play_exec_move m).
         apply (lwp_white _ v); auto.
       }
       destruct sm as [w [w_d w_m]].
-      destruct (atomic_res s) eqn:s_res.
+      destruct (atomic_res t) eqn:t_res.
       { exfalso.
         pose proof (enum_all m) as pf.
-        rewrite (atomic_res_nil s_res) in pf.
+        rewrite (atomic_res_nil t_res) in pf.
         exact pf.
       }
       rewrite forallb_forall in Hforall.
       rewrite tb_step in *.
       simpl in *.
-      assert (forall m, {w : win White (exec_move s m) & depth w <= curr tb /\ minimal w}).
+      assert (forall m, {w : win White (exec_move t m) & depth w <= curr tb /\ minimal w}).
       { intro m'.
-        specialize (Hforall m' (enum_all m')).
-        destruct (hash_lookup (exec_move s m')
-          (add_positions (white_positions tb) White (curr tb)
-          (last_white_positions tb))) as [[[|] n]|] eqn:Hsm; try congruence.
+        specialize (Hforall (forward G G auto (normalize_bisim _) m') (enum_all _)).
+        destruct (hash_lookup
+              (normalize
+                 (exec_move (normalize t)
+                    (forward G G auto (normalize_bisim t) m')))
+              (add_positions (white_positions tb) White
+                 (curr tb) (last_white_positions tb))) as [[[|] n]|] eqn:Hsm; try congruence.
         clear Hforall.
         destruct (hash_lookup_adds_invert _ _ _ _ Hsm) as [HIn|tb_sm].
         + destruct (in_map_sig HIn) as [s' [G1 G2]]; inversion G1; subst.
           pose (lwp_mate _ v G2) as sm.
           rewrite tb_step in sm; simpl in sm.
-          destruct sm as [w' [w'_d w'_m]].
+          apply mate_of_normal_mate in sm.
+          apply bisim_mate with (B := auto) (s' := exec_move t m') in sm;
+            [|apply auto_sym; apply exec_forward].
+          destruct sm as [w' []].
           exists w'; split; [lia|auto].
-        + pose (@tb_mate _ v (exec_move s m') White n) as sm.
+        + pose (@tb_mate _ v (normalize (exec_move (normalize t) (forward G G auto (normalize_bisim t) m'))) White n) as sm.
           unfold tb_lookup in sm.
+          rewrite to_play_normalize in sm.
           rewrite to_play_exec_move in sm.
-          rewrite s_play in sm; simpl in sm.
-          destruct (sm tb_sm) as [w' [w'_d w'_m]].
+          rewrite to_play_normalize in sm.
+          rewrite t_play in sm; simpl in sm.
+          rewrite normalize_idem in sm.
+          pose (sm tb_sm) as sm'.
+          apply mate_of_normal_mate in sm'.
+          apply bisim_mate with (B := auto) (s' := exec_move t m') in sm';
+            [| apply auto_sym; apply exec_forward].
+          destruct sm' as [w' [w'_d w'_m]].
           exists w'; split; auto.
-          pose (@tb_small _ v (exec_move s m') White n).
+          pose (@tb_small _ v (exec_move (normalize t) (forward G G auto (normalize_bisim t) m')) White n).
           unfold tb_lookup in l.
           rewrite to_play_exec_move in l.
-          rewrite s_play in l; specialize (l tb_sm); lia.
+          rewrite to_play_normalize in l.
+          rewrite t_play in l; specialize (l tb_sm); lia.
       }
-      pose (w' := @abelard_win _ White _ s_res s_play (fun m => projT1 (X m))).
+      pose (w' := @abelard_win _ White _ t_res t_play (fun m => projT1 (X m))).
+      apply mate_to_normal_mate.
       exists w'; simpl; split.
       * f_equal.
         apply PeanoNat.Nat.le_antisymm.
@@ -1319,23 +1375,26 @@ Proof.
       rewrite nodup_In in HIn.
       rewrite In_filter_Nones_iff in HIn.
       destruct HIn as [Hs1 Hs2].
-      destruct (in_concat_sig _ _ Hs2) as [xs [Hxs1 Hxs2]].
+      apply in_map_sig in Hs2.
+      destruct Hs2 as [t [Ht1 Ht2]].
+      destruct (in_concat_sig _ _ Ht2) as [xs [Hxs1 Hxs2]].
       destruct (in_map_sig Hxs1) as [s' [Hs'1 Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hxs2) as [m Hm]; subst.
       pose (lwp_mate _ v Hs'2) as sm.
       rewrite tb_step in sm; simpl in sm.
-      assert (to_play s = Black) as s_play.
+      assert (to_play t = Black) as s_play.
       { apply opp_inj.
         rewrite <- (to_play_exec_move m).
         apply (lwp_white _ v); auto.
       }
       destruct sm as [w [w_d w_m]].
-      destruct (atomic_res s) eqn:s_res.
+      destruct (atomic_res t) eqn:s_res.
       { exfalso.
         pose proof (enum_all m) as pf.
         rewrite (atomic_res_nil s_res) in pf.
         exact pf.
       }
+      apply mate_to_normal_mate.
       (* can this be cleaned up? *)
       exists (eloise_win s_res s_play m w).
       split; [simpl; congruence|].
@@ -1417,25 +1476,31 @@ Proof.
       destruct HIn as [HIn' _].
       rewrite In_filter_Nones_iff in HIn'.
       destruct HIn' as [_ HIn].
-      rewrite in_concat in HIn.
-      destruct HIn as [l [Hl1 Hl2]].
+      rewrite in_map_iff in HIn.
+      destruct HIn as [t [Ht1 Ht2]].
+      rewrite in_concat in Ht2.
+      destruct Ht2 as [l [Hl1 Hl2]].
       rewrite in_map_iff in Hl1.
       destruct Hl1 as [s' [Hs' Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hl2) as [m]; subst.
       pose proof (lbp_black _ v _ Hs'2) as sm_play.
       rewrite to_play_exec_move in sm_play.
+      rewrite to_play_normalize.
       now apply opp_inj.
     + unfold eloise_step in HIn.
       rewrite nodup_In in HIn.
       rewrite In_filter_Nones_iff in HIn.
       destruct HIn as [_ HIn'].
-      rewrite in_concat in HIn'.
-      destruct HIn' as [l [Hl1 Hl2]].
+      rewrite in_map_iff in HIn'.
+      destruct HIn' as [t [Ht1 Ht2]].
+      rewrite in_concat in Ht2.
+      destruct Ht2 as [l [Hl1 Hl2]].
       rewrite in_map_iff in Hl1.
       destruct Hl1 as [s' [Hs' Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hl2) as [m]; subst.
       pose proof (lbp_black _ v _ Hs'2) as sm_play.
       rewrite to_play_exec_move in sm_play.
+      rewrite to_play_normalize.
       now apply opp_inj.
   (* lbp_black *)
   - simpl; intros s HIn.
@@ -1446,25 +1511,31 @@ Proof.
       destruct HIn as [HIn' _].
       rewrite In_filter_Nones_iff in HIn'.
       destruct HIn' as [_ HIn].
-      rewrite in_concat in HIn.
-      destruct HIn as [l [Hl1 Hl2]].
+      rewrite in_map_iff in HIn.
+      destruct HIn as [t [Ht1 Ht2]].
+      rewrite in_concat in Ht2.
+      destruct Ht2 as [l [Hl1 Hl2]].
       rewrite in_map_iff in Hl1.
       destruct Hl1 as [s' [Hs' Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hl2) as [m]; subst.
       pose proof (lwp_white _ v _ Hs'2) as sm_play.
       rewrite to_play_exec_move in sm_play.
+      rewrite to_play_normalize.
       now apply opp_inj.
     + unfold eloise_step in HIn.
       rewrite nodup_In in HIn.
       rewrite In_filter_Nones_iff in HIn.
       destruct HIn as [_ HIn'].
-      rewrite in_concat in HIn'.
-      destruct HIn' as [l [Hl1 Hl2]].
+      rewrite in_map_iff in HIn'.
+      destruct HIn' as [t [Ht1 Ht2]].
+      rewrite in_concat in Ht2.
+      destruct Ht2 as [l [Hl1 Hl2]].
       rewrite in_map_iff in Hl1.
       destruct Hl1 as [s' [Hs' Hs'2]]; subst.
       destruct (enum_preds_correct1 _ _ Hl2) as [m]; subst.
       pose proof (lwp_white _ v _ Hs'2) as sm_play.
       rewrite to_play_exec_move in sm_play.
+      rewrite to_play_normalize.
       now apply opp_inj.
 Defined.
 
@@ -1677,10 +1748,10 @@ Proof.
       length (last_white_positions tb) +
       length (last_black_positions tb) > 0).
     { destruct (to_play s) eqn:s_play.
-      + assert (In s (last_white_positions tb)).
+      + assert (In (normalize s) (last_white_positions tb)).
         { eapply (mate_lwp _ X0); eauto. }
         pose (In_length_pos _ _ H6); lia.
-      + assert (In s (last_black_positions tb)).
+      + assert (In (normalize s) (last_black_positions tb)).
         { eapply (mate_lbp _ X0); eauto. }
         pose (In_length_pos _ _ H6); lia.
     }
@@ -1832,24 +1903,24 @@ Proof.
       apply enum_states_correct.
     }
     destruct (to_play s) eqn:s_play.
-    + assert (In (s, (Black, 0)) (map (tag Black 0) (nodup IntHash_dec (enum_wins Black)))) as Hs.
+    + assert (In (normalize s, (Black, 0)) (map (tag Black 0) (nodup IntHash_dec (enum_norm_wins Black)))) as Hs.
       { rewrite in_map_iff.
-        exists s; split; [reflexivity|].
+        exists (normalize s); split; [reflexivity|].
         rewrite nodup_In.
         erewrite atomic_win_opp in s_play; [|exact s_res].
-        apply enum_wins_correct2; now destruct pl.
+        apply enum_norm_wins_correct2; now destruct pl.
       }
-      pose proof (hash_adds_ne_pos (map (tag Black 0) (nodup IntHash_dec (enum_wins Black)))
-        s (Black, 0) Hs); lia.
-    + assert (In (s, (White, 0)) (map (tag White 0) (nodup IntHash_dec (enum_wins White)))) as Hs.
+      pose proof (hash_adds_ne_pos (map (tag Black 0) (nodup IntHash_dec (enum_norm_wins Black)))
+        (normalize s) (Black, 0) Hs); lia.
+    + assert (In (normalize s, (White, 0)) (map (tag White 0) (nodup IntHash_dec (enum_norm_wins White)))) as Hs.
       { rewrite in_map_iff.
-        exists s; split; [reflexivity|].
+        exists (normalize s); split; [reflexivity|].
         rewrite nodup_In.
         erewrite atomic_win_opp in s_play; [|exact s_res].
-        apply enum_wins_correct2; now destruct pl.
+        apply enum_norm_wins_correct2; now destruct pl.
       }
-      pose proof (hash_adds_ne_pos (map (tag White 0) (nodup IntHash_dec (enum_wins White)))
-        s (White, 0) Hs); lia.
+      pose proof (hash_adds_ne_pos (map (tag White 0) (nodup IntHash_dec (enum_norm_wins White)))
+        (normalize s) (White, 0) Hs); lia.
   - intros s pl s_res.
     apply mate_TB_final_lookup.
     exists (atom_win s_res).
diff --git a/theory/Util/Bisim.v b/theory/Util/Bisim.v
index 0b10b39..11f4e0f 100644
--- a/theory/Util/Bisim.v
+++ b/theory/Util/Bisim.v
@@ -8,8 +8,26 @@ Require Import Games.Game.NoWorse.
 
 Require Import TBGen.Util.ListUtil.
 
-Record Bisim (G H : Game) : Type := {
-  bisim : GameState G -> GameState H -> Prop;
+(*
+Definition inv_forward s m s' :
+  bisim G G auto (exec_move s m) s' ->
+  { s'' : GameState G & Move s'' }.
+Proof.
+  intro pf.
+
+Admitted.
+
+Lemma inv_forward_correct s m s' (b : bisim G G auto (exec_move s m) s') :
+  exec_move (projT1 (inv_forward s m s' b)) (projT2 (inv_forward s m s' b)) = s'.
+Admitted.
+
+Lemma exec_inv_forward s m s' (b : bisim G G auto (exec_move s m) s') :
+  bisim G G auto s (projT1 (inv_forward s m s' b)).
+Admitted.
+*)
+
+Record InvertibleBisim (G H : Game) : Type := {
+  bisim : GameState G -> GameState H -> Type;
 
   forward : forall {s s'}, bisim s s' ->
     Move s -> Move s';
@@ -38,9 +56,28 @@ Record Bisim (G H : Game) : Type := {
   back_forward : forall s s' m (b : bisim s s'),
     back b (forward b m) = m;
 
+  inv_forward s m s' :
+    bisim (exec_move s m) s' ->
+    { s'' : GameState H & Move s'' };
+
+  inv_forward_correct s m s' (b : bisim (exec_move s m) s') :
+    exec_move (projT1 (inv_forward s m s' b)) (projT2 (inv_forward s m s' b)) = s';
+
+  exec_inv_forward s m s' (b : bisim (exec_move s m) s') :
+    bisim s (projT1 (inv_forward s m s' b));
+
+  inv_back s m s' :
+    bisim s' (exec_move s m) ->
+    { s'' : GameState G & Move s'' };
+
+  inv_back_correct s m s' (b : bisim s' (exec_move s m)) :
+    exec_move (projT1 (inv_back s m s' b)) (projT2 (inv_back s m s' b)) = s';
+
+  exec_inv_back s m s' (b : bisim s' (exec_move s m)) :
+    bisim (projT1 (inv_back s m s' b)) s;
   }.
 
-Definition Bisim_sym {G H} (B : Bisim G H) : Bisim H G.
+Definition Bisim_sym {G H} (B : InvertibleBisim G H) : InvertibleBisim H G.
 Proof.
   unshelve econstructor.
   - exact (fun s' s => bisim G H B s s').
@@ -48,23 +85,33 @@ Proof.
     apply (@back G H B).
   - simpl; intros s s'.
     apply (@forward G H B).
+  - intros.
+    eapply inv_back.
+    exact X.
+  - intros.
+    eapply inv_forward.
+    exact X.
   - intros; symmetry.
-    apply (to_play_bisim G H B _ _ H0).
+    apply (to_play_bisim G H B _ _ X).
   - intros; symmetry.
-    apply (atomic_bisim G H B _ _ H0).
+    apply (atomic_bisim G H B _ _ X).
   - simpl; intros. apply exec_back.
   - simpl; intros. apply exec_forward.
   - simpl; intros. apply back_forward.
   - simpl; intros. apply forward_back.
+  - apply inv_back_correct.
+  - apply exec_inv_back.
+  - apply inv_forward_correct.
+  - apply exec_inv_forward.
 Defined.
 
-Lemma bisim_sym {G H} (B : Bisim G H) s s' :
+Lemma bisim_sym {G H} (B : InvertibleBisim G H) s s' :
   bisim G H B s s' -> bisim H G (Bisim_sym B) s' s.
 Proof.
   simpl; auto.
 Qed.
 
-Fixpoint bisim_win {G H} {p} (B : Bisim G H) s s'
+Fixpoint bisim_win {G H} {p} (B : InvertibleBisim G H) s s'
   (b : bisim G H B s s') 
   (w : win p s) : win p s'.
 Proof.
@@ -103,7 +150,7 @@ Proof.
     apply list_max_is_max; auto.
 Qed.
 
-Lemma bisim_win_depth {G H} {p} (B : Bisim G H)
+Lemma bisim_win_depth {G H} {p} (B : InvertibleBisim G H)
   s (w : win p s) : forall s' (b : bisim G H B s s'),
   depth (bisim_win B s s' b w) = depth w.
 Proof.
@@ -130,7 +177,7 @@ Proof.
       * apply H.
 Qed.
 
-Lemma bisim_mate {G H} {p} {n} (B : Bisim G H) s s' :
+Lemma bisim_mate {G H} {p} {n} (B : InvertibleBisim G H) s s' :
   bisim G H B s s' -> mate p s n -> mate p s' n.
 Proof.
   intros b [w [w_depth w_min]].
@@ -144,7 +191,7 @@ Proof.
     apply w_min.
 Qed.
 
-CoFixpoint bisim_no_worse {G H} {p} (B : Bisim G H) s s'
+CoFixpoint bisim_no_worse {G H} {p} (B : InvertibleBisim G H) s s'
   (b : bisim G H B s s') (n : no_worse p s) : no_worse p s'.
 Proof.
   destruct n.
@@ -168,7 +215,7 @@ Proof.
       * apply n.
 Defined.
 
-CoFixpoint bisim_draw {G H} (B : Bisim G H) s s'
+CoFixpoint bisim_draw {G H} (B : InvertibleBisim G H) s s'
   (b : bisim G H B s s') 
   (d : draw s) : draw s'.
 Proof.