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