A quasiorder is a symmetrical reflexive relation. is a well quasi order (WQO) if in addition for every sequence from X there is i < j s.t. . WQOs are important in proving termination. If X is WQO the power set of X is not always WQO by the Egli-Milner ordering. The class of Better Quasi-orders is a class of WQOs designed to be closed under this operation. It turns out that the class of BQOs can be given a coinductive definition which is equivalent to the usual combinatorial definition.
As a result, one can give smooth proofs of results whose standard combinatorial proofs are ...not for fainthearts.
LS Home page or Talks in 1998/99
This abstract was produced with the help of
LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)
Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.