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