set f = the Function of {0,1},O;

take I -TwoStatesMooreSM (0,1, the Function of {0,1},O) ; :: thesis: ( 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 ) ; :: thesis: verum

take I -TwoStatesMooreSM (0,1, the Function of {0,1},O) ; :: thesis: ( 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 ) ; :: thesis: verum