Require Undecidability.L.L.
Import L (term, var, app, lam).

Require Undecidability.LambdaCalculus.Lambda.
Import Lambda (closed).

Inductive eterm := closure : list eterm -> term -> eterm.

Inductive halt_cbn : list eterm -> list eterm -> term -> Prop :=
  | halt_var_0 ts ctx t ctx' :
      halt_cbn ts ctx t ->
      halt_cbn ts ((closure ctx t)::ctx') (var 0)
  | halt_var_S ts ctx n t :
      halt_cbn ts ctx (var n) ->
      halt_cbn ts (t::ctx) (var (S n))
  | halt_app ts ctx s t :
      halt_cbn ((closure ctx t)::ts) ctx s ->
      halt_cbn ts ctx (app s t)
  | halt_lam_ts t ts ctx s :
      halt_cbn ts (t::ctx) s ->
      halt_cbn (t::ts) ctx (lam s)
  | halt_lam ctx s :
      halt_cbn nil ctx (lam s).

Definition KrivineM_HALT : term -> Prop :=
  fun t => halt_cbn nil nil t.

Definition KrivineMclosed_HALT : { t : term | closed t } -> Prop :=
  fun '(exist _ t _) => KrivineM_HALT t.