# Library CoLoR.Term.WithArity.ASubterm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sidi Ould-Biha, 2010-04-27
Properties of the subterm relation.

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (vector term).

list of immediate subterms

Fixpoint subterm_lst t :=
match t with
| Var _ => nil
| Fun f ts =>
let fix subterm_lst_vec k (us : terms k) {struct us} : list term :=
match us with
| Vnil => nil
| Vcons u1 us' => subterm_lst u1 ++ subterm_lst_vec _ us'
end
in list_of_vec ts ++ subterm_lst_vec (arity f) ts
end.

Fixpoint subterm_lst_vec k (us : terms k) : list term :=
match us with
| Vnil => nil
| Vcons u1 us' => subterm_lst u1 ++ subterm_lst_vec us'
end.

Lemma subterm_lst_fun : forall F ts,
subterm_lst (Fun F ts) = list_of_vec ts ++ subterm_lst_vec ts.

list of immediate subterms

Lemma In_subterm_lst_vec_elim : forall v n (ts : terms n),
In v (subterm_lst_vec ts) ->
exists i, exists p : i < n, In v (subterm_lst (Vnth ts p)).

Lemma In_subterm_lst_vec_intro : forall n (ts : terms n) v i (p : i < n),
In v (subterm_lst (Vnth ts p)) -> In v (subterm_lst_vec ts).

the supterm relation is finitely branching

Notation supterm := (@supterm Sig).

Lemma fin_branch_supterm : finitely_branching supterm.

End S.