let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N holds Shift (Stop S),k = (il. S,k) .--> (halt S)
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N holds Shift (Stop S),k = (il. S,k) .--> (halt S)
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N; :: thesis: Shift (Stop S),k = (il. S,k) .--> (halt S)
A1: dom (Shift (Stop S),k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom (Stop S) } by Def16;
A2: il. S,0 in dom (Stop S) by Lm5;
A3: dom (Shift (Stop S),k) = {(il. S,k)}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(il. S,k)} c= dom (Shift (Stop S),k)

let x be set ; :: thesis: ( x in dom (Shift (Stop S),k) implies x in {(il. S,k)} )
assume x in dom (Shift (Stop S),k) ; :: thesis: x in {(il. S,k)}
then consider m being Element of NAT such that
A4: x = il. S,(m + k) and
A5: il. S,m in dom (Stop S) by A1;
il. S,m in {(il. S,0 )} by A5, Lm5;
then il. S,m = il. S,0 by TARSKI:def 1;
then m = 0 by AMISTD_1:25;
hence x in {(il. S,k)} by A4, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(il. S,k)} or x in dom (Shift (Stop S),k) )
assume x in {(il. S,k)} ; :: thesis: x in dom (Shift (Stop S),k)
then x = il. S,(0 + k) by TARSKI:def 1;
hence x in dom (Shift (Stop S),k) by A1, A2; :: thesis: verum

end;

A6: dom ((il. S,k) .--> (halt S)) = {(il. S,k)} by FUNCOP_1:19;
for x being set st x in {(il. S,k)} holds
(Shift (Stop S),k) . x = ((il. S,k) .--> (halt S)) . x

proof

let x be set ; :: thesis: ( x in {(il. S,k)} implies (Shift (Stop S),k) . x = ((il. S,k) .--> (halt S)) . x )
assume x in {(il. S,k)} ; :: thesis: (Shift (Stop S),k) . x = ((il. S,k) .--> (halt S)) . x
then A7: x = il. S,(0 + k) by TARSKI:def 1;
il. S,0 in dom (Stop S) by Lm5;
hence (Shift (Stop S),k) . x = (Stop S) . (il. S,0 ) by A7, Def16
.= halt S by FUNCOP_1:87
.= ((il. S,k) .--> (halt S)) . x by A7, FUNCOP_1:87 ;
:: thesis: verum

end;

hence Shift (Stop S),k = (il. S,k) .--> (halt S) by A3, A6, FUNCT_1:9; :: thesis: verum