Well-founded subterm relation on trees

Consider a type of binary trees where the nodes are labeled with an arbitrary type A:Set and define the relation "t is the left or right subtree of t'" Show that this relation is well-founded (Please give two different proofs.)

Solution

Follow this link





Yves Bertot
Last modified: Sun May 3 13:52:38 CEST 2015