:: deftheorem defines Trivial-multLoopStr_0 ALGSTR_0:def 34 :
Trivial-multLoopStr_0 = multLoopStr_0(# {0},op2,op0,op0 #);