:: deftheorem defines octatonic MUSIC_S1:def 61 :
for MS being MusicSpace
for scale being Element of 9 -tuples_on the carrier of MS holds
( scale is octatonic iff ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6, r7, r8, r9 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & scale . 7 = r7 & scale . 8 = r8 & scale . 9 = r9 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 & r8 < r9 & scale . 9 = Octave (MS,frequency) ) );