take P = (Start-At (0,S)) +* (0 .--> (halt S)); :: thesis: P is halting
thus P is halting by Th10; :: thesis: verum