:: deftheorem defines Tape-Chg TURING_1:def 2 :
for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T holds Tape-Chg (t,h,s) = t +* (h .--> s);