# Re: [PVS-Help] choose problem

```Dear Song,

[NB: the declarations you've included in your mail contain a few
mistakes; I've tried to mend these in the PVS theory attached to this
mail. The following is relative to that theory which might differ from
yours.]

> <<(env1:VarEnv,env2:VarEnv): bool= FORALL (x:Vars): env1(x)=env2(x)
>
> c(f,g): trans =
>   LAMBDA (s: Env): choose({y: VarEnv|y<<f(s) or y<<g(s)})
>
> how can I to proof the nonemptyness of {y: VarEnv|y<<f(s) or y<<g(s)}?

You need to find a "y" such that "y << f(s)" or "y << g(s)". Since
"<<" essentially denotes equality on environments, you can pick, e.g.,
"f(s)" for "y".

A step-by-step proof of the TCC would be

(skosimp*)
(expand "nonempty?")
(expand "empty?")
(expand "member")
(inst -1 "f!1(s!1)")
(flatten)
(expand "<<")

a more automatic version would use (grind :if-match best).

>   |-------
> {1}   choose({y: VarEnv | y << f!1(Init_env) OR y << g!1(Init_env)}) =
>        choose({y: VarEnv | y << g!1(Init_env) OR y << f!1(Init_env)}
>
> then I do not know how to proof this issue

Since "OR" is commutative, the two sets are equal. To tell PVS that
you know this, use the command "case-replace". In a subsequent step
you need to show that the sets are indeed equal; you need the command
"apply-extensionality" to do this. A complete step-by-step proof is as
follows:

(skosimp*)
(expand "c")
(case-replace
"{y: Env | y << f!1(init_env) OR y << g!1(init_env)} = {y: Env | y <<
g!1(init_env) OR y << f!1(init_env)}")
(apply-extensionality :hide? t)
(iff)
(ground)

Regards,

- Holger

```
```song : THEORY

BEGIN

Vars  : TYPE
Value : TYPE+

% Env   : TYPE = [Env->Value]  % mistake:  Env also occurs on right-hand side

Env   : TYPE = [Vars -> Value]
trans : TYPE = [Env  -> Env]

f,g   : VAR trans

% <<(env1:VarEnv,env2:VarEnv): bool =   % VarEnv not declared, should be Env?
%  FORALL (x:Vars): env1(x)=env2(x)

<<(env1:Env,env2:Env): bool =
FORALL (x:Vars): env1(x)=env2(x)

c(f,g): trans =
LAMBDA (s: Env): choose({y: Env | y<<f(s) OR y<<g(s)})

init_env : Env

% Existence TCC  for  init_env: Env
% init_env_TCC1: OBLIGATION EXISTS (x: Env): TRUE;
%
% Solution: type Value must be non-empty: Value : TYPE+

L1 : LEMMA
FORALL (f, g: trans):
c(f, g)(init_env) = c(g, f)(init_env)

END song
```