Brute-force composition is associative proof, lambda calc

comp_is_assoc.md

Prelude

T1: B = (\f g x. f (g x))

Goal

(B a (B b c)) = (B (B a b) c)

Proof

LHS: (B a (B b c))
T1: (B a ((\f g x. f (g x)) b c))
Apply: (B a (\x. b (c x)))
Let term1 = (\x. b (c x))
So: (B a term1)
T1: ((\f g x. f (g x)) a term1)
Rename x -> y: ((\f g y. f (g y)) a term1)
Apply: \y. a (term1 y)
Sub term1: \y. a ((\x. b (c x)) y)
Apply: \y. a(b(c y))

RHS: (B (B a b) c)
T1: (B ((\f g x. f (g x)) a b) c)
Apply: (B (\x. a (b x)) c)
Let term2 = (\x. a (b x))
So: (B term2 c)
T1: ((\f g x. f (g x)) term2 c)
Rename x -> y: ((\f g y. f (g y)) term2 c)
Apply: \y. term2 (c y)
Sum term2: \y. (\x. a (b x))) (c y)
Apply: \y. a(b(c y))

LHS = RHS,
QED