Documentation

Strict order between expressions as defined in TRAAT p103.

s > t iff |s| > |t| and , for all x in V, |s|_x > |t|_x

This is perhaps the simplest order that can be used with KBC.

Strict order between expressions loosely as defined in TRAAT p124 (KBO)

Reversed K >| for Knuth, sorry Bendix.

Dershowitz reduction order as defined in TRAAT

|> a D for Dershowitz

This is not a simplification order on funny Exprs.

Weight function for kboBy:

• Variables weigh 1
• Nullary functions weigh 1 (a.k.a. constants)
• N-ary functions weigh 0
• Unary functions weigh 1

This is the weight when using >|.

Weight function for kboBy:

• Variables weigh 1
• Nullary functions weigh 1 (a.k.a. constants)
• N-ary functions weigh 0
• Unary functions weigh 1 except for the one given as argument

To be used alongside weightExcept

Returns True when an Expression has either a functional type or functional variables.

funny xx        =  False
funny one       =  False
funny idE       =  True
funny (ff one)  =  True

Returns True when an Expression has no functional return type and no functional variables.

serious xx        =  True
serious one       =  True
serious idE       =  False
serious (ff one)  =  False