coqやlernならともかく

> 基本シンプルな機械言語でこの定義をプログラミングするとは可能だろうか?

と言い出しているのはどこの底辺大理学部職員だろうか