(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_{1} being All-State of T holds verum ) )
by MCART_1:69; :: thesis: verum

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