Show that the string $( [ ) ]$ is not in a Dyck language

I think I understand why the string $( [ ) ]$ is not in a Dyck language.

In my words,

D2* is all the dyck words of 2 parentheses.

From the definiton of $D2*$, every words must have exactly 2 pairs correctly nested pairs of parentheses.

All the words of the language are given by

$\sum = { (1, )1, (2, )2 } $

The alphabet consisting of 2 kinds of left and right parentheses.

The language is given by the following grammar :

-
Terminal set is $\sum$

-
Start variable is not in terminal set

-
$ S -> \big( \epsilon | SS | (i S )i \big)$ for all i > 1

But the form of that word is $(i (j )i )j$ which fails to match the definition.

But I'm having trouble writing a formal proof on that.

Consider producing a leftmost derivation of ( [ ) ]. We can begin with
$$
S\Rightarrow SS\stackrel{*}{\Rightarrow}SS\dotsc S
$$
and to get the ( on the left we must eventually use the production $S\rightarrow(S)$ on the leftmost $S$, giving
$$
S\stackrel{*}{\Rightarrow}(S)S\dotsc S
$$
and then we'll have
$$
S\stackrel{*}{\Rightarrow}(SS\dotsc S)S\dotsc S
$$
and to get the [ as the second terminal on the left we must eventually use the production $S\rightarrow[S]$, giving
$$
S\stackrel{}{\Rightarrow}([S]SS\dotsc S)S\dotsc S\stackrel{}{\Rightarrow}([SS\dotsc S]SS\dotsc S)S\dotsc S
$$
and now we're stuck, since no production will give us the ) terminal we need on the left without introducing a ( first.

For a slightly different take, consider that $S$ can only derive strings in $D_2$, so to derive ( ] ) ] we must use the production $S\rightarrow (S)$, where the $S$ in the right term of the production must also derive a string in $D_2$, but that would imply $S$ derives ], which cannot be, since $]\notin D_2$.

StackExchange Computer Science Q#32334, answer score: 3