[kb]  Several formal proofs, definitions and statements added