You can reduce a proof by finding the term that corresponds to it, finding a term \alpha equivalent to that term, and then reconstructing a proof from the equivalent term.

A proof is a candidate for reduction whenever an implication is introduced and then immediately used as either premise of a use of \rightarrowE

Reducing a proof will never change its conclusion.

You can reduce a proof by finding the term that corresponds to it, \beta reducing the term, and then reconstructing a proof from the reduced term.

Reducing a proof will never change its open assumptions.

an application in the term means a step of \rightarrowE in the proof

a lambda abstraction in the term means a step of \rightarrowE in the proof

a lambda abstraction in the term means a step of \rightarrowI in the proof

a variable in the term means an assumption in the proof, free if the assumption is open and bound if the assumption is discharged

a variable in the term means an assumption in the proof, free if the

assumption is discharged and bound if the assumption is open

an application in the term means a step of \rightarrowI in the proof

23

The function that takes a number and spells out its name in text, so for example would take 23 to "twenty-three".

The function that takes a string of text and returns the number of characters it contains, so for example would take "Hatshepsut" to 10.

The function that takes a string of text and reverses it, so for example would take "Hatshepsut" to "tuspehstaH".

"Hatshepsut"

z (\lambda w . y)

z (\lambda z. y)

\lambda y . y ((\lambda w . y) z)

z (\lambda w . z)

\lambda y . x z

(\lambda z . z)\lambda w . x z

(\lambda y . y)\lambda z . x z

\lambda x . x \lambda y . x z