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;

A2: (IC the State of S) + 1 <> (IC the State of S) + 0 ;

NIC (i,(IC the State of S)) = {((IC the State of S) + 1)} by A1, Th12;

then NIC (i,(IC the State of S)) <> {(IC the State of S)} by ZFMISC_1:3, A2;

hence not i is halting by Th2; :: thesis: verum

assume A1: i is sequential ; :: thesis: not i is halting

set s = the State of S;

A2: (IC the State of S) + 1 <> (IC the State of S) + 0 ;

NIC (i,(IC the State of S)) = {((IC the State of S) + 1)} by A1, Th12;

then NIC (i,(IC the State of S)) <> {(IC the State of S)} by ZFMISC_1:3, A2;

hence not i is halting by Th2; :: thesis: verum