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 SCMNORM:2;
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, SCMPDS_4:38, x, y; :: thesis: verum