Soundness and Completeness

When decompose/abstract the system S to

S1||S2||S3

Soundness:

Whatever true in S1||S2||S3 true in S is sound

S1||S2||S3 is subset of S

Completeness:

Whatever true in S true in S1||S2||S3 is complete

S is subset of S1||S2||S3

When Soundness and Completeness hold

Checking S is equivalent of checking S1||S2||S3