let loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom (stop I) & (stop I) . loc <> halt SCMPDS holds
loc in dom I
let I be Program of SCMPDS; :: thesis: ( loc in dom (stop I) & (stop I) . loc <> halt SCMPDS implies loc in dom I )
assume that
A1: loc in dom (stop I) and
A2: (stop I) . loc <> halt SCMPDS ; :: thesis: loc in dom I
set SS = Stop SCMPDS;
set S2 = Shift ((Stop SCMPDS),(card I));
assume not loc in dom I ; :: thesis: contradiction
then loc in dom (Shift ((Stop SCMPDS),(card I))) by A1, FUNCT_4:13;
then loc in { (l1 + (card I)) where l1 is Element of NAT : l1 in dom (Stop SCMPDS) } by VALUED_1:def 12;
then consider l1 being Element of NAT such that
A3: loc = l1 + (card I) and
A4: l1 in dom (Stop SCMPDS) ;
y: 0 in dom (Stop SCMPDS) by COMPOS_1:45;
x: (Stop SCMPDS) . 0 = halt SCMPDS by AFINSQ_1:38;
dom (Stop SCMPDS) = {0} by AFINSQ_1:36, CARD_1:87;
then l1 = 0 by A4, TARSKI:def 1;
hence contradiction by A2, A3, x, y, AFINSQ_1:def 4; :: thesis: verum