On Lazy Commutation

Abstract. We investigate combinatorial commutation properties for reordering a sequence of two kinds of steps, and for separating wellfoundedness of unions of relations. To that end, we develop the notion of a constricting sequence. These results can be applied, for example, to generic path orderings used in termination proofs. “Loop” as a train destination means that the train enters the Loop elevated structure in downtown Chicago, does a complete circle, and then returns the way it came. Red Line and Blue Line trains serve the Loop area of Chicago. . . . – Paul Inast (wikipedia.org)

• Type: Conference
• Year: 2009
• Where: BIRTHDAY
• Authors: Nachum Dershowitz
• Keywords: Applied Computing, BIRTHDAY 2009, Combinatorial Commutation Properties, Generic Path Orderings, Loop Elevated Structure