:: deftheorem defines exp_R1 E_TRANS1:def 1 :
exp_R1 = exp_R ^ ;