let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N; :: thesis: for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let loc be Instruction-Location of S; :: thesis: for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let l be Element of ObjectKind (IC S); :: thesis: ( l = loc implies for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting )
assume A1: l = loc ; :: thesis: for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let h be Element of ObjectKind loc; :: thesis: ( h = halt S implies (IC S),loc --> l,h is halting )
assume A2: h = halt S ; :: thesis: (IC S),loc --> l,h is halting
thus (IC S),loc --> l,h is halting :: thesis: verum

proof

let s be State of S; :: according to AMI_1:def 26 :: thesis: ( (IC S),loc --> l,h c= s implies ProgramPart s halts_on s )
assume A3: (IC S),loc --> l,h c= s ; :: thesis: ProgramPart s halts_on s
take 0 ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,0 ) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,0 )) = halt S )
IC (Computation s,0 ) in NAT by Def4;
hence IC (Computation s,0 ) in dom (ProgramPart s) by LmU; :: thesis: (ProgramPart s) . (IC (Computation s,0 )) = halt S
CurInstr (Computation s,0 ) = CurInstr s by Th13
.= halt S by A1, A2, A3, Th64 ;
hence (ProgramPart s) . (IC (Computation s,0 )) = halt S by LmX; :: thesis: verum

end;