let S be COM-Struct ; :: thesis: for J, I being Program of S holds I ';' J = (CutLastLoc I) ^ (IncAddr (J,((card I) -' 1)))
let J, I be Program of S; :: thesis: I ';' J = (CutLastLoc I) ^ (IncAddr (J,((card I) -' 1)))
card (CutLastLoc I) = (card I) -' 1 by VALUED_1:65;
hence I ';' J = (CutLastLoc I) ^ (IncAddr (J,((card I) -' 1))) by AFINSQ_1:77; :: thesis: verum