let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds (il. (S,0)) .--> (halt S) is really-closed
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; (il. (S,0)) .--> (halt S) is really-closed
reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued finite Function ;
let l be Nat; AMISTD_1:def 9 ( not l in dom ((il. (S,0)) .--> (halt S)) or NIC ((((il. (S,0)) .--> (halt S)) /. l),l) c= dom ((il. (S,0)) .--> (halt S)) )
assume A1:
l in dom ((il. (S,0)) .--> (halt S))
; NIC ((((il. (S,0)) .--> (halt S)) /. l),l) c= dom ((il. (S,0)) .--> (halt S))
A3:
l = il. (S,0)
by A1, TARSKI:def 1;
F /. l =
F . l
by A1, PARTFUN1:def 6
.=
halt S
by A3, FUNCOP_1:72
;
hence
NIC ((((il. (S,0)) .--> (halt S)) /. l),l) c= dom ((il. (S,0)) .--> (halt S))
by A3, AMISTD_1:2; verum