#include <iostream>
using namespace std;



//-----------------------------------------------------------------------
// 識別子 (変数名)
//-----------------------------------------------------------------------

typedef int id;



//-----------------------------------------------------------------------
// λ項の定義
//    M ::= x | λx.M | M M
//-----------------------------------------------------------------------

template<id x>               struct var;
template<id x, class M>      struct abst;
template<class M1, class M2> struct appl;



//-----------------------------------------------------------------------
// そのλ項に出現しないFreshな変数名を取得
//-----------------------------------------------------------------------

template<class M> struct newvar;

template<id x> struct newvar< var<x> >
{
	static const int val = x+1;
};
template<id x, class M> struct newvar< abst<x,M> >
{
	static const int v1 = x+1;
	static const int v2 = newvar<M>::val;
	static const int val = (v1 < v2 ? v2 : v1);
};
template<class M1, class M2> struct newvar< appl<M1,M2> >
{
	static const int v1 = newvar<M1>::val;
	static const int v2 = newvar<M2>::val;
	static const int val = (v1 < v2 ? v2 : v1);
};




//-----------------------------------------------------------------------
// 代入の定義
//   [N/x]x       = N
//   [N/x]y       = y
//   [N/x]λx.M   = M
//   [N/x]λy.M   = λz.[N/x][z/y]M  (z is not in N)
//   [N/x](M1 M2) = [N/x]M1 [N/x]M2
//-----------------------------------------------------------------------

template<class N, id x, class M> struct substitute;

template<class N, id x> struct substitute< N, x, var<x> >
{
	typedef N term;
};
template<class N, id x, id y> struct substitute< N, x, var<y> >
{
	typedef var<y> term;
};
template<class N, id x, class M> struct substitute< N, x, abst<x,M> >
{
	typedef abst<x,M> term;
};
template<class N, id x, id y, class M> struct substitute< N, x, abst<y,M> >
{
	static const int z = newvar< appl<N,M> >::val;
	typedef abst<z, typename substitute< N, x,
		typename substitute<var<z>,y,M>::term >::term > term;
};
template<class N, id x, class M1, class M2> struct substitute< N, x, appl<M1,M2> >
{
	typedef appl< typename substitute<N,x,M1>::term, typename substitute<N,x,M2>::term > term;
};




//-----------------------------------------------------------------------
// β-reduction
//    β(x)         -> x
//    β(λx.M)     -> λx.β(M)
//    β(x M2)      -> x β(M2)
//    β(λx.M1 M2) -> β([M2/x] M1)
//    β(M1 M2)     -> β(β(M1) M2)    if M1 !=β(M1)
//    β(M1 M2)     -> M1 β(M2)        otherwise
//-----------------------------------------------------------------------

template<class M> struct reduct;

template<id x> struct reduct< var<x> >
{
	typedef var<x> term;
};
template<id x, class M> struct reduct< abst<x,M> >
{
	typedef abst< x, typename reduct<M>::term > term;
};
template<id x, class M2> struct reduct< appl<var<x>,M2> >
{
	typedef appl< var<x>, typename reduct<M2>::term > term;
};
template<id x, class M1, class M2> struct reduct< appl<abst<x,M1>,M2> >
{
	typedef typename reduct< typename substitute<M2,x,M1>::term >::term term;
};
	// helper begin
	template<class A, class B> struct is_ { enum{same=false}; };
	template<class A> struct is_<A,A> { enum{same=true}; };
	template<bool b, class M1, class rM1, class M2> struct red_helper {
		typedef appl<M1, typename reduct<M2>::term> term;
	};
	template<class M1, class rM1, class M2> struct red_helper<false,M1,rM1,M2> {
		typedef typename reduct< appl<rM1, M2> >::term term;
	};
	// helper_end
template<class M1, class M2> struct reduct< appl<M1,M2> >
{
	typedef typename reduct<M1>::term rM1;
	typedef typename red_helper< is_<M1,rM1>::same, M1, rM1, M2 >::term term;
};





//-----------------------------------------------------------------------
// できるだけ小さいidになるように変数名のつけかえ (Debug用）
//-----------------------------------------------------------------------

template<id base, class M> struct shorterid;
template<id base, id x> struct shorterid< base, var<x> >
{
	typedef var<base-x> term;
};
template<id base, id x, class M> struct shorterid< base, abst<x,M> >
{
	typedef abst<base-x, typename shorterid<base,M>::term> term;
};
template<id base, class M1, class M2> struct shorterid< base, appl<M1,M2> >
{
	typedef appl<typename shorterid<base,M1>::term, typename shorterid<base,M2>::term> term;
};

//-----------------------------------------------------------------------
// 出力 (Debug用）
//-----------------------------------------------------------------------

template<class M> struct print_impl;
template<class M> struct print
{
	static ostream& to( ostream& os )
	{
		print_impl< typename shorterid<newvar<M>::val-1, M>::term >::to( os );
		return os;
	};
};
template<id x> struct print_impl< var<x> > {
	static void to( ostream& os ) {
		if( x == 0 )
			os << 'a';
		else
			for(int xx=x; xx>0; xx/=26)
				os << char('a' + (xx % 26));
	}
};
template<id x, class M> struct print_impl< abst<x,M> > {
	static void to( ostream& os ) {
		os << 'L';
		print_impl< var<x> >::to( os );
		os << '.';
		print_impl< M >::to( os );
	}
};
template<class M1, class M2> struct print_impl< appl<M1, M2> > {
	static void to( ostream& os ) {
		os << '(';
		print_impl<M1>::to( os );
		os << ' ';
		print_impl<M2>::to( os );
		os << ')';
	}
};





//-----------------------------------------------------------------------
// test
//-----------------------------------------------------------------------

int main()
{
	#define DO_PRINT  print< reduct<
	#define END_PRINT >::term >::to(cout) << endl;

	enum{a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z};

	typedef abst<s, abst<z, var<z> > > zero;
	typedef abst<s, abst<z, appl<var<s>,var<z> > > > one;
	typedef abst<s, abst<z, appl<var<s>, appl<var<s>,var<z> > > > > two;
	typedef abst<s, abst<z, appl<var<s>, appl<var<s>, appl<var<s>,var<z> > > > > > three;
	typedef abst<s, abst<z, appl<var<s>, appl<var<s>, appl<var<s>, appl<var<s>,var<z> > > > > > > four;

	// 足し算
	typedef abst<m, abst<n, abst<s, abst<z,
		appl< appl<var<m>,var<s> >, appl< appl<var<n>,var<s> >,var<z> > >
	> > > > add;

	// 掛け算
	typedef abst<m, abst<n, abst<s,
		appl< var<m>, appl< var<n>,var<s> > >
	> > > mult;

	// １引く
	typedef abst<n, abst<s, abst<z,
		appl< appl< appl<var<n>,
			abst<g, abst<h, appl<var<h>, appl<var<g>,var<s> > > > >
		>, abst< d, var<z> > >, abst< i,var<i> > >
	> > > pred;

	// 引き算
	typedef abst<m, abst<n,
		appl< appl< var<n>, pred >, var<m> >
	> > sub;


	DO_PRINT
		appl<appl<mult, three>, two>
	END_PRINT

	DO_PRINT
		appl<appl<sub, two>, two>
	END_PRINT
}