Conclusion
à We need a normal form,
s.t an MTT in normal form which
is not finite copying, is also not
MSO definable!
Given an MTT, how can we decide whether or not
its translation is MSO definable??
END of FOURTH DAY!