theorem
for
MS being
MusicSpace for
frequency being
Element of
MS holds
(
intrval (
(penta_fondamentale (MS,frequency)),
(penta_1 (MS,frequency)))
= pythagorean_tone &
intrval (
(penta_1 (MS,frequency)),
(penta_2 (MS,frequency)))
= pythagorean_tone &
intrval (
(penta_2 (MS,frequency)),
(penta_3 (MS,frequency)))
= pentatonic_pythagorean_semiditone &
intrval (
(penta_3 (MS,frequency)),
(penta_4 (MS,frequency)))
= pythagorean_tone &
intrval (
(penta_4 (MS,frequency)),
(penta_octave (MS,frequency)))
= pentatonic_pythagorean_semiditone )