let T be TuringStr ; 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; 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 ; ( 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
; t storeData <*s,n*>
A2:
(Sum (Prefix (<*s,n*>,(1 + 1)))) + (2 * 1) = (s + n) + 2
by Th4;
now 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;
( 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*>
;
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;
verum end;
hence
t storeData <*s,n*>
; verum