# Re: "<<" TCC ?

```Hi,

After typecheckeing I've got TCC which is unprovable. Could you hint
me: what do I wrong ?

typechecks and proved all TCC's (see appended dump).

Bye,

Hendrik

```
```
%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
\$\$\$t.pvs
gen_tree[T: TYPE]: DATATYPE
BEGIN

leaf(fringe: list[T]): isLeaf?
node(val: T, desc: list[gen_tree]): isNode?

END gen_tree

T : Theory
Begin
IMPORTING gen_tree

sum(ls: list[nat]): RECURSIVE nat =
CASES ls OF
null: 0,
cons(x, ls1): x + sum(ls1)
ENDCASES
MEASURE ls BY <<

%size function
size(tr : gen_tree[nat]): RECURSIVE nat =
CASEs tr OF
leaf(tr): length(tr),
node(val,desc): 1 + sum(map(size ,desc))
ENDCASES
MEASURE tr BY <<
end T

\$\$\$t.prf
(gen_tree)
(T
(sum_TCC1 0
(sum_TCC1-1 nil 3262925471 3262925471 ("" (termination-tcc) nil nil)
180 nil shostak))
(size_TCC1 0
(size_TCC1-1 nil 3262925471 3262928168
("" (skosimp*)
((""
(case "Forall(l1,l2 : list[gen_tree[nat]]) : tr!1 = node(val!1, append(l1,l2)) IMPLIES every[gen_tree[nat]] (LAMBDA (z: gen_tree[nat]): <<[nat](z, tr!1))(l2)")
(("1" (inst -1 "null" "desc!1")
(("1" (expand "append") (("1" (assert) nil nil)) nil)) nil)
("2" (hide-all-but 1)
(("2" (induct "l2")
(("1" (grind) nil nil)
("2" (skosimp*)
(("2" (expand "every" 1)
(("2" (prop)
(("1" (replace -2 * lr)
(("1" (hide -1 -2)
(("1" (expand "<<")
(("1" (generalize "cons1_var!1" "t")
(("1" (generalize "cons2_var!1" "l2")
(("1" (generalize "l1!1" "l1")
(("1" (induct "l1")
(("1" (grind) nil nil)
("2"
(skosimp*)
(("2"
(expand "append" 1)
(("2"
(expand "some" 1)
(("2" (rewrite -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst -1 "append(l1!1, cons(cons1_var!1, null))")
(("2" (prop)
(("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("1" (decompose-equality) nil nil)
("2" (replace -1 * lr)
(("2" (assert)
(("2" (hide -1)
(("2"
(generalize "cons1_var!1" "t")
(("2"
(generalize "cons2_var!1" "l2")
(("2"
(generalize "l1!1" "l1")
(("2"
(induct "l1")
(("1"
(expand "append")
(("1"
(expand "append")
(("1" (propax) nil nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand "append" 1)
(("2" (rewrite -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(append def-decl "list[T]" list_props nil)
(node adt-constructor-decl "[[T, list[gen_tree]] -> (isNode?)]"
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)