:: deftheorem defines mod SCM_COMP:def 7 :
for t1, t2 being bin-term holds t1 mod t2 = [0,4] -tree (t1,t2);