Нормализация термов в точных моделях логики доказательств LP

Базисная модель логики свидетельств является точной, если конструкторы свидетельских термов $\cdot, +, !$ в модели интерпретируются в точности в соответствии с их неформальным пониманием как применение правила modus ponens, объединение и верификация свидетельств. В статье строится пример точной базисной модели для логики доказательств LP и доказывается, что в точных моделях LP каждый терм эквивалентен некоторому полиному доказательств.