let S be COM-Struct ; :: thesis: for I being Program of S
for loc being Nat st loc in dom (stop I) & (stop I) . loc <> halt S holds
loc in dom I
let I be Program of S; :: thesis: for loc being Nat st loc in dom (stop I) & (stop I) . loc <> halt S holds
loc in dom I
let loc be Nat; :: thesis: ( loc in dom (stop I) & (stop I) . loc <> halt S implies loc in dom I )
assume that
A1: loc in dom (stop I) and
A2: (stop I) . loc <> halt S ; :: thesis: loc in dom I
set SS = Stop S;
set S2 = Shift ((Stop S),(card I));
XX: stop I = I +* (Shift ((Stop S),(card I))) by AFINSQ_1:77;
assume not loc in dom I ; :: thesis: contradiction
then loc in dom (Shift ((Stop S),(card I))) by A1, FUNCT_4:12, XX;
then loc in { (l1 + (card I)) where l1 is Element of NAT : l1 in dom (Stop S) } 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 S) ;
A5: 0 in dom (Stop S) by Th3;
A6: (Stop S) . 0 = halt S by AFINSQ_1:34;
dom (Stop S) = {0} by AFINSQ_1:33, CARD_1:49;
then l1 = 0 by A4, TARSKI:def 1;
hence contradiction by A2, A3, A6, A5, AFINSQ_1:def 3; :: thesis: verum