:: deftheorem defines storeData TURING_1:def 13 :
for f being natural-valued FinSequence
for T being TuringStr
for t being Tape of T holds
( t storeData f iff for i being Nat st 1 <= i & i < len f holds
t is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i) );