take the data-only PartState of S ; :: thesis: the data-only PartState of S is program-free
thus the data-only PartState of S is program-free ; :: thesis: verum