, where angle-brackets denote a pair
# G = [p][q][r]
#
# Ma Ma =
# -> G a Note switch to reduction from equality.
# -> G G a a 2nd G gets used for [z] pair
# -> 2nd G becomes [p] in 1st G, a as [p] and [r]
# -> When F selects list a, then element a of list a
# Prove combinators have normal form
Ma = reduce Ma
Mb = reduce Mb
Mc = reduce Mc
Md = reduce Md
# Prove combinators distinct
Ma = Mb
Ma = Mc
Ma = Md
Mb = Mc
Mb = Md
Mc = Md
# Prove identity property
reduce Ma Ma = Ma
reduce Mb Mb = Ma
reduce Mc Mc = Ma
reduce Md Md = Ma
# Prove associative property
reduce Ma Mb = reduce Mb Ma
reduce Ma Mc = reduce Mc Ma
reduce Ma Md = reduce Md Ma
reduce Mb Mc = reduce Mc Mb
reduce Mb Md = reduce Md Mb
reduce Mc Md = reduce Md Mc
# Prove the distinctness of products
reduce Ma Mb = Mb
reduce Ma Mc = Mc
reduce Ma Md = Md
reduce Mb Ma = Mb
reduce Mb Mc = Md
reduce Mb Md = Mc
reduce Mc Ma = Mc
reduce Mc Mb = Md
reduce Mc Md = Mb
reduce Md Ma = Md
reduce Md Mb = Mc
reduce Md Mc = Mb