:: deftheorem defines hepta_octave MUSIC_S1:def 88 :
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds hepta_octave (HPS,frequency) = Octave (HPS,frequency);