Princeton University
Computer Science Dept.

Computer Science 496
Automated Theorem Proving

Andrew W. Appel

Spring 2001
Assignment 5
Prove the Recursion Theorem on page 16 of Nathan Jacobson's Basic Algebra I (W. H. Freeman and Company, 1974). You can find the statement of the theorem and lots of useful supporting lemmas in as5.tar (which has more files than the proving.tar of previous assignments).

For easy reference, here is a statement of the theorem in our logic.

Suggested method: Start by proving these lemmas
.

Bug reports

The map predicate given originally is incorrect; it didn't require that f map every element of the domain. Here is the (almost) correct one: 
map: tm (rel3 (per T) (per U) (rel T U)) =
  lam3 [eqt][equ][f]
   (forall4 [x][x'][y][y']
      eqt @ x @ x' imp f @ x @ y imp f @ x' @ y' imp equ @ y @ y')
   and (forall [x] eqt @ x @ x imp exists [y] f @ x @ y).

Another bug report

The map predicate above is still not right; it didn't require that f fully respect the equivalence relations. Here is the (probably) correct one: 
map: tm (rel3 (per T) (per U) (rel T U)) =
  lam3 [eqt][equ][f]
   (forall4 [x][x'][y][y']
      eqt @ x @ x' imp f @ x @ y imp f @ x' @ y' imp equ @ y @ y')
   and (forall4 [x][x'][y][y']
         eqt @ x @ x' imp equ @ y @ y' imp
           (f @ x @ y equiv f @ x' @ y'))
   and (forall [x] eqt @ x @ x imp exists [y] f @ x @ y).