For the thumb branch instruction (b), arm-none-eabi-gcc uses both T1 and T2 encodings, it is legal?

Hello,

    I just found arm-gcc uses both two thumb encodings, see the following example

```C

int x = 100, y = 60;

if (x - 30 > y + 11) {
x = 0xefff;
}
else {
y = 0xdffff;
}

/*  arm-none-eabi-gcc -c -O0 -mcpu=cortex-m4 -march=armv7e-m -mthumb armtest.c && arm-none-eabi-objdump -D armtest.o >> armbin.txt

18: 429a cmp r2, r3
1a: dd03 ble.n 24 <main+0x24>
1c: f64e 73ff movw r3, #61439 ; 0xefff
20: 607b str r3, [r7, #4]
22: e001 b.n 28 <main+0x28>

*/

```

But the architecture manual mentioned that `` As a result, encodings T1 and T2 are never both available to the assembler, nor are
encodings T3 and T4.``, see [ARM DDI 0406C.d ID040418 (A8-333)](https://developer.arm.com/documentation/ddi0406/cd)

So, is it ok?