theorem Th25: :: TURING_1:25

for T being TuringStr
for s being All-State of T
for p, h, t being set st s = [p,h,t] & p <> the AcceptS of T holds
Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] by Def6;