Start by fixing *Phi* and *w*, and assuming the hypotheses
of the rule.

Since **check** works by structural recursion on *t*, let's
do induction on *t*.

In fact, if I was feeling extra moral, I'd say let's do *recursion
induction* on **check**, effectively using elimination wrt the
implementation to justify elimination wrt the specification. Of
course, recursion induction on check is just structural recursion
on *t* wrapped up and specifically labelled as `the induction
which allows one step of computation'. This is good design, as it
removes the apparent coincidence by which induction on the data
seems to work.

Next: induction on *t* |
Prev: **check**'s elim rule |
Up: contents

Conor's Work Page