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

now :: thesis: for i being Nat st 1 <= i & i < len <*s,n*> holds
t is_1_between (Sum (Prefix (<*s,n*>,i))) + (2 * (i - 1)),(Sum (Prefix (<*s,n*>,(i + 1)))) + (2 * i)

let i be Nat; :: thesis: ( 1 <= i & i < len <*s,n*> implies t is_1_between (Sum (Prefix (<*s,n*>,i))) + (2 * (i - 1)),(Sum (Prefix (<*s,n*>,(i + 1)))) + (2 * i) )
assume that
A3: 1 <= i and
A4: i < len <*s,n*> ; :: thesis: t is_1_between (Sum (Prefix (<*s,n*>,i))) + (2 * (i - 1)),(Sum (Prefix (<*s,n*>,(i + 1)))) + (2 * i)
len <*s,n*> = 2 by FINSEQ_1:44;
then i + 1 <= 1 + 1 by A4, INT_1:7;
then i <= 1 by XREAL_1:6;
then i = 1 by A3, XXREAL_0:1;
hence t is_1_between (Sum (Prefix (<*s,n*>,i))) + (2 * (i - 1)),(Sum (Prefix (<*s,n*>,(i + 1)))) + (2 * i) by A1, A2, Th4; :: thesis: verum

end;

hence t storeData <*s,n*> ; :: thesis: verum