Thm*  (ABC) ~ ((AB)C)

We give a little more detail in this proof than usual, since it's a short proof and paradigmatic of many little proofs heavy on trivial computation.

The idea, as with many of our proofs of "<type> ~ <type>" is to explicitly give the two expressions for inverse functions, and use calculation directly to show they are inverses.

In this case we map <a,b,c>  ABC to <<a,b>,c>  (AB)C (and vice-versa).

We show the expressions gotten by expanding

Def  InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)

then instantiating the arguments with the appopriate nested pairs and compute down.

Here's one reduction step-by-step; watch <a1,a3,a4> get passed to a destructor, then get broken down and rebuilt as <<a1,a3>,a4>, and then again broken down and rebuilt back into <a1,a3,a4>.

(xyz.xyz/xy,z. xy/x,y. <x,y,z>)
((abc.abc/a,bc. bc/b,c. <<a,b>,c>)(<a1,a3,a4>)) look
*
(abc.abc/a,bc. bc/b,c. <<a,b>,c>)(<a1,a3,a4>)/xy,z. xy/x,y. <x,y,z>
*
(<a1,a3,a4>/a,bc. bc/b,c. <<a,b>,c>)/xy,z. xy/x,y. <x,y,z>
*
(<a3,a4>/b,c. <<a1,b>,c>)/xy,z. xy/x,y. <x,y,z>
*
<<a1,a3>,a4>/xy,z. xy/x,y. <x,y,z> look
*
<a1,a3>/x,y. <x,y,a4>
*
<a1,a3,a4> look

Also see the amusing proof of Thm*  a,b,c:. a(bc) = (ab)c from this theorem.

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