let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Instruction of S st i is sequential holds
not i is halting
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over 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
set s = the State of S;
NIC (i,(IC the State of S)) = {(NextLoc ((IC the State of S),S))} by A1, Th21;
then NIC (i,(IC the State of S)) <> {(IC the State of S)} by Th15, ZFMISC_1:3;
hence not i is halting by AMISTD_1:2; :: thesis: verum