:: deftheorem defines is_1_between TURING_1:def 12 :
for T being TuringStr
for t being Tape of T
for i, j being Integer holds
( t is_1_between i,j iff ( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds
t . k = 1 ) ) );