let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed weakly_standard AMI-Struct of N
for i being Instruction of S st i is sequential holds
not i is halting
let S be non empty stored-program IC-Ins-separated definite realistic steady-programmed weakly_standard AMI-Struct of N; :: thesis: for i being Instruction of S st i is sequential holds
not i is halting
let i be Instruction of S; :: thesis: ( i is sequential implies not i is halting )
assume A1: i is sequential ; :: thesis: not i is halting
consider s being State of S;
NIC (i,(IC s)) = {(NextLoc ((IC s),S))} by A1, Th41;
then NIC (i,(IC s)) <> {(IC s)} by Th35, ZFMISC_1:6;
hence not i is halting by AMISTD_1:15; :: thesis: verum