let s be All-State of SumTuring; :: thesis: for p, h, t being set st s = [p,h,t] & p <> 5 holds
Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))]
let p, h, t be set ; :: thesis: ( s = [p,h,t] & p <> 5 implies Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] )
assume A1: ( s = [p,h,t] & p <> 5 ) ; :: thesis: Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))]
5 = the AcceptS of SumTuring by Def14;
hence Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] by A1, Th25; :: thesis: verum