О длине совмещающего типа в исчислении Ламбека

В 1992 г. М. Р. Пентусом был установлен критерий существования такого типа $C$, что для данных типов $A$ и $B$ секвенции $A\to C$ и $B\to C$ являются выводимыми в исчислении Ламбека. В настоящей статье предлагается алгоритм построения типа $C$ (в случае, если он существует) и доказывается квадратичная верхняя оценка его длины.