```> Resent-Date: Wed, 19 Nov 1997 09:19:30 -0800 (PST)
> Date: Wed, 19 Nov 1997 18:19:03 +0100
> From: Matteo Vaccari <vaccari@dsi.unimi.it>
> Organization: University of Milano Comp. Sci. Dept.
> Resent-From: pvs-help@csl.sri.com
> X-Mailing-List: <pvs-help@csl.sri.com> archive/latest/84
> X-Loop: pvs-help@csl.sri.com
> Precedence: list
>
> Why is it that the extensionality axiom is an implication and not an
> equivalence?
>
> I have a simple tree datatype:
>
> tree[t:TYPE+] : DATATYPE
>   BEGIN
>     scalar (scalar: t): scalar?
>     pair   (left: tree, right: tree): pair?
>   END tree
>
> among the automatically generated axioms I have
>
>   tree_pair_extensionality: AXIOM
>         (FORALL (pair?_var: (pair?), pair?_var2: (pair?)):
>            left(pair?_var) = left(pair?_var2)
>                AND right(pair?_var) = right(pair?_var2)
>                IMPLIES pair?_var = pair?_var2);
>
> but I'd like to be able to prove the reverse implication, for instance
>
>   pair(a,b) = pair(c,d) IMPLIES a=c AND b=d
>
> Am I missing something obvious?
>
>
> 	Matteo
>
>

I had the same problem with cons before pvs-help was set up.
Something along these lines should work (I haven't tested it).

(""
(SKOSIMP*)
(CASE "left(pair(a!1, b!1)) = left(pair(c!1, d!1))"
"right(pair(a!1, b!1)) = right(pair(c!1, d!1))")
(("1" (ASSERT)) ("2" (REPLACE*)) ("3" (REPLACE*))))

--
Paul Loewenstein          Sun Microsystems Inc., Mailstop UMPK12-302
Staff Engineer            901 San Antonio Road, Palo Alto, California 94303
Tel: 650-786-6015  FAX: 650-568-9603
paul.loewenstein@eng.sun.com

```

• References: