let x be set ; :: thesis: for i being Instruction of holds
( x in dom (stop (Load i)) iff ( x = inspos 0 or x = inspos 1 ) )
let i be Instruction of ; :: thesis: ( x in dom (stop (Load i)) iff ( x = inspos 0 or x = inspos 1 ) )
set pi = stop (Load i);
set A = NAT ;
A1: card (stop (Load i)) = 2 by Th8;

hereby :: thesis: ( ( x = inspos 0 or x = inspos 1 ) implies x in dom (stop (Load i)) )

assume A2: x in dom (stop (Load i)) ; :: thesis: ( x = inspos 0 or x = inspos 1 )
dom (stop (Load i)) c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCMPDS by A2, AMI_1:def 4;
reconsider n = l as Element of NAT by ORDINAL1:def 13;
n < 1 + 1 by A1, A2, SCMPDS_4:1;
then n <= 1 by NAT_1:13;
hence ( x = inspos 0 or x = inspos 1 ) by NAT_1:26; :: thesis: verum

end;

assume A3: ( x = inspos 0 or x = inspos 1 ) ; :: thesis: x in dom (stop (Load i))

per cases ( x = inspos 0 or x = inspos 1 ) by A3;

suppose x = inspos 0 ; :: thesis: x in dom (stop (Load i))

hence x in dom (stop (Load i)) by A1, SCMPDS_4:1; :: thesis: verum

end;

suppose x = inspos 1 ; :: thesis: x in dom (stop (Load i))

hence x in dom (stop (Load i)) by A1, SCMPDS_4:1; :: thesis: verum

end;

end;