:: deftheorem defines SBP SCMP_GCD:def 3 :
SBP = intpos 1;