(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:73; :: thesis: verum