I'm not sure if your idea will work, but have some notation to help you avoid mixing the levels. Here's how you say "try to prove this fact conditional on some other fact":

function main()
{
if (proves(outputs(1), n1))
return 1;
else if (proves("implies(!proves(outputs(1), n1), eval(outputs(2)))", n2))
return 2;
else
return 0;
}