<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* 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')

.