let a be Int_position; :: thesis: for i being Integer
for I being Program of SCMPDS holds
( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) )
let i be Integer; :: thesis: for I being Program of SCMPDS holds
( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) )
let I be Program of SCMPDS; :: thesis: ( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) )
3 <= (card I) + 3 by NAT_1:11;
then ( 0 < (card I) + 3 & 1 < (card I) + 3 ) by XXREAL_0:2;
hence ( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) ) by Th9; :: thesis: verum