:: deftheorem defines sum SCMPDS_7:def 3 :
for n being Nat holds sum n = (((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))));