let I be Program of ; :: thesis: for k being Element of NAT holds UsedIntLoc I = UsedIntLoc (Reloc (I,k))
let k be Element of NAT ; :: thesis: UsedIntLoc I = UsedIntLoc (Reloc (I,k))
UsedIntLoc (Reloc (I,k)) = UsedIntLoc (Reloc (I,k))
.= UsedIntLoc (Shift (I,k)) by Th28
.= UsedIntLoc I by Th26 ;
hence UsedIntLoc I = UsedIntLoc (Reloc (I,k)) ; :: thesis: verum