definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
C G L (ⒶVs.V2) → ⬆[0, i+1] V1 ≡ V2 →
⬇[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
definition S6 ≝ λRP,C:candidate.
definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
C G L (ⒶVs.V2) → ⬆[0, i+1] V1 ≡ V2 →
⬇[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
definition S6 ≝ λRP,C:candidate.