Thm* i:{8...}. m,n:. 3m+5n = i

This is usually posed as an argument that a postage of any amount of 8 cents or over can be composed of 3- and 5-cent stamps.

We use induction up from 8.

For 8 = i, a value of 1 for both m and n suffices.

Now, for 8<i, we show m,n:. 3m+5n = i assuming

3m+5n = i-1, for some m and n.

Show m,n:. 3m+5n = i.

If n = 0 then take away three 3-cent stamps and add two 5-cent stamps, i.e., use m-3 and n+2 to instantiate the goal quantifiers; this is possible because m3.

If n = 0   then take away one 5-cent stamp and add two 3-cent stamps, i.e., use m+2 and n-1 to instantiate the goal.

QED

Why 8 cents?

Because Thm* (m,n:. 3m+5n = 7).
And this is because 3m+5n = 7  m  3 & n  2, and each case of m and n over this range contradicts 3m+5n = 7.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html