:: deftheorem defines Goto SCMPDS_6:def 1 :
for k1 being Integer holds Goto k1 = Load (goto k1);