型解析：ユニフィケーションの進行と成功／完全失敗

証明ターゲット S⊆T が完全失敗とは、S∩T = never が証明できてしまうこと。以下、S∩T = never を、S⊥T を書くことにする。

• S⊆T が成功 ⇔ S⊆T が成立（健全性より）
• S⊆T が完全失敗 ⇔ S⊥T が成立
• S⊆T が条件付きで成功 ⇔ S⊆T は成立しない（その意味では失敗）が、S⊥T ではない。

トップダウン・ユニフィケーションのとある過程（実行の途中）で成功／完全失敗したとき、その成功／完全失敗が、より上位に伝搬していく状況は以下のとおりである。

1. joinのすべての成分で成功すれば、そのjoinは成功。joinのすべての成分で完全失敗すれば、そのjoinは完全失敗。その他は成功でも完全失敗でもない。
2. interの進行先で成功しても完全失敗しても、inter全体は成功も完全失敗もしない。なぜなら、interは必ず変数を含むから。
3. b-optの進行先で成功すれば成功。b-optの進行先で完全失敗してもb-optは完全失敗しない。条件 not_exist が残る。
4. r-optの進行先で成功すれば成功。r-optの進行先で完全失敗すればr-optは完全失敗。
5. l-optの進行先で成功しても成功ではない。l-optの進行先で完全失敗すればr-optは完全失敗。
6. xunionの進行先で成功すれば成功。xunionの進行先で完全失敗すれば完全失敗。
7. arrayのすべての進行先で成功すれば成功。arrayの進行先のひとつで完全失敗すればarrayが完全失敗。
8. objectのすべての進行先で成功すれば成功。objectの進行先のひとつで完全失敗すればobjectが完全失敗。
9. tagの進行先で成功すれば成功。tagの進行先で完全失敗すればtagが完全失敗。

完全失敗に注目すると：

1. joinのすべての成分で完全失敗すれば、そのjoinは完全失敗。ALL条件
2. （interは完全失敗しない。）
3. （b-optは完全失敗しない。）
4. r-optの進行先で完全失敗すればr-optは完全失敗。
5. l-optの進行先で完全失敗すればr-optは完全失敗。
6. xunionの進行先で完全失敗すれば完全失敗。
7. arrayの進行先のひとつで完全失敗すればarrayが完全失敗。SOME条件
8. objectの進行先のひとつで完全失敗すればobjectが完全失敗。SOME条件
9. tagの進行先で完全失敗すればtagが完全失敗。

join(ALL), r-opt, l-opt, xunion, array(SOME), object(SOME), tagの7つのケースで、ボトムアップに完全失敗の可能性がある。