thus (la,lb) --> (a,b) is FinPartState of SCMPDS ; :: thesis: verum