let i, j, k be Instruction of SCMPDS; :: thesis: for I being Program of holds ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)
let I be Program of ; :: thesis: ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)
thus ((i ';' I) ';' j) ';' k = (i ';' (I ';' j)) ';' k by SCMPDS_4:15
.= i ';' ((I ';' j) ';' k) by SCMPDS_4:15 ; :: thesis: verum