分解還元法の分解図

u = undefined として、記号の乱用で u = {u}。ブラケット内の数値はランクが減少する量。

●opt-right
          A ⊆ B+u

[u!∈A] -----------[-1]

          A ⊆ B
●opt-both

                A+u ⊆ B+u

[u!∈A, u!∈B] -----------[-2]

                 A ⊆ B
●object
  object {pi: Ai} ⊆ object {pi: Bi}

 ------------------------------------[-2]

       Ai ⊆ Bi  (i=1, ..., n)
●array
  array [Ai] ⊆ array [Bi]

 ------------------------------------[-2]

       Ai ⊆ Bi  (i=1, ..., n)
●union-left
  A|B ⊆ C

 ----------------[-1]

  A ⊆ C, B ⊆ C
●union-right
  α=>A ⊆ (α=>B | C)

 ----------------------[-1]

  A ⊆ B
●bag
   bag [A] ⊆ bag [B]

 --------------------[-2]

      A ⊆ B
●tagging
  @α A ⊆ @α B

 ----------------[-2]

   A ⊆ B
●intersection-right
  A ⊆ B & C

 ------------------[-1]

  A ⊆ B, A ⊆ C
●intersection-left
  α=>A & α=>B ⊆ α=>C

 ------------------------------[-1]

      α=>X ⊆ α=>C 

最後の「α=>X」のところをちゃんとやる必要がある。

それと次は「すぐに偽だとわかる」ケース。

                 A+u ⊆ B

[u!∈A, u!∈B] -----------

                  false