for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1