^1ВЫП (^ , ОТВЕТ ^5, :г,^))^'^ П0Д10СЛ (34.,^)) V

8 ) V5\/^^^\/A СНЕПРВ0ПС^,сс,^,4) s

^3s^3Si (НЕПРВОП Г5^,^,^,А)аПСЛАН (^2,^)& ЯВ ^ соед С5,,5г;^И.З'^35Л

ГЭЛАН 0,3^) Ä НЕПРОП С>.^,ДД>П0Ж10СЛ r^A,4)i^ 2- ВЫП С^, ОТВЕТ {;5,C3r,^))J\/

3^ / H№ÄC^^3f ) ^ 3KBf^>)ÄHEIIPB3Ärs,cr^^J)j^

ВсштСу - , ОТВЕТ Г^.^.^))) '

в расширенной таким образом системе доказуема теорема : Vx Vs Ч}ЩА ПСЛАН (s, s,, ос^^) &г ЛУа(0ШЩ (j,A) ^ ПРВОП (соед (s, s Д:г^^,а) \/ \/. HEÎTPBOn (соед (s^ ^0. ^-^> А ))) ^

Содержательный смысл этой теоремы отражает смысл рочной процедуры.

Из доказательства этой теоремы методом , предложенным в работе [з] , можно извлечь следущий алгоритм проверочной цедуры.

1 . Если выполнено условие Г » то считается, что задача решена правильно. Анализ прекращается. Шаче переход к шагу 2.

2 . Из анализа условий Г^ , ..., F\ составляется спи - сок имен операций, выполненных правильно (СП) и список имен операций выполненных неправильно (СН). Операции, имена которых входят в СН,считаются выполненными неправильно. Операции, имена которых входят в СП и не входят в СН, считаются вьшолненными правильно«

3 . Определяется существенная операция эталона, имя которой не вошло в СП и в СН. Если такой операции нет, анализ вается.

4 . Для выбранной операции определяется соответствующая ей задача (подзадача исходной задачи).

5 . Ддя найденной подзадачи каждой задачи проводится анализ (описан ниже), в результате которого определяется, правильно ЕЛЕ неправильно решена данная подзадача.

6 . Если подзадача хюшена правильно, то имя соответствую -

- 58 -