let T be TuringStr ; :: thesis: for s being All-State of T st s is Accept-Halt holds
ex k being Nat st
( (() . k) `1_3 = the AcceptS of T & Result s = () . k & ( for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T ) )

let s be All-State of T; :: thesis: ( s is Accept-Halt implies ex k being Nat st
( (() . k) `1_3 = the AcceptS of T & Result s = () . k & ( for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T ) ) )

defpred S1[ Nat] means (() . \$1) `1_3 = the AcceptS of T;
assume A1: s is Accept-Halt ; :: thesis: ex k being Nat st
( (() . k) `1_3 = the AcceptS of T & Result s = () . k & ( for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T ) )

then ex k being Nat st (() . k) `1_3 = the AcceptS of T ;
then A2: ex k being Nat st S1[k] ;
consider k being Nat such that
A3: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: ( (() . k) `1_3 = the AcceptS of T & Result s = () . k & ( for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T ) )

thus S1[k] by A3; :: thesis: ( Result s = () . k & ( for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T ) )

thus Result s = () . k by A1, A3, Def9; :: thesis: for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T

thus for i being Nat st i < k holds
(() . i) `1_3 <> the AcceptS of T by A3; :: thesis: verum