let T be TuringStr ; 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; 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 ; ( t storeData <*s,n*> implies t is_1_between s,(s + n) + 2 )
set f = <*s,n*>;
assume A1:
t storeData <*s,n*>
; 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; verum