:: deftheorem defines triv-times SFMASTR2:def 5 :
for d being read-write Int-Location holds triv-times d = times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))));