set f = the Function of {0,1},O;
take
I -TwoStatesMooreSM (0,1, the Function of {0,1},O)
; ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting )
thus
( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting )
; verum