[FOM] Gentzen's consistency proof

[Timothy Y. Chow]

I'm trying to understand Gentzen's consistency proof of PA.  There is 
something that I think follows as a corollary of the proof but I'm 
wondering if I'm missing something.

Suppose I write down explicitly a Turing machine M that represents 
epsilon_0.  That is, M takes a pair of natural numbers (a,b) as input and 
outputs either 0 or 1, and I can prove (using ZF or whatever) that if I 
interpret an output of 1 as "a < b" then I get a total ordering on the 
natural numbers that is order isomorphic to epsilon_0.

Does Gentzen's proof give an effective procedure for taking a PA-proof of 
0=1 and producing a Turing machine M' that outputs an infinite sequence of 
natural numbers a_1, a_2, a_3, ... such that a_i > a_{i+1} for all i, 
where ">" denotes the aforementioned epsilon_0 ordering computed by M?

I think that the answer is yes but I'm a little concerned that 
ineffectivity might creep in somewhere.

Tim