C

C. Теорема Гливенко

Имя входного файла:                 стандартный ввод
Имя выходного файла:                стандартный вывод
Ограничение по времени:             15 секунд
Ограничение по памяти:              512 мегабайт

На вход вашей программе дается корректное доказательство утверждения α в классическом исчислении высказываний. Доказательство записано с использованием грамматики из предыдущего задания. Вам требуется построить корректное доказательство утверждения ¬¬α в интуиционистском исчислении высказываний.

Формат входных данных

Во входном файле задано доказательство утверждения α в классическом исчислении высказываний. Размер входного файла не превышает 5 КБ.

Формат выходных данных

Файл должен содержать корректное доказательство утверждения ¬¬α в интуиционистском исчислении высказываний в том же контексте, что доказательство во входном файле.

Пример

стандартный ввод
A |- A
A
стандартный вывод
A |- !!A
A
(A -> (!A -> A))
(!A -> A)
(!A -> (!A -> !A))
((!A -> (!A -> !A)) -> ((!A -> ((!A -> !A) -> !A)) -> (!A -> !A)))
((!A -> ((!A -> !A) -> !A)) -> (!A -> !A))
(!A -> ((!A -> !A) -> !A))
(!A -> !A)
((!A -> A) -> ((!A -> !A) -> !!A))
((!A -> !A) -> !!A)
!!A