# [isabelle] termination on higher-oreder recursion function

Dear all:
I meet a problem on termination of a higher-oreder recursion
function as follows:
Despite my efforts of reading the material on function definition
problems in the
doc directory of Isabelle, I still cannot prove the following goals
on the termination of the
function evalf .
Who can help me?
theory bdd imports "Main"
begin
datatype form = Var nat | AndList "form list" | Xnor form form | BNot form
definition xnor :: "bool \<Rightarrow>bool \<Rightarrow> bool" where
"xnor x y \<equiv> (x \<and> y) \<or> ( ~ x \<and>~ y)"
fun evalf :: "(nat \<Rightarrow> bool) \<Rightarrow> form
\<Rightarrow> bool" where
"evalf e (Var i) = e i"
| "evalf e (AndList L) = foldl conj True (map (evalf e) L)"
| "evalf e (Xnor f1 f2) = xnor (evalf e f1) (evalf e f2)"
|"evalf e (BNot f) = (~ (evalf e f)) "
termination proof

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*