proposition: Lemma negator_loop: forall d n, Decider d -> CodeOf (negator d) n -> ~ Loop (Call n [[n]]).
proof: Proof. unfold negator. intros d n cp cn N. run_simpl_all. inversion_clear N. - apply decider_to_not_loop in H; auto. - destruct b; auto; inversion_clear H0. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed