:: deftheorem defines hypomixolydian MUSIC_S1:def 99 :
for HPS being MusicSpace
for n being natural non zero Number
for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds
( scale is hypomixolydian iff ex t1, t2 being positive Real st
( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );