theory FunTerm imports Main begin

function tst1 :: "nat \<Rightarrow> nat"
     and tst2 :: "nat \<Rightarrow> nat"
where
  "tst1 n = (tst2 n) + 1"
| "tst2 n = n + 1"
 by pat_completeness auto


fun tstMeasure :: "nat + nat => nat" where
  "tstMeasure n =
    (case n of Inl n1 \<Rightarrow> 1
             | Inr n2 \<Rightarrow> 0
    )"

termination tst1
 apply(relation "measure tstMeasure")
 apply(auto)
done

function tst1' :: "nat \<Rightarrow> nat"
     and tst2' :: "nat \<Rightarrow> nat"
     and tst3' :: "nat \<Rightarrow> nat" 
where
  "tst1' n = (tst2' n) + 1"
| "tst2' n = (tst3' n) + 1"
| "tst3' n = n + 1"
 by pat_completeness auto

fun tstMeasure' :: "nat + nat + nat => nat" where
  "tstMeasure' n =
    (case n of Inl n1 \<Rightarrow> 2
             | Inr n1 \<Rightarrow> (case n1 of Inl n2 \<Rightarrow> 1
                                   | Inr n2 \<Rightarrow> 0
                         )
    )"

termination tst1'
 apply(relation "measure tstMeasure'")
 apply(auto)
done

function t1 :: "nat \<Rightarrow> nat"
     and t2 :: "nat \<Rightarrow> nat"
     and t3 :: "nat \<Rightarrow> nat" 
     and t4 :: "nat \<Rightarrow> nat" 
where
  "t1 n = (t2 n) + 1"
| "t2 n = (t3 n) + 1"
| "t3 n = (t4 n) + 1"
| "t4 n = n + 1"
by pat_completeness auto

fun tMeasure :: "nat + nat + nat + nat \<Rightarrow> nat" 
where
  "tMeasure v = (case v of Inl x \<Rightarrow> 3
                         | Inr x \<Rightarrow> (case x of Inl y \<Rightarrow> 2
                                             | Inr y \<Rightarrow> (case y of Inl z \<Rightarrow> 1
                                                                 | Inr z \<Rightarrow> 0
                                                        )
                                    )
                )"

termination t1
 apply(relation "measure tMeasure")

end