[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: help discharging a TCC*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Wed, 9 Jun 1999 10:30:02 -0400 (EDT)

I want to discharge a TCC generated by the following declaration: elements(a: finseq): finite_set[T] = {x: T | exists (n: nat): n < length(a) and seq(a)(n) = x} The function, elements, takes a finite_sequence and returns the set of components of the sequence. The TCC generated requires me to show that for any finite sequence, the set of its components is a finite set (required since I have "finite_set[T]" as the range for the elements function): elements_TCC1: OBLIGATION (FORALL (a: finseq[T]): is_finite[T]({x: T | EXISTS (n: nat): n < length(a) AND seq(a)(n) = x})); If you apply (grind) right off you get a subgoal to show that there is an injective function, f, on the component set of the sequence that maps its elements of the naturals less than some N. I've tried doing this by supplying "length(a)" for the N and various functions for f, but have not succeeded. I need some help figuring out a way to prove this. Anyone have some time to give me some pointers? Mark Aronszajn Reusable Software Research Group Department of Computer Science & Electrical Engineering West Virginia University

- Prev by Date:
**pvs specification on information systems** - Next by Date:
**Re: help discharging a TCC** - Prev by thread:
**trigonometry** - Next by thread:
**Re: help discharging a TCC** - Index(es):