Better-Quasi-Orderings and Coinduction

Thomas Forster


A quasi-order is a reflexive transitive relation.  Well-quasi-orderings
are quasiorderings whos strict part is wellfounded and has no infinite
antichains.   Better-quasi-orderings are a specially, well, *better*
kind of WQO usually characterised by a complicated combinatorial formulation
but which can nvertheless be economically described in an algebraic way:
viz, coinductively.