theorem Th45: :: COMPOS_2:46

for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S holds ((i ';' j) ';' k) . 1 = IncAddr (j,1)