diff --git a/examples/top-down-tree-automaton b/examples/top-down-tree-automaton
new file mode 100644
index 0000000000000000000000000000000000000000..4fbbdc8c56c5dae54e422371831bb2e8afbc3f40
--- /dev/null
+++ b/examples/top-down-tree-automaton
@@ -0,0 +1,25 @@
+# This is an example from [1], used to distinguish the expressivity of
+# deterministic and non-deterministic top down tree automata.
+#
+# The automaton below accepts the tree language
+#
+#   T = { f(a, b), f(b, a) }
+#
+# with symbols a/0, b/0 and f/2. A deterministic top-down automaton would not
+# accept that language. See [1, Proposition 1.6.2].
+
+{init, non_init} x Ƥ({a,b} + {f}×X×X)
+
+
+q_i: (init,     { inj1 (f, q_a, q_b), inj1 (f, q_b, q_a) })
+
+q_a: (non_init, { inj0 a })
+q_b: (non_init, { inj0 b })
+
+
+
+# [1]: Comon, Hubert; Dauchet, Max; Gilleron, Rémi; Jacquemard, Florent;
+#      Lugiez, Denis; Löding, Christof; Tison, Sophie; Tommasi, Marc
+#      (November 2008).
+#      Tree Automata Techniques and Applications.
+#      Retrieved 2019-03-15.
diff --git a/examples/top-down-tree-automaton.out b/examples/top-down-tree-automaton.out
new file mode 100644
index 0000000000000000000000000000000000000000..601bca154318c580fb2c0e2304cf3ecb70c45dcc
--- /dev/null
+++ b/examples/top-down-tree-automaton.out
@@ -0,0 +1,3 @@
+Block 0: q_i
+Block 1: q_a
+Block 2: q_b