:: deftheorem defines offset TURING_1:def 3 :
for T being TuringStr
for g being Tran-Goal of T holds offset g = g `3_3 ;