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