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