Re: A new proof of the wellfoundednes of the multiset ordering
Didn't Steve Simpson do a bunch of proofs of orderings like this one?
And I thought that even he referenced Diana Schmidt (though perhaps I
have the name wrong) from Heidelberg?
TN> Attached you find a new(?) proof of the wellfoundednes of the
TN> multiset ordering due to Wilfried Buchholz. Salient features:
TN> - it is completely inductive and does not involve classical
TN> reasoning (in contrast to the proof by Dershowitz and Manna);
TN> - it is a joy for theorem provers (it takes about 40 lines in
TN> I would be interested to hear if this proof is known in the