Lemma 1: There's a proof that M'(DefectBot)=D, and that there does not exist a shorter proof of M'(DefectBot)=C.

Proof: There's a short proof that DefectBot(DefectBot)=D, and a proof of length (waiting time + short) that FB'(DefectBot)=DefectBot(FB')=D. (It needs to wait until FB' stops looking for only cooperative proofs.) Clearly there are no shorter proofs of contrary statements.

So there's a proof that M' skips to its default defection (since there's nothing strictly better), and this proof has length less than (g(short) + g(wait + short) + short), where g is the function that bounds how long it takes to verify that something is the shortest proof of a certain type, in terms of the proof length. (I think g is just bounded by an exponential, but it doesn't matter).

Thus, of course, Lemma 1 has a proof of length at most g(g(short) + g(wait + short) + short).

Lemma 2: There's a proof that M'(FB')=FB'(M')=C, and that there does not exist a shorter proof of any alternative outcome.

Proof: Similar to Lemma 1. The initial proofs are a bit longer because we need the Löbian proof of length less than (waiting time) that FB'(FB')=C, instead of the short proof that DefectBot(DefectBot)=D.

And so there's a proof of length (g(wait+short) + g(wait) + short) that M' goes to the sanity-check trying to prove that FB'(M')=FB'(FB'). Now a proof of length L that FB'(M')=C would imply a proof of length L + (g(wait+short) + g(wait) + 2*short) that M'(FB')=C...

Oh, and here's the impasse again, because the existence of a proof that M'(FB')=C is no longer enough to prove that FB'(M')=C, you also need that there's no shorter proof that M'(FB')=D. Unless there's a clever way to finesse that (within something provable by the same system), it looks like that's where this last-ditch fix fails.

Drat.