Basic defining clauses (2 versions)

up | previous | next | detailed contents | brief contents

Basic defining clauses (2 versions)

The basic defining conditions for setof can be expressed in two alternate, equivalent ways:

setof f pair(x,y) = p1 iff f x = y, otherwise setof f pair(x,y) = p2.
setof f z = p1 iff p2 z = f (p1 z), otherwise setof f z = p2.

As one would expect, once the first pair of clauses is proved, the second pair, being a simple reformulation of the first, have very short proofs.

Defining clauses for setof using pair

Defining clauses for setof using p1 and p2.

up | previous | next | detailed contents | brief contents