let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed weakly_standard AMI-Struct of N holds (il. S,0 ) .--> (halt S) is closed
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed weakly_standard AMI-Struct of N; :: thesis: (il. S,0 ) .--> (halt S) is closed
reconsider F = (il. S,0 ) .--> (halt S) as NAT -defined the Instructions of S -valued FinPartState of ;
let l be Element of NAT ; :: according to AMISTD_1:def 17 :: thesis: ( not l in proj1 ((il. S,0 ) .--> (halt S)) or NIC (((il. S,0 ) .--> (halt S)) /. l),l c= proj1 ((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= proj1 ((il. S,0 ) .--> (halt S))
A2: dom F = {(il. S,0 )} by FUNCOP_1:19;
then A3: l = il. S,0 by A1, TARSKI:def 1;
F /. l = F . l by A1, PARTFUN1:def 8
.= halt S by A3, FUNCOP_1:87 ;
hence NIC (((il. S,0 ) .--> (halt S)) /. l),l c= proj1 ((il. S,0 ) .--> (halt S)) by A2, A3, AMISTD_1:15; :: thesis: verum