let T be TuringStr ; :: thesis: for t being Tape of T
for s, n being Element of NAT st t storeData <*s,n*> holds
t is_1_between s,(s + n) + 2
let t be Tape of T; :: thesis: for s, n being Element of NAT st t storeData <*s,n*> holds
t is_1_between s,(s + n) + 2
let s, n be Element of NAT ; :: thesis: ( t storeData <*s,n*> implies t is_1_between s,(s + n) + 2 )
set f = <*s,n*>;
assume A1: t storeData <*s,n*> ; :: thesis: t is_1_between s,(s + n) + 2
A2: len <*s,n*> = 2 by FINSEQ_1:44;
( (Sum (Prefix (<*s,n*>,1))) + (2 * (1 - 1)) = s & (Sum (Prefix (<*s,n*>,(1 + 1)))) + (2 * 1) = (s + n) + 2 ) by Th4;
hence t is_1_between s,(s + n) + 2 by A1, A2; :: thesis: verum