let T be TuringStr ; :: thesis: for t being Tape of T
for s being Element of NAT
for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds
t is_1_between s,(s + (f /. 1)) + 2
let t be Tape of T; :: thesis: for s being Element of NAT
for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds
t is_1_between s,(s + (f /. 1)) + 2
let s be Element of NAT ; :: thesis: for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds
t is_1_between s,(s + (f /. 1)) + 2
let f be FinSequence of NAT ; :: thesis: ( len f >= 1 & t storeData <*s*> ^ f implies t is_1_between s,(s + (f /. 1)) + 2 )
set g = <*s*> ^ f;
assume that
A1: len f >= 1 and
A2: t storeData <*s*> ^ f ; :: thesis: t is_1_between s,(s + (f /. 1)) + 2
len <*s*> = 1 by FINSEQ_1:39;
then len (<*s*> ^ f) = 1 + (len f) by FINSEQ_1:22;
then len (<*s*> ^ f) >= 1 + 1 by A1, XREAL_1:7;
then A3: 1 < len (<*s*> ^ f) by XXREAL_0:2;
( (Sum (Prefix ((<*s*> ^ f),1))) + (2 * (1 - 1)) = s & (Sum (Prefix ((<*s*> ^ f),(1 + 1)))) + (2 * 1) = (s + (f /. 1)) + 2 ) by A1, Th20;
hence t is_1_between s,(s + (f /. 1)) + 2 by A2, A3; :: thesis: verum