Forced fourth terms over $(0,1,-1)$ and $P^*=(0,1,-1,-5)$

Tree orders: for a tree witness $\theta(k,r)\in\{0,1\}$ and distinct integers $x,y$ with $k=\nu_2(y-x)$, $x\prec_\theta y$ iff $\mathrm{bit}_k(x)=\theta(k,\,x\bmod 2^k)$. A finite word $Q$ is $\theta$-safe if "$Q$ in order, then all other integers in $\prec_\theta$-order" has no monotone $4$-term arithmetic progression; it is tree-safe if it is $\theta$-safe for some $\theta$. An in-order pair $a$ before $b$ in $Q$ is open if $2b-a,3b-2a\notin Q$. Let $P^*=(0,1,-1,-5)$. If $Q$ is $\theta$-safe then: (a) if $Q$ begins $(0,1,-1)$ and $-3\in Q$, then $-5\in Q$ and $-5$ precedes $-3$; (b) if $Q$ begins $P^*$ and $2\in Q$, then $3\in Q$ and $3$ precedes $2$.

Formalization note: treeLt is from Definitions.Def_Erdos195_tree; Safe, bitOne from Definitions.Def_Erdos195_defs; positions are List.idxOf, $\nu_2$ is padicValInt 2, L <+: Q means $L$ is a prefix of $Q$.