let s be All-State of U3(n)Turing ; :: thesis: for p, h, t being set st s = [p,h,t] & p <> 3 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 <> 3 implies Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))] )
assume A1: ( s = [p,h,t] & p <> 3 ) ; :: thesis: Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]
3 = the AcceptS of U3(n)Turing by Def22;
hence Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))] by A1, Th29; :: thesis: verum