let T be TuringStr ; :: thesis: for s being All-State of T st s is Accept-Halt holds

ex k being Nat st

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . 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

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) ) )

defpred S_{1}[ Nat] means ((Computation s) . $1) `1_3 = the AcceptS of T;

assume A1: s is Accept-Halt ; :: thesis: ex k being Nat st

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

then ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T ;

then A2: ex k being Nat st S_{1}[k]
;

consider k being Nat such that

A3: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A2);

reconsider k = k as Element of NAT by ORDINAL1:def 12;

take k ; :: thesis: ( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

thus S_{1}[k]
by A3; :: thesis: ( Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

thus Result s = (Computation s) . k by A1, A3, Def9; :: thesis: for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T

thus for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T by A3; :: thesis: verum

ex k being Nat st

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . 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

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) ) )

defpred S

assume A1: s is Accept-Halt ; :: thesis: ex k being Nat st

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

then ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T ;

then A2: ex k being Nat st S

consider k being Nat such that

A3: ( S

k <= n ) ) from NAT_1:sch 5(A2);

reconsider k = k as Element of NAT by ORDINAL1:def 12;

take k ; :: thesis: ( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

thus S

((Computation s) . i) `1_3 <> the AcceptS of T ) )

thus Result s = (Computation s) . k by A1, A3, Def9; :: thesis: for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T

thus for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T by A3; :: thesis: verum