(Head s) + (offset (TRAN s)) in INT by INT_1:def 2;
hence ( ( s `1_3 <> the AcceptS of T implies [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] is All-State of T ) & ( not s `1_3 <> 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