let N be with_zero set ; :: thesis: 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; :: thesis: (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; :: according to AMISTD_1:def 9 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum