Hofstadter's TQ

This is a quick follow up from Hofstadter's MIU and Hofstadter's PQ.

Here is Hofstadter's TQ system in metamath: