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));
A3: 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, A3, FUNCT_4:12;
then loc in { (l1 + (card I)) where l1 is Nat : l1 in dom (Stop S) } by VALUED_1:def 12;
then consider l1 being Nat such that
A4: loc = l1 + (card I) and
A5: l1 in dom (Stop S) ;
A6: 0 in dom (Stop S) by Th2;
A7: (Stop S) . 0 = halt S ;
l1 = 0 by A5, TARSKI:def 1;
hence contradiction by A2, A4, A7, A6, AFINSQ_1:def 3; :: thesis: verum