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