(Head s) + (offset (TRAN s)) in INT by INT_1:def 2;
hence ( ( s `1 <> the AcceptS of T implies [((TRAN s) `1),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3),(Head s),((TRAN s) `2)))] is All-State of T ) & ( not s `1 <> the AcceptS of T implies s is All-State of T ) & ( for b₁ being All-State of T holds verum ) ) by MCART_1:69; :: thesis: verum