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