:: deftheorem Def6 defines Following TURING_1:def 6 :
for T being TuringStr
for s being All-State of T holds
( ( s `1_3 <> the AcceptS of T implies Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] ) & ( not s `1_3 <> the AcceptS of T implies Following s = s ) );