Re: [PVS-Help] Non empty finite set induction

[Jerome <jerome@xxxxxxxxxxxxxx>]

Given the previous definition of curry:

>example[R: TYPE, o: FUNCTION[R, R -> R]]: THEORY
>BEGIN
>  ASSUMING
>    comm:  ASSUMPTION commutative?(o)
>    assoc: ASSUMPTION associative?(o)
>  ENDASSUMING
>
>  IMPORTING finite_sets@finite_sets_inductions[posnat]
>
>  myset:   TYPE = ARRAY[posnat -> R]
>  indices: TYPE = non_empty_finite_set[posnat]
>
>  curry(s: myset, K: indices): RECURSIVE R =
>    IF singleton?(K) THEN s(the(K))
>    ELSE s(choose(K)) o curry(s, rest(K))
>    ENDIF
>  MEASURE card(K)
>END example

A subgoal to a lemma I'm trying to prove looks like the following:

   [-1]  singleton?(remove(k!1, U!1))
   [-2]  U!1(k!1)
     |-------
   [1]   empty?[index[N, value]](U!1)
   [2]   singleton?(U!1)
   [3]   s!1(choose(U!1)) o curry(s!1, rest(U!1)) =
	   s!1(k!1) o curry(s!1, remove(k!1, U!1))

The antecedents imply that U!1 has two elements: k!1 and something
else. Given this fact, [3] should be able to be expanded so that the
curry's are removed:

   ...
   [3]   s!1(choose(U!1)) o s!1(k!1) = s!1(k!1) o s!1(the(U!1))

Does anyone know how I can perform these rewrites in PVS? Thanks

jerome