DES-PIPINV = DES-PIP " by Lm7, FUNCT_2:60;