(* generated by Ott 0.10.14 from: ../tests/test10.ott *) Require Import Arith. Require Import Bool. Require Import List. (** syntax *) Definition termvar := nat. Lemma eq_termvar: forall (x y : termvar), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_termvar : ott_coq_equality. Inductive t : Set := t_Var : termvar -> t | t_Lam : termvar -> t -> t | t_App : t -> t -> t . (** library functions *) Fixpoint list_mem (A:Set) (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list A) {struct l} : bool := match l with | nil => false | cons h t => if eq h x then true else list_mem A eq x t end. Implicit Arguments list_mem. (** subrules *) Definition is_v_of_t (t_6:t) : Prop := match t_6 with | (t_Var x) => False | (t_Lam x t5) => (True) | (t_App t5 t') => False end. (** substitutions *) Fixpoint tsubst_t (t_6:t) (x5:termvar) (t__7:t) {struct t__7} : t := match t__7 with | (t_Var x) => (if eq_termvar x x5 then t_6 else (t_Var x)) | (t_Lam x t5) => t_Lam x (if list_mem eq_termvar x5 (cons x nil) then t5 else (tsubst_t t_6 x5 t5)) | (t_App t5 t') => t_App (tsubst_t t_6 x5 t5) (tsubst_t t_6 x5 t') end. (** definitions *) (* defns Jop *) Inductive (* defn reduce *) reduce : t -> t -> Prop := | ax_app : forall (x:termvar) (t12:t) (v2:t), is_v_of_t v2 -> reduce (t_App (t_Lam x t12) v2) (tsubst_t v2 x t12 ) | ctx_app_fun : forall (t1:t) (t_5:t) (t1':t), reduce t1 t1' -> reduce (t_App t1 t_5) (t_App t1' t_5) | ctx_app_arg : forall (v5:t) (t1:t) (t1':t), is_v_of_t v5 -> reduce t1 t1' -> reduce (t_App v5 t1) (t_App v5 t1') .