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