let T be TuringStr ; :: thesis: 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),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3),(Head s),((TRAN s) `2)))]
let s be All-State of T; :: thesis: for p, h, t being set st s = [p,h,t] & p <> the AcceptS of T holds
Following s = [((TRAN s) `1),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3),(Head s),((TRAN s) `2)))]
let p, h, t be set ; :: thesis: ( s = [p,h,t] & p <> the AcceptS of T implies Following s = [((TRAN s) `1),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3),(Head s),((TRAN s) `2)))] )
assume that
A1: s = [p,h,t] and
A2: p <> the AcceptS of T ; :: thesis: Following s = [((TRAN s) `1),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3),(Head s),((TRAN s) `2)))]
s `1 = p by A1, MCART_1:64;
hence Following s = [((TRAN s) `1),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3),(Head s),((TRAN s) `2)))] by A2, Def7; :: thesis: verum