⌈m⌉ * ⌈n⌉ ≡ λf x.⌈m⌉ (⌈n⌉ f) x | ; def * |
≡ λf x.(λg x.gm x) (⌈n⌉ f) x | ; def ⌈m⌉ |
= λf x.(λx.(⌈n⌉ f)m x) x | ; →β |
= λf x.(λy.(⌈n⌉ f)m y) x | ; →α |
= λf x.((⌈n⌉ f)m x) | ; →β |
= λf x.(((λh x.hn x) f)m x) | ; def ⌈n⌉ |
= λf x.(λx.fn x)m x | ; →β |
= λf x.(fn)m x | ; →β |
= λf x.fnm x | ; def композиции |