Rules of lambda epsilon calculus
Here are the rules of this calculus:
(beta *) for any fresh variable ,
(R1) (Reidemeister one) if then
(R2) (Reidemeister two) if then
(ext1) (extensionality one) if then
(ext2) (extensionality two) if then
These are taken together with usual substitution and -conversion.
The relation between the operations from calculus and emergent algebras is illustrated in the next figure.