let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 2 = IncAddr (i3,2)
let i1, i2, i3, i4 be No-StopCode Instruction of S; :: thesis: (((i1 ';' i2) ';' i3) ';' i4) . 2 = IncAddr (i3,2)
LastLoc ((i1 ';' i2) ';' i3) = 3 by Th31;
hence (((i1 ';' i2) ';' i3) ';' i4) . 2 = ((i1 ';' i2) ';' i3) . 2 by Th23, Th28
.= IncAddr (i3,2) by Th50 ;
:: thesis: verum