let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N holds (il. S,0 ) .--> (halt S) is closed
let S be non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N; :: thesis: (il. S,0 ) .--> (halt S) is closed
set F = (il. S,0 ) .--> (halt S);
A1: dom ((il. S,0 ) .--> (halt S)) = {(il. S,0 )} by FUNCOP_1:19;
let l be Instruction-Location of S; :: according to AMISTD_1:def 17 :: thesis: ( l in dom ((il. S,0 ) .--> (halt S)) implies NIC (pi ((il. S,0 ) .--> (halt S)),l),l c= dom ((il. S,0 ) .--> (halt S)) )
assume A2: l in dom ((il. S,0 ) .--> (halt S)) ; :: thesis: NIC (pi ((il. S,0 ) .--> (halt S)),l),l c= dom ((il. S,0 ) .--> (halt S))
then A3: l = il. S,0 by A1, TARSKI:def 1;
pi ((il. S,0 ) .--> (halt S)),l = ((il. S,0 ) .--> (halt S)) . l by A2, AMI_1:def 47
.= halt S by A3, FUNCOP_1:87 ;
hence NIC (pi ((il. S,0 ) .--> (halt S)),l),l c= dom ((il. S,0 ) .--> (halt S)) by A1, A3, Th15; :: thesis: verum