Proof of correctness of addition and multiplication of Church numerals in Agda - #1

Open

timjb wants to merge 8 commits into

pi8027:masterfrom

Commits on May 26, 2013

formalize closed terms in Agda
timjb
committed
d32b553
prove correctness of addition of church numerals
timjb
committed
56a4a66
use new module for reasoning about beta-reduction in agda
timjb
committed
61378d7
simplify proof of church addition by using special reduction rule for closed terms
timjb
committed
8f6201d
rename constructors for Closed′
timjb
committed
8c6e1e0
simplified proof of church addition using congruence construction
timjb
committed
0cb7f7c
prove correctness of multiplication of church numerals
timjb
committed
48c03f5
small cleanup
timjb
committed
c960bd2