renamed LexOrds.thy to Termination.thy; examples for sizechange method
authorkrauss
Sat Dec 27 17:35:00 2008 +0100 (2008-12-27)
changeset 29181cc177742e607
parent 29180 62513d4d34c2
child 29182 9304afad825e
renamed LexOrds.thy to Termination.thy; examples for sizechange method
src/HOL/IsaMakefile
src/HOL/ex/LexOrds.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Termination.thy
     1.1 --- a/src/HOL/IsaMakefile	Sat Dec 27 17:09:27 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Dec 27 17:35:00 2008 +0100
     1.3 @@ -789,14 +789,14 @@
     1.4    ex/Binary.thy ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy	\
     1.5    ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
     1.6    ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
     1.7 -  ex/Lagrange.thy ex/LexOrds.thy ex/LocaleTest2.thy ex/MT.thy		\
     1.8 +  ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy		\
     1.9    ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
    1.10    ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
    1.11    ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML	\
    1.12    ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
    1.13    ex/Reflected_Presburger.thy ex/coopertac.ML				\
    1.14    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.15 -  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy			\
    1.16 +  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy			\
    1.17    ex/Unification.thy ex/document/root.bib			\
    1.18    ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
    1.19    ex/svc_funcs.ML ex/svc_test.thy	\
     2.1 --- a/src/HOL/ex/LexOrds.thy	Sat Dec 27 17:09:27 2008 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,182 +0,0 @@
     2.4 -(* Title:       HOL/ex/LexOrds.thy
     2.5 -   ID:          $Id$
     2.6 -   Author:      Lukas Bulwahn, TU Muenchen
     2.7 -*)
     2.8 -
     2.9 -header {* Examples and regression tests for method lexicographic order. *}
    2.10 - 
    2.11 -theory LexOrds
    2.12 -imports Main
    2.13 -begin
    2.14 -
    2.15 -subsection {* Trivial examples *}
    2.16 -
    2.17 -fun identity :: "nat \<Rightarrow> nat"
    2.18 -where
    2.19 -  "identity n = n"
    2.20 -
    2.21 -fun yaSuc :: "nat \<Rightarrow> nat"
    2.22 -where 
    2.23 -  "yaSuc 0 = 0"
    2.24 -| "yaSuc (Suc n) = Suc (yaSuc n)"
    2.25 -
    2.26 -
    2.27 -subsection {* Examples on natural numbers *}
    2.28 -
    2.29 -fun bin :: "(nat * nat) \<Rightarrow> nat"
    2.30 -where
    2.31 -  "bin (0, 0) = 1"
    2.32 -| "bin (Suc n, 0) = 0"
    2.33 -| "bin (0, Suc m) = 0"
    2.34 -| "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)"
    2.35 -
    2.36 -
    2.37 -fun t :: "(nat * nat) \<Rightarrow> nat"
    2.38 -where
    2.39 -  "t (0,n) = 0"
    2.40 -| "t (n,0) = 0"
    2.41 -| "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" 
    2.42 -
    2.43 -
    2.44 -fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat"
    2.45 -where
    2.46 -  "k ((0,0),(0,0)) = 0"
    2.47 -| "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *)
    2.48 -| "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *)
    2.49 -| "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *)
    2.50 -| "k ((0,0), (0, Suc v)) = k((1,1), (1,v))"   (* v is descending *)
    2.51 -
    2.52 -
    2.53 -fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.54 -where
    2.55 -  "gcd2 x 0 = x"
    2.56 -| "gcd2 0 y = y"
    2.57 -| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
    2.58 -                                    else gcd2 (x - y) (Suc y))"
    2.59 -
    2.60 -fun ack :: "(nat * nat) \<Rightarrow> nat"
    2.61 -where
    2.62 -  "ack (0, m) = Suc m"
    2.63 -| "ack (Suc n, 0) = ack(n, 1)"
    2.64 -| "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))"
    2.65 -
    2.66 -
    2.67 -fun greedy :: "nat * nat * nat * nat * nat => nat"
    2.68 -where
    2.69 -  "greedy (Suc a, Suc b, Suc c, Suc d, Suc e) =
    2.70 -  (if (a < 10) then greedy (Suc a, Suc b, c, d + 2, Suc e) else
    2.71 -  (if (a < 20) then greedy (Suc a, b, Suc c, d, Suc e) else
    2.72 -  (if (a < 30) then greedy (Suc a, b, Suc c, d, Suc e) else
    2.73 -  (if (a < 40) then greedy (Suc a, b, Suc c, d, Suc e) else
    2.74 -  (if (a < 50) then greedy (Suc a, b, Suc c, d, Suc e) else
    2.75 -  (if (a < 60) then greedy (a, Suc b, Suc c, d, Suc e) else
    2.76 -  (if (a < 70) then greedy (a, Suc b, Suc c, d, Suc e) else
    2.77 -  (if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else
    2.78 -  (if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else
    2.79 -  greedy (Suc a, Suc b, Suc c, d, e))))))))))"
    2.80 -| "greedy (a, b, c, d, e) = 0"
    2.81 -
    2.82 -
    2.83 -fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat"
    2.84 -where
    2.85 -  "blowup 0 0 0 0 0 0 0 0 0 = 0"
    2.86 -| "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)"
    2.87 -| "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)"
    2.88 -| "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)"
    2.89 -| "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)"
    2.90 -| "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)"
    2.91 -| "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)"
    2.92 -| "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)"
    2.93 -| "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)"
    2.94 -| "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)"
    2.95 -
    2.96 -  
    2.97 -subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
    2.98 -
    2.99 -datatype tree = Node | Branch tree tree
   2.100 -
   2.101 -fun g_tree :: "tree * tree \<Rightarrow> tree"
   2.102 -where
   2.103 -  "g_tree (Node, Node) = Node"
   2.104 -| "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
   2.105 -| "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
   2.106 -| "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))"
   2.107 -
   2.108 -
   2.109 -fun acklist :: "'a list * 'a list \<Rightarrow> 'a list"
   2.110 -where
   2.111 -  "acklist ([], m) = ((hd m)#m)"
   2.112 -|  "acklist (n#ns, []) = acklist (ns, [n])"
   2.113 -|  "acklist ((n#ns), (m#ms)) = acklist (ns, acklist ((n#ns), ms))"
   2.114 -
   2.115 -
   2.116 -subsection {* Examples with mutual recursion *}
   2.117 -
   2.118 -fun evn od :: "nat \<Rightarrow> bool"
   2.119 -where
   2.120 -  "evn 0 = True"
   2.121 -| "od 0 = False"
   2.122 -| "evn (Suc n) = od (Suc n)"
   2.123 -| "od (Suc n) = evn n"
   2.124 -
   2.125 -
   2.126 -fun sizechange_f :: "'a list => 'a list => 'a list" and
   2.127 -sizechange_g :: "'a list => 'a list => 'a list => 'a list"
   2.128 -where
   2.129 -  "sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)"
   2.130 -| "sizechange_g a b c = sizechange_f a (b @ c)"
   2.131 -
   2.132 -
   2.133 -fun
   2.134 -  prod :: "nat => nat => nat => nat" and
   2.135 -  eprod :: "nat => nat => nat => nat" and
   2.136 -  oprod :: "nat => nat => nat => nat"
   2.137 -where
   2.138 -  "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)"
   2.139 -| "oprod x y z = eprod x (y - 1) (z+x)"
   2.140 -| "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
   2.141 -
   2.142 -
   2.143 -fun
   2.144 -  pedal :: "nat => nat => nat => nat"
   2.145 -and
   2.146 -  coast :: "nat => nat => nat => nat"
   2.147 -where
   2.148 -  "pedal 0 m c = c"
   2.149 -| "pedal n 0 c = c"
   2.150 -| "pedal n m c =
   2.151 -     (if n < m then coast (n - 1) (m - 1) (c + m)
   2.152 -               else pedal (n - 1) m (c + m))"
   2.153 -
   2.154 -| "coast n m c =
   2.155 -     (if n < m then coast n (m - 1) (c + n)
   2.156 -               else pedal n m (c + n))"
   2.157 -
   2.158 -
   2.159 -subsection {*Examples for an unprovable termination *}
   2.160 -
   2.161 -text {* If termination cannot be proven, the tactic gives further information about unprovable subgoals on the arguments *}
   2.162 -
   2.163 -function noterm :: "(nat * nat) \<Rightarrow> nat"
   2.164 -where
   2.165 -  "noterm (a,b) = noterm(b,a)"
   2.166 -by pat_completeness auto
   2.167 -(* termination by apply lexicographic_order*)
   2.168 -
   2.169 -function term_but_no_prove :: "nat * nat \<Rightarrow> nat"
   2.170 -where
   2.171 -  "term_but_no_prove (0,0) = 1"
   2.172 -| "term_but_no_prove (0, Suc b) = 0"
   2.173 -| "term_but_no_prove (Suc a, 0) = 0"
   2.174 -| "term_but_no_prove (Suc a, Suc b) = term_but_no_prove (b, a)"
   2.175 -by pat_completeness auto
   2.176 -(* termination by lexicographic_order *)
   2.177 -
   2.178 -text{* The tactic distinguishes between N = not provable AND F = False *}
   2.179 -function no_proof :: "nat \<Rightarrow> nat"
   2.180 -where
   2.181 -  "no_proof m = no_proof (Suc m)"
   2.182 -by pat_completeness auto
   2.183 -(* termination by lexicographic_order *)
   2.184 -
   2.185 -end
   2.186 \ No newline at end of file
     3.1 --- a/src/HOL/ex/ROOT.ML	Sat Dec 27 17:09:27 2008 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Sat Dec 27 17:35:00 2008 +0100
     3.3 @@ -56,7 +56,7 @@
     3.4    "set",
     3.5    "Meson_Test",
     3.6    "Code_Antiq",
     3.7 -  "LexOrds",
     3.8 +  "Termination",
     3.9    "Coherent"
    3.10  ];
    3.11  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/Termination.thy	Sat Dec 27 17:35:00 2008 +0100
     4.3 @@ -0,0 +1,212 @@
     4.4 +(* Title:       HOL/ex/Termination.thy
     4.5 +   ID:          $Id$
     4.6 +   Author:      Lukas Bulwahn, TU Muenchen
     4.7 +   Author:      Alexander Krauss, TU Muenchen
     4.8 +*)
     4.9 +
    4.10 +header {* Examples and regression tests for automated termination proofs *}
    4.11 + 
    4.12 +theory Termination
    4.13 +imports Main Multiset
    4.14 +begin
    4.15 +
    4.16 +text {*
    4.17 +  The @{text fun} command uses the method @{text lexicographic_order} by default.
    4.18 +*}
    4.19 +
    4.20 +subsection {* Trivial examples *}
    4.21 +
    4.22 +fun identity :: "nat \<Rightarrow> nat"
    4.23 +where
    4.24 +  "identity n = n"
    4.25 +
    4.26 +fun yaSuc :: "nat \<Rightarrow> nat"
    4.27 +where 
    4.28 +  "yaSuc 0 = 0"
    4.29 +| "yaSuc (Suc n) = Suc (yaSuc n)"
    4.30 +
    4.31 +
    4.32 +subsection {* Examples on natural numbers *}
    4.33 +
    4.34 +fun bin :: "(nat * nat) \<Rightarrow> nat"
    4.35 +where
    4.36 +  "bin (0, 0) = 1"
    4.37 +| "bin (Suc n, 0) = 0"
    4.38 +| "bin (0, Suc m) = 0"
    4.39 +| "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)"
    4.40 +
    4.41 +
    4.42 +fun t :: "(nat * nat) \<Rightarrow> nat"
    4.43 +where
    4.44 +  "t (0,n) = 0"
    4.45 +| "t (n,0) = 0"
    4.46 +| "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" 
    4.47 +
    4.48 +
    4.49 +fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat"
    4.50 +where
    4.51 +  "k ((0,0),(0,0)) = 0"
    4.52 +| "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *)
    4.53 +| "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *)
    4.54 +| "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *)
    4.55 +| "k ((0,0), (0, Suc v)) = k((1,1), (1,v))"   (* v is descending *)
    4.56 +
    4.57 +
    4.58 +fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    4.59 +where
    4.60 +  "gcd2 x 0 = x"
    4.61 +| "gcd2 0 y = y"
    4.62 +| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
    4.63 +                                    else gcd2 (x - y) (Suc y))"
    4.64 +
    4.65 +fun ack :: "(nat * nat) \<Rightarrow> nat"
    4.66 +where
    4.67 +  "ack (0, m) = Suc m"
    4.68 +| "ack (Suc n, 0) = ack(n, 1)"
    4.69 +| "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))"
    4.70 +
    4.71 +
    4.72 +fun greedy :: "nat * nat * nat * nat * nat => nat"
    4.73 +where
    4.74 +  "greedy (Suc a, Suc b, Suc c, Suc d, Suc e) =
    4.75 +  (if (a < 10) then greedy (Suc a, Suc b, c, d + 2, Suc e) else
    4.76 +  (if (a < 20) then greedy (Suc a, b, Suc c, d, Suc e) else
    4.77 +  (if (a < 30) then greedy (Suc a, b, Suc c, d, Suc e) else
    4.78 +  (if (a < 40) then greedy (Suc a, b, Suc c, d, Suc e) else
    4.79 +  (if (a < 50) then greedy (Suc a, b, Suc c, d, Suc e) else
    4.80 +  (if (a < 60) then greedy (a, Suc b, Suc c, d, Suc e) else
    4.81 +  (if (a < 70) then greedy (a, Suc b, Suc c, d, Suc e) else
    4.82 +  (if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else
    4.83 +  (if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else
    4.84 +  greedy (Suc a, Suc b, Suc c, d, e))))))))))"
    4.85 +| "greedy (a, b, c, d, e) = 0"
    4.86 +
    4.87 +
    4.88 +fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat"
    4.89 +where
    4.90 +  "blowup 0 0 0 0 0 0 0 0 0 = 0"
    4.91 +| "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)"
    4.92 +| "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)"
    4.93 +| "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)"
    4.94 +| "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)"
    4.95 +| "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)"
    4.96 +| "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)"
    4.97 +| "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)"
    4.98 +| "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)"
    4.99 +| "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)"
   4.100 +
   4.101 +  
   4.102 +subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
   4.103 +
   4.104 +datatype tree = Node | Branch tree tree
   4.105 +
   4.106 +fun g_tree :: "tree * tree \<Rightarrow> tree"
   4.107 +where
   4.108 +  "g_tree (Node, Node) = Node"
   4.109 +| "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
   4.110 +| "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
   4.111 +| "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))"
   4.112 +
   4.113 +
   4.114 +fun acklist :: "'a list * 'a list \<Rightarrow> 'a list"
   4.115 +where
   4.116 +  "acklist ([], m) = ((hd m)#m)"
   4.117 +|  "acklist (n#ns, []) = acklist (ns, [n])"
   4.118 +|  "acklist ((n#ns), (m#ms)) = acklist (ns, acklist ((n#ns), ms))"
   4.119 +
   4.120 +
   4.121 +subsection {* Examples with mutual recursion *}
   4.122 +
   4.123 +fun evn od :: "nat \<Rightarrow> bool"
   4.124 +where
   4.125 +  "evn 0 = True"
   4.126 +| "od 0 = False"
   4.127 +| "evn (Suc n) = od (Suc n)"
   4.128 +| "od (Suc n) = evn n"
   4.129 +
   4.130 +
   4.131 +fun sizechange_f :: "'a list => 'a list => 'a list" and
   4.132 +sizechange_g :: "'a list => 'a list => 'a list => 'a list"
   4.133 +where
   4.134 +  "sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)"
   4.135 +| "sizechange_g a b c = sizechange_f a (b @ c)"
   4.136 +
   4.137 +fun
   4.138 +  pedal :: "nat => nat => nat => nat"
   4.139 +and
   4.140 +  coast :: "nat => nat => nat => nat"
   4.141 +where
   4.142 +  "pedal 0 m c = c"
   4.143 +| "pedal n 0 c = c"
   4.144 +| "pedal n m c =
   4.145 +     (if n < m then coast (n - 1) (m - 1) (c + m)
   4.146 +               else pedal (n - 1) m (c + m))"
   4.147 +
   4.148 +| "coast n m c =
   4.149 +     (if n < m then coast n (m - 1) (c + n)
   4.150 +               else pedal n m (c + n))"
   4.151 +
   4.152 +
   4.153 +
   4.154 +subsection {* Refined analysis: The @{text sizechange} method *}
   4.155 +
   4.156 +text {* Unsolvable for @{text lexicographic_order} *}
   4.157 +
   4.158 +function fun1 :: "nat * nat \<Rightarrow> nat"
   4.159 +where
   4.160 +  "fun1 (0,0) = 1"
   4.161 +| "fun1 (0, Suc b) = 0"
   4.162 +| "fun1 (Suc a, 0) = 0"
   4.163 +| "fun1 (Suc a, Suc b) = fun1 (b, a)"
   4.164 +by pat_completeness auto
   4.165 +termination by sizechange
   4.166 +
   4.167 +
   4.168 +text {* 
   4.169 +  @{text lexicographic_order} can do the following, but it is much slower. 
   4.170 +*}
   4.171 +
   4.172 +function
   4.173 +  prod :: "nat => nat => nat => nat" and
   4.174 +  eprod :: "nat => nat => nat => nat" and
   4.175 +  oprod :: "nat => nat => nat => nat"
   4.176 +where
   4.177 +  "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)"
   4.178 +| "oprod x y z = eprod x (y - 1) (z+x)"
   4.179 +| "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
   4.180 +by pat_completeness auto
   4.181 +termination by sizechange
   4.182 +
   4.183 +text {* 
   4.184 +  Permutations of arguments:
   4.185 +*}
   4.186 +
   4.187 +function perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   4.188 +where
   4.189 +  "perm m n r = (if r > 0 then perm m (r - 1) n
   4.190 +                  else if n > 0 then perm r (n - 1) m
   4.191 +                  else m)"
   4.192 +by auto
   4.193 +termination by sizechange
   4.194 +
   4.195 +text {*
   4.196 +  Artificial examples and regression tests:
   4.197 +*}
   4.198 +
   4.199 +function
   4.200 +  fun2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   4.201 +where
   4.202 +  "fun2 x y z =
   4.203 +      (if x > 1000 \<and> z > 0 then
   4.204 +           fun2 (min x y) y (z - 1)
   4.205 +       else if y > 0 \<and> x > 100 then
   4.206 +           fun2 x (y - 1) (2 * z)
   4.207 +       else if z > 0 then
   4.208 +           fun2 (min y (z - 1)) x x
   4.209 +       else
   4.210 +           0
   4.211 +      )"
   4.212 +by pat_completeness auto
   4.213 +termination by sizechange -- {* requires Multiset *}
   4.214 +
   4.215 +end