decides_hp(B)           == all(C,program(C)=> all(D,decides(B,C,D))).

program_decides_hp(B)   == (program(B)and decides_hp(B)).
algorithm_decides_hp(B) == (algorithm(B)and decides_hp(B)).

program_halts(B,C)      == (program(B)and halts(B,C)).
program_not_halts(B,C)  == (program(B)and ~halts(B,C)).
outputs(B,C,O)          -> program_halts(B,C).


outputs_if_halts_on(B,O,C,D) 
            == (program_halts(C,cons(D,nil)) => outputs(B,cons(C,cons(D,nil)),O)).

outputs_if_not_halts_on(B,O,C,D) 
            == (program_not_halts(C,cons(D,nil)) => outputs(B,cons(C,cons(D,nil)),O)).

exists(B,algorithm_decides_hp(B)) -> exists(C,program_decides_hp(C)).

decides(B,C,D) == (outputs_if_halts_on(B,good,C,D) and
	           outputs_if_not_halts_on(B,bad,C,D)).



% self halt C -> DP halts on C
exists(B,program(B)
         and all(C,outputs_if_halts_on(B,good,C,C) and
                   outputs_if_not_halts_on(B,bad,C,C)))
	->
exists(D,program(D)
       and all(C,(program_halts(C,cons(C,nil))  => outputs(D,cons(C,nil),good))
	          and
		 (program_not_halts(C,cons(C,nil)) => outputs(D,cons(C,nil),bad)))).

exists(B,program(B)
         and all(C,(program_halts(C,cons(C,nil))  => outputs(B,cons(C,nil),good)) and
		   (program_not_halts(C,cons(C,nil)) => outputs(B,cons(C,nil),bad))))
	->

exists(D,program(D)
         and all(C,(program_halts(C,cons(C,nil))  => program_not_halts(D,cons(C,nil))) and
		   (program_not_halts(C,cons(C,nil)) => outputs(D,cons(C,nil),good)))).

goal exists(B,algorithm_decides_hp(B)).

precedence([algorithm_decides_hp,program_decides_hp,decides_hp,decides,
	outputs_if_halts_on,outputs_if_not_halts_on,outputs,
	program_halts,program_not_halts,out,halts,algorithm,program]).