Added proof of prop 5.2 (h-initial iff recursive)
Further experiments