Вариант индуктивной тактики c, который не требует использования `запомнить` на подтермах

Question

Допустим, у меня есть два отношения R1 и R2. Если мне нужно решить проблему путем индукции через термин R1 A (R2 B C), мне сначала нужно сделать remember R2 B C, в противном случае я теряю информацию о том, что второй аргумент R1 равен R2 B C. Есть ли вариант индукции, что tacti c, который не требует, чтобы я с этим справился?

Answer 1

Ответ - нет.

Способ индукции работает, он заменяет каждый экземпляр каждого аргумента значениями, которые появляются в одном и том же месте в конструкторах индуктивных предикатов. Чтобы сделать это проще, remember tacti c заменяет составное выражение (R2 B C) на переменную. иногда этого можно избежать, если в вашей цели появляется (R2 B C), но это редко.