#include <bits/stdc++.h>
#include <variant>

const bool DO_EVAL = 1;

typedef std::variant<int, bool> body_type;
typedef std::variant<std::function<void(body_type&)>, std::function<void(body_type&, body_type&)>> eval_func;

const char LAMBDA = '@';
const char SPACE = ' ';
const char OPEN = '(';
const char CLOSE = ')';
const char DOT = '.';
const char COMMA = ',';
const char COLON = ':';

const char AT = '&';
const char LT = '$'; // LT

const int OUT_INDENT = 4;

const int PARENT = -1;
const int VALUE = 0;
const int ABST = 1;
const int APPLY = 2;
const int TYPE = 3;
const int TARGET = 4;
const int FUNC = 5; // 他で明示的に指定されてるもの
const int PAIR = 6;
const int ACCESS = 7;
const int LET = 8;

const std::string BOOL = "B";
const std::string TRUE = "true";
const std::string FALSE = "false";

const int BOOL_INT = 0;
const int NAT_INT = 1;
const int PAIR_INT = 2; // pairを基底型とした場合
const int VARIABLE_INT = -1; // 変数

const std::string NAT = "N";

const int MAX = 1e9+7;

std::string input;

/*

   生成が先で展開が後になるような書き方をするべき(?)

   (lx.ly.y) b cの場合、まずは括弧で囲われた部分の子ノードを生成する
   次にbを生成して、その次に空白がある事を確認したらbとcを合体させたノードを生成する

	Childが両方埋まっていて空白がある -> child[0]を生成する

	簡約について
	applyのchildが abst + funcの形になっている場合に簡約できそう

	(@x:B.@y:B x y) true false
	(@y:B true y) false


	型検査の実装をしないといけない
	apply ->
		abst ->
			value(対象の変数)
			value(type)
			expr(関数)
		value(適用する関数)
	
		typeの型が適用する関数の型と一致している必要がある

	letの文法について
	"$val" と名前を置く
	束縛の示す先をそのまま括弧で括って
	$v(@x:N.(5 x))
	のように宣言する事ができる
	"v 3" で8が出力される

*/

auto type_value_to_str = [](int val){

	if(val == BOOL_INT)
		return "bool";
	if(val == NAT_INT)
		return "nat";
	if(val == PAIR_INT)
		return "pair";
	if(val == VARIABLE_INT)
		return "variable";

	return "not match";
};

auto type_to_str = [](int val){
	if(val == VALUE)
		return "value";
	else if(val == PARENT)
		return "parent";
	else if(val == ABST)
		return "abst";
	else if(val == APPLY)
		return "apply";
	else if(val == TYPE)
		return "type";
	else if(val == TARGET)
		return  "target";
	else if(val == PAIR)
		return  "pair";
	else if(val == ACCESS)
		return  "access";
	else if(val == LET)
		return  "let";
	else if(val == FUNC)
		return  "func";
	return "err";
};

auto is_nat = [](std::string& inp, int st, int en){
	// 先頭のマイナスは許容
	if(inp.at(st) == '-')
		++st;
	for(int index = st; index < en; ++index)
		if(!('0' <= inp.at(index) && inp.at(index) <= '9'))
			return false;
	return true;
};

auto is_val = [](std::string& inp, int st, int en){

	for(int index = st; index < en; ++index)
		if(!(('a' <= inp.at(index) && inp.at(index) <= 'z') ||
		   ('A' <= inp.at(index) && inp.at(index) <= 'Z')))
			return false;
	return true;
};

// inp[st,en)("type": value)がどのような型(bool, nat等)を取っているか
auto check_type = [](std::string& inp, int st, int en){
	std::string subst = inp.substr(st, en - st);
	if(subst == FALSE || subst == TRUE)
		return BOOL_INT;
	else if(is_nat(inp, st, en))
		return NAT_INT;
	else if(is_val(inp, st, en))
		return VARIABLE_INT;

	// matchしない場合
	return MAX;
};

auto match_type = [](std::string& inp, int st, int en){
	std::string subst = inp.substr(st, en - st);
	if(subst == BOOL)
		return BOOL_INT;
	if(subst == NAT)
		return NAT_INT;
	return MAX;
};

auto match = [](std::string& inp, int st, int en, char pattern, bool foward = true){
	if(foward)
		for(int index = st; index < en; ++index){
			if(inp.at(index) == pattern)
				return index;
		}
	else
		for(int index = en - 1; index >= st; --index)
			if(inp.at(index) == pattern)
				return index;

	return MAX;
};

auto match_nest = [](std::string& inp, int st, int en, char pattern){
	int nest = 0;
	for(int index = st; index < en; ++index){
		if(inp.at(index) == OPEN)
			++nest;
		else if(inp.at(index) == CLOSE)
			--nest;
		else if(!nest && inp.at(index) == pattern)
			return index;
		if(nest < 0)
			return -1;
	}
	return MAX;
};

// ここにプリミティブな何かを書いていく
/*
	演算子を実装したい
	add 15 20 -> 35 みたいな処理ができたら嬉しい
	内部ではadd = @x.(@y.(x + y)) って事になる

	とりあえずsuccのみ実装
	apply ->
		succ
		expr
	
	の形になる事は保証されている

	加算の演算ができた

	pairを型検査ができる段階に持っていきたい
	そうすれば四則演算が "* (a,b)" の形で表現できる

	pair(や配列)のアクセスに対して特例処置として演算子"$"を生成して、それでどうにかする

	pairを引数に取る関数の実装について
	pairの中身の型を把握する必要がある
	pairの各要素に対する参照を持つ必要がある

*/


struct Primitive{
	std::string name;
	int id, arg_type, ret_type;
	int first, second;
	eval_func func;
	Primitive(std::string name, int id, int arg_type, int ret_type, eval_func func, int first = MAX, int second = MAX) : 
		name(name),
		id(id),
		arg_type(arg_type),
		ret_type(ret_type),
		func(func),
		first(first),
		second(second)
	{
	}
};

std::vector<Primitive> prims;

void init(){

	std::function<void(body_type&)> succ = [](body_type& inp){
		++std::get<int>(inp);
	};
	prims.emplace_back("succ", 1, NAT_INT, NAT_INT, succ);

	std::function<void(body_type&)> pred = [](body_type& inp){
		--std::get<int>(inp);
	};
	prims.emplace_back("pred", 1, NAT_INT, NAT_INT, pred);

	std::function<void(body_type&)> any = [](body_type& inp){
		inp = static_cast<bool>(std::get<int>(inp) != 0);
	};
	prims.emplace_back("any", 1, NAT_INT, BOOL_INT, any);

	std::function<void(body_type&)> not_ = [](body_type& inp){
		inp = static_cast<bool>(std::get<bool>(inp) == 0);
	};
	prims.emplace_back("not", 1, BOOL_INT, BOOL_INT, not_);

	std::function<void(body_type&)> to_nat = [](body_type& inp){
		inp = static_cast<int>(std::get<bool>(inp));
	};
	prims.emplace_back("to_nat", 1, BOOL_INT, NAT_INT, to_nat);

	// ここにpairを引数に取って加算を定義していく
	std::function<void(body_type&, body_type&)> add = [](body_type& inp1, body_type& inp2){
		std::get<int>(inp1) += std::get<int>(inp2);
	};
	prims.emplace_back("add", 1, PAIR_INT, NAT_INT, add, NAT_INT, NAT_INT);

	std::function<void(body_type&, body_type&)> sub = [](body_type& inp1, body_type& inp2){
		std::get<int>(inp1) -= std::get<int>(inp2);
	};
	prims.emplace_back("sub", 1, PAIR_INT, NAT_INT, sub, NAT_INT, NAT_INT);

	std::function<void(body_type&, body_type&)> mul = [](body_type& inp1, body_type& inp2){
		std::get<int>(inp1) *= std::get<int>(inp2);
	};
	prims.emplace_back("mul", 1, PAIR_INT, NAT_INT, mul, NAT_INT, NAT_INT);

	std::function<void(body_type&, body_type&)> div = [](body_type& inp1, body_type& inp2){
		std::get<int>(inp1) /= std::get<int>(inp2);
	};
	prims.emplace_back("div", 1, PAIR_INT, NAT_INT, div, NAT_INT, NAT_INT);

	std::function<void(body_type&, body_type&)> mod = [](body_type& inp1, body_type& inp2){
		std::get<int>(inp1) %= std::get<int>(inp2);
	};
	prims.emplace_back("mod", 1, PAIR_INT, NAT_INT, mod, NAT_INT, NAT_INT);

}

auto match_func = [](std::string& inp, int st, int en){
	std::string subst = inp.substr(st, en - st);

	for(int index = 0; index < prims.size(); ++index){
		if(subst == prims.at(index).name)
			return index;
	}

	return MAX;

};

class Node{

public:
	Node(std::string& inp, int inp_st = 0, int inp_en = -1, int inp_type = -1) : 
		parent_str(inp)
	{
		// [st,en)の半開区間を持つ
		

		// 親ノードの働きをする
		if(inp_en == -1){
			st = 0;
			en = 0;
			type = PARENT;
			child.emplace_back(std::make_shared<Node>(inp, inp_st, parent_str.length()));

			return ;
		}

		st = inp_st;
		en = inp_en;


		int fn_index = match_func(parent_str, st, en);
		if(fn_index != MAX){
			type = FUNC;
			value_type = prims.at(fn_index).ret_type;
			return ;
		}

		int ch_type = check_type(parent_str, st, en);

		if(ch_type != MAX){
			// 明示的に指定されているなら(targetかtypeなら)
			if(inp_type != -1)
				type = inp_type;
			else{
				type = VALUE;
				value_type = ch_type;
			}
		}

		else
			expand();
	}

	Node(std::string& inp, int inp_st, int inp_en, std::shared_ptr<Node> child_1, std::shared_ptr<Node> child_2) : 
		parent_str(inp)
	{
		if(inp_en == -1)
			inp_en = parent_str.length();


		st = inp_st;
		en = inp_en;


		// 必ず関数適用になる
		type = APPLY;

		// ここで子の展開処理がされる
		child.push_back(child_1);
		child.push_back(child_2);

		// 親の展開処理はしない
	}

	void output(int indent = 0){

		std::string indent_str(indent, ' ');
		std::string out_indent_str(indent + OUT_INDENT, ' ');

		std::string result;


		auto add_text = [&result, &out_indent_str](std::string head, std::string body, bool is_str = true, bool use_comma = true){
			result += out_indent_str + "\"" +  head + "\": " + (is_str ? "\"" : "")  + body + (is_str ? "\"" : "") + (use_comma ? "," : "") + "\n";
		};

		std::string type_str = type_to_str(type);

		std::string value_type_str = type_value_to_str(value_type);

		add_text("body", parent_str.substr(st, en - st));
		add_text("type", type_str);
		if(value_type != MAX)
			add_text("value_type", value_type_str);
		if(access_index != MAX)
			add_text("access_index", std::to_string(access_index));
		add_text("st", std::to_string(st), false);
		add_text("en", std::to_string(en), false, child.size());



	}

	std::string str(){
		return parent_str.substr(st, en - st);
	}
	
	std::string strout(){
		if(type == PARENT)
			return child.at(0)->strout();

		else if(type == APPLY){
			return  child.at(0)->strout() + " " + child.at(1)->strout();
		}
		else if(type == ABST){
			return "@" + child.at(0)->strout() +  ":" + child.at(1)->strout() +  "." + child.at(2)->strout();
		}
		else
			return str();
	}

	std::vector<std::shared_ptr<Node>> child;

	std::string& parent_str;
	int st, en;

	int type;

	int value_type = MAX;
	int access_index = MAX;

	/*
	
	   (@y:B.y) (@y:B.y) v
	-> (@y:B.y) v
	-> v

		parent ->
			apply ->
				abst ->
					value(match)
					value(type)
					value(func)
				expr

		parent ->
			[match->expr]value(func)
		

		abstのchildのうち[0][1]が削除され、[2]のうちの[0]にマッチする部分がvalueに置き換わる
		abstのあったノードは削除されて、そこにはabstのchild[2]が入る

	*/

	// 型検査とラベルつけ
	int check(){

		// apply時にabstの引数として渡される型とvariable_body->typeの型が一致しているか確かめる

		if(type == ABST){
			value_type = match_type(parent_str, child.at(1)->st, child.at(1)->en);
			child.at(2)->setType(child.at(0)->str(), value_type);
			for(auto ch : child)
				ch->check();
			return value_type;
		}

		if(type == APPLY){

			if(child.at(0)->type == FUNC){
				Primitive& prim = prims.at(match_func(parent_str, child.at(0)->st, child.at(0)->en));

				// funcの引数が合っているかどうかの型検査

				int check_1 = child.at(1)->check();
				if(prim.arg_type != check_1)
					typeCheckError(prim.arg_type, check_1);

				if(check_1 == PAIR_INT){
					if(prim.first  != child.at(1)->child.at(0)->check())
						typeCheckError(prim.first, child.at(1)->child.at(0)->type);
					if(prim.second != child.at(1)->child.at(1)->check())
						typeCheckError(prim.second, child.at(1)->child.at(1)->type);
				}

				return value_type = prim.ret_type;
			}

			else if(child.at(0)->type == ACCESS){

				if(child.at(1)->type != PAIR){
					std::cerr << "operator access at not pair function" << std::endl;
					abort();
				}

				int access = child.at(0)->access_index;
				if(access >= child.at(1)->child.size()){
					std::cerr << "out of range at access operator" << std::endl;
					abort();
				}
				value_type = child.at(1)->child.at(access)->check();
				return value_type;
			}

			int check_0 = child.at(0)->check();
			int check_1 = child.at(1)->check();
			if(check_0 != check_1)
				typeCheckError(check_0, check_1);
			return value_type = check_0;
		}
		// if(type == VALUE || type == FUNC)
		if(type == VALUE)
			return value_type;

		// pair自体は基底の型ではない
		if(type == PAIR)
			return PAIR_INT;

		if(type == PARENT)
			for(auto ch : child)
				ch->check();
		return 0;
	}

	void setType(std::string target, int val){
		if(type == VALUE && str() == target && value_type == VARIABLE_INT)
			value_type = val;
		for(auto ch : child)
			ch->setType(target, val);
	}

	bool simplify(){

		bool flag = false;

		for(int index = 0; index < child.size(); ++index){ // 適用 -> 抽象の適用
			if(child.at(index)->type == APPLY && child.at(index)->child.at(0)->type == ABST){
				// index->0->1でtype
				child.at(index)->child.at(0)->child.at(2)->simplification(child.at(index)->child.at(0), child.at(index)->child.at(1));
				child.at(index) = child.at(index)->child.at(0)->child.at(2);

				flag = true;
			}
		}

		for(auto ch : child)
			flag |= ch->simplify();

		return flag;
	}

	// target.child[1]型のtarget.child[0]をexpr.str()で置き換える
	void simplification(std::shared_ptr<Node> target, std::shared_ptr<Node> expr){

		if(type == VALUE && target->child.at(0)->str() == str()){

			st = expr->st;
			en = expr->en;

			child.clear();
			if(check_type(parent_str, st, en) != MAX){
				type = VALUE;
				value_type = match_type(parent_str, target->child.at(1)->st, target->child.at(1)->en);
			}
			else
				expand();
		}
		else
			for(auto ch : child)
				ch->simplification(target, expr);
	}

	// typeにはその文字列の指す意味を代入する
	// varならchildは無し, lambdaなら@以降と.以降の二つ, SPACEなら' '以前とそれ以降の二つ
	
	// lambdaの場合は明示的に指定した方がよさそう(先頭が@で始まるように切る, みたいな感じ)

	// 展開
	void expand(){

		// 関数宣言は必ず先頭にくる
		if(parent_str.at(st) == LT){

			// lambda抽象: @x:N.(x y)
			// let束縛   : $x(y)
			// 束縛はそれが出てきた(それ以降の)ネストをxに置き換える
			// [x->s]f = (@x.f) s
			// [x->y]f = $x(y) f
			// ここの空白は許されないって事にしておきます
			int open_index = match(parent_str, st, en, OPEN);

			int nest = 0;

			for(int index = open_index; index < en; ++index){
				if(parent_str.at(index) == OPEN)
					++nest;
				if(parent_str.at(index) == CLOSE){
					--nest;
					if(!nest){
						// 関数宣言の末尾
						type = LET;
						int pass_space = index;

						while(parent_str.at(pass_space + 1) == SPACE)
							++pass_space;

						child.emplace_back(std::make_shared<Node>(parent_str, st + 1, open_index));
						child.emplace_back(std::make_shared<Node>(parent_str, open_index + 1, index));

						child.emplace_back(std::make_shared<Node>(parent_str, pass_space + 1, en));
						return ;
					}
				}
			}
			parseError("let expr is incorrect");
		}

		if(parent_str.at(st) == LAMBDA){
			int colon_index = match(parent_str, st, en, COLON);
			if(en - 1 <= colon_index || colon_index < st + 2)
				parseError("colon is not found or out of range");

			child.push_back(std::make_shared<Node>(parent_str, st + 1, colon_index, TARGET));

			// ":"と"."の後にある空白は許容

			while(parent_str.at(colon_index + 1) == SPACE)
				++colon_index;

			int dot_index = match(parent_str, colon_index, en, DOT);
			child.push_back(std::make_shared<Node>(parent_str, colon_index + 1, dot_index, TYPE));

			while(parent_str.at(dot_index + 1) == SPACE)
				++dot_index;
			if(en - 1 <= dot_index || dot_index < colon_index + 2)
				parseError("dot is not found or out of range");

			child.push_back(std::make_shared<Node>(parent_str, dot_index + 1, en));

			type = ABST;
			return ;
		}
		else if(parent_str.at(st) == OPEN){
			int nest = 0;
			for(int index = st; index < en - 1; ++index){
				if(parent_str.at(index) == OPEN)
					++nest;
				if(parent_str.at(index) == CLOSE){
					--nest;
					if(!nest)nest = -MAX;
				}
			}

			int close_index = match(parent_str, st, en, CLOSE, false);
			if(nest == 1 && close_index == en - 1){

				++st;
				--en;

				// ここにpairとして組ませる処理を書く
				int comma_index = match_nest(parent_str, st, en, COMMA);

				if(!(comma_index == st || comma_index > en - 2)){

					int first_en = comma_index;

					// 空白の許容
					while(parent_str.at(comma_index + 1) == SPACE)
						++comma_index;

					if(en - (comma_index + 1) > 0){

						type = PAIR;
						// pair自体が返す型は存在しない(pairは基底のものではないため)
						value_type = PAIR_INT;

						child.push_back(std::make_shared<Node>(parent_str, st, first_en));

						child.push_back(std::make_shared<Node>(parent_str, comma_index + 1, en));

						return ;
					}
				}

				// 括弧を除去して再度展開
				expand();
				return ;
			}
		}
		// "$" + natの形式であれば
		else if(parent_str.at(st) == AT && is_nat(parent_str, st + 1, en)){
			type = ACCESS;
			value_type = MAX;
			access_index = std::stoi(parent_str.substr(st + 1, en - (st + 1)));
			return ;
		}


		// 変数(variable)であれば(is_val:typeの形なら)
		int colon_index = match(parent_str, st, en, COLON);
		if(!(colon_index == st || colon_index > en - 2) && is_val(parent_str, st, colon_index) && is_val(parent_str, colon_index + 1, en)){
			type = VALUE;
			value_type = match_type(parent_str, colon_index + 1, en);
			en = colon_index;
			if(value_type == MAX)
				parseError("value type is incorrect");
			return ;
		}

		auto check_child = [&](int pos){
			if(child.size() != 3)
				return ;

			std::shared_ptr<Node> union_child = std::make_shared<Node>(parent_str, st, pos, child.at(0), child.at(1));

			std::shared_ptr<Node> new_child = child.at(2);
			child.clear();
			child.emplace_back(union_child);
			child.emplace_back(new_child);
		};

		std::function<void(int)> split_by_space = [&](int func_st){

			int space_index = match_nest(parent_str, func_st, en, SPACE);

			if(!space_index)
				parseError("space postion is incorrect");

			// not found
			else if(space_index == MAX){
				if(func_st == st)
					parseError("expr cannot split");
				child.push_back(std::make_shared<Node>(parent_str, func_st, en));
				check_child(func_st - 1);
			}

			else{
				// SPACEを区切りに分割
				child.push_back(std::make_shared<Node>(parent_str, func_st, space_index));
				check_child(func_st - 1);
				split_by_space(space_index + 1);
			}
		};

		type = APPLY;

		split_by_space(st);

		if(child.size() != 2)
			parseError("substring is not val and not found");

	}

	void parseError(std::string input_string = ""){
		std::cerr << "parseError : " << input_string << std::endl << "\"" << parent_str <<"\" at [" << st << "," << en << ")  -> ";
		for(int index = st; index < en; ++index)
			std::cerr << parent_str.at(index);
		std::cerr << std::endl;
		abort();
	}

	void typeCheckError(int inp_1, int inp_2){
		std::cerr << "typeCheckError : " << type_value_to_str(inp_1) << " != " << type_value_to_str(inp_2) << std::endl << "\"" << parent_str <<"\" at [" << st << "," << en << ")  -> ";
		for(int index = st; index < en; ++index)
			std::cerr << parent_str.at(index);
		std::cerr << std::endl;
		abort();
	}

};

class EvalNode{
public:
	body_type body;
	int type, value_type, access_index;
	int func_type = MAX;
	std::vector<std::shared_ptr<EvalNode>> child;

	EvalNode(std::shared_ptr<Node> node){
		type = node->type;
		value_type = node->value_type;
		access_index = node->access_index;

		// 評価の終わったnodeなら
		if(type == VALUE){
			if(value_type == NAT_INT){
				try{
					body = std::stoi(node->str());
				}
				catch (std::invalid_argument& e) {
					std::cerr << "EvalNode constructor error : " << "stoi: invalid argument -> " << node->str() << std::endl;
					abort();
				}
			}
			else if(value_type == BOOL_INT)
				body = (node->str() == "true");
		}
		else if(type == FUNC){
			func_type = match_func(node->parent_str, node->st, node->en);
			if(func_type == MAX){
				std::cerr << "func not match\n";
				abort();
			}
		}

		for(auto ch : node->child)
			child.emplace_back(std::make_shared<EvalNode>(ch));
	}

	bool eval(){
		// FUNCの適用が可能ならば
		bool flag = false;

		for(auto ch : child)
			flag |= ch->eval();

		for(int index = 0; index < child.size(); ++index){

			if(child.at(index)->type == APPLY && child.at(index)->child.at(0)->type == FUNC){
				if(child.at(index)->child.at(1)->type == VALUE){

					// ここで処理を行っている
					
					std::get<0>(prims.at(child.at(index)->child.at(0)->func_type).func)(child.at(index)->child.at(1)->body);

					child.at(index)->child.at(1)->value_type = prims.at(child.at(index)->child.at(0)->func_type).ret_type;
					child.at(index) = child.at(index)->child.at(1);

					flag = true;
				}
				else if(child.at(index)->child.at(1)->type == PAIR){

					child.at(index)->child.at(1)->eval();

					std::get<1>(prims.at(child.at(index)->child.at(0)->func_type).func)(child.at(index)->child.at(1)->child.at(0)->body, child.at(index)->child.at(1)->child.at(1)->body);

					child.at(index)->child.at(1)->child.at(0)->value_type = prims.at(child.at(index)->child.at(0)->func_type).ret_type;
					child.at(index) = child.at(index)->child.at(1)->child.at(0);
				}
			}
			else if(child.at(index)->type == APPLY && child.at(index)->child.at(0)->type == VALUE && child.at(index)->child.at(1)->type == VALUE){

				auto& body_0 = child.at(index)->child.at(0)->body;
				auto& body_1 = child.at(index)->child.at(1)->body;
				
				int body_index = body_0.index();
				if(body_index != body_1.index())
					break;
				
				// int
				if(body_index == 0){
					std::get<0>(body_0) += std::get<0>(body_1);
				}
				// bool
				else if(body_index == 1){
					std::get<1>(body_0) &= std::get<1>(body_1);
				}

				child.at(index) = child.at(index)->child.at(0);

				flag = true;
			}
			else if(child.at(index)->type == APPLY && child.at(index)->child.at(0)->type == ACCESS && child.at(index)->child.at(1)->type == PAIR){

				child.at(index) = child.at(index)->child.at(1)->child.at(child.at(index)->child.at(0)->access_index);
				flag = true;
			}
		}

		return flag;
	}

	void out(int indent = 0){
		std::string indent_str(indent, ' ');
		std::string out_indent_str(indent + OUT_INDENT, ' ');
		std::cout << indent_str + "{\n";

		std::cout << out_indent_str + "\"type\" :  " + type_value_to_str(value_type) << std::endl;
		
		std::visit([&out_indent_str](auto val){std::cout << out_indent_str << "\"value\" : " << val << std::endl;}, body);

		
		for(auto ch : child)
			ch->out(indent + OUT_INDENT * 2);
		std::cout << indent_str + "}\n";

	}

	void strout(){
		if(type == PARENT){
			child.at(0)->strout();
			std::cout << std::endl;
		}

		else if(type == APPLY){
			child.at(0)->strout();
			std::cout << " ";
			child.at(1)->strout();
		}
		else if(type == ABST){
			std::cout << "@";
			child.at(0)->strout();
			std::cout << ":";
			child.at(1)->strout();
			std::cout << ".";
			child.at(2)->strout();
		}
		else if(type == PAIR){
			std::cout << "(";
			child.at(0)->strout();
			std::cout << ",";
			child.at(1)->strout();
			std::cout << ")";
		}
		else{
			std::visit([](auto val){std::cout << val;}, body);
		}
	}

	bool finished(){
		if(type != VALUE && type != PARENT)
			return false;

		for(auto ch : child)
			if(!ch->finished())
				return false;

		return true;
	}

};

void evalAll(std::shared_ptr<Node> node, std::shared_ptr<EvalNode> ev_ptr){

	while(node->simplify());


	ev_ptr = std::make_shared<EvalNode>(node);

	while(ev_ptr->eval());

	ev_ptr->strout();
}

int main(){

	// 読み込み
	std::string a,b;
	std::cin >> a >> b;

	input = "add (div (" + b + ", " + a + "), to_nat (any (mod (" + b + ", " + a + "))))";

	init();
	
	// 読み込んだ文字列を構文解析
	std::shared_ptr<Node> par = std::make_shared<Node>(input);

	// 型検査
	par->check();

	std::shared_ptr<EvalNode> ev_ptr;

	// 簡約と評価
	evalAll(par, ev_ptr);

}