let T be TuringStr ; :: thesis: for s being All-State of T st s is Accept-Halt holds
ex k being Element of NAT st
( ((Computation s) . k) `1 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T ) )
let s be All-State of T; :: thesis: ( s is Accept-Halt implies ex k being Element of NAT st
( ((Computation s) . k) `1 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T ) ) )
defpred S₁[ Nat] means ((Computation s) . $1) `1 = the AcceptS of T;
assume A1: s is Accept-Halt ; :: thesis: ex k being Element of NAT st
( ((Computation s) . k) `1 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T ) )
then ex k being Element of NAT st ((Computation s) . k) `1 = the AcceptS of T by Def9;
then A2: ex k being Nat st S₁[k] ;
consider k being Nat such that
A3: ( S₁[k] & ( for n being Nat st S₁[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 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T ) )
thus S₁[k] by A3; :: thesis: ( Result s = (Computation s) . k & ( for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T ) )
thus Result s = (Computation s) . k by A1, A3, Def10; :: thesis: for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T
thus for i being Element of NAT st i < k holds
((Computation s) . i) `1 <> the AcceptS of T by A3; :: thesis: verum