Act alpha.E ->alpha E Sumj Ej ->alpha Ej' sumEi ->alpha Ej' Com1 E ->alpha E' E|F ->alpha E'|F Com2 F ->alpha F' E|F ->alpha E|F' Com3 E ->l E' F ->l F' E|F ->tau E'|F' Res E ->alpha E' E\L ->alpha E'\L (alpha, alpha not in L) Rel E ->alpha E' E[f] ->f(alpha) E'[f] Con P ->alpha P' A ->alpha P' (A := P)