# Theory FrecR_Arities

```theory FrecR_Arities
imports
FrecR
begin

context
notes FOL_arities[simp]
begin

arity_theorem intermediate for "fst_fm"
lemma arity_fst_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(fst_fm(x,t)) = succ(x) ∪ succ(t)"
using arity_fst_fm'
by auto

arity_theorem intermediate for "snd_fm"
lemma arity_snd_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_fm(x,t)) = succ(x) ∪ succ(t)"
using arity_snd_fm'
by auto

lemma arity_snd_snd_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_snd_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding snd_snd_fm_def hcomp_fm_def
using arity_snd_fm arity_empty_fm union_abs2 pred_Un_distrib
by auto

lemma arity_ftype_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(ftype_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding ftype_fm_def
using arity_fst_fm
by auto

lemma arity_name1_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(name1_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding name1_fm_def hcomp_fm_def
using arity_fst_fm arity_snd_fm union_abs2 pred_Un_distrib
by auto

lemma arity_name2_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(name2_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding name2_fm_def hcomp_fm_def
using arity_fst_fm arity_snd_snd_fm union_abs2 pred_Un_distrib
by auto

lemma arity_cond_of_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(cond_of_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding cond_of_fm_def hcomp_fm_def
using arity_snd_fm arity_snd_snd_fm union_abs2 pred_Un_distrib
by auto

lemma arity_eclose_n1_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n1_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding eclose_n1_fm_def
using arity_is_eclose_fm arity_singleton_fm arity_name1_fm union_abs2 pred_Un_distrib
by auto

lemma arity_eclose_n2_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n2_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding eclose_n2_fm_def
using arity_is_eclose_fm arity_singleton_fm arity_name2_fm union_abs2 pred_Un_distrib
by auto

lemma arity_ecloseN_fm [arity] :
"⟦x∈nat ; t∈nat⟧ ⟹ arity(ecloseN_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding ecloseN_fm_def
using arity_eclose_n1_fm arity_eclose_n2_fm arity_union_fm union_abs2 pred_Un_distrib
by auto

lemma arity_frecR_fm [arity]:
"⟦a∈nat;b∈nat⟧ ⟹ arity(frecR_fm(a,b)) = succ(a) ∪ succ(b)"
unfolding frecR_fm_def
using arity_ftype_fm arity_name1_fm arity_name2_fm arity_domain_fm
arity_empty_fm arity_union_fm pred_Un_distrib arity_succ_fm
by auto

end ― ‹@{thm [source] FOL_arities}›

end```