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

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

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

end;

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

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

suppose x = 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 = 1 ; :: thesis: x in dom (stop (Load i))

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

end;

end;