proposition: Lemma step'_dec s : (exists t, step' s t) \/ not (exists t, step' s t).
proof: Proof. elim: s. - move=> ?. right. by move=> [?] /step'E. - move=> [?|s1 s2|{}s] IHs {}t _. + right. by move=> [?] /step'E []. + have [?|?] := normal_form_dec t; first last. { right. move=> [?] /step'E. tauto. } move: IHs => [[?] IHs|IHs]. * left. eexists. constructor; eassumption. * right. by move=> [?] /step'E [?] /IHs. + have [?|?] := normal_form_dec t; first last. { right. move=> [?] /step'E. tauto. } have [?|?] := normal_form_dec s; first last. { right. move=> [?] /step'E. tauto. } left. eexists. by constructor. - move=> ??. right. by move=> [?] /step'E. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect