consider f being Function of {0,1},O;
take I -TwoStatesMooreSM (0,1,f) ; :: thesis: ( I -TwoStatesMooreSM (0,1,f) is calculating_type & I -TwoStatesMooreSM (0,1,f) is halting )
thus ( I -TwoStatesMooreSM (0,1,f) is calculating_type & I -TwoStatesMooreSM (0,1,f) is halting ) ; :: thesis: verum