# Re: Missing theorem

I hope it is unprovable manually as well, since it's false.  See Section 16.1.9 in Specifying Systems.

Yes I see: the semantics doesn't specify if S and << S >> are equal or not.

Thank you.

By the way Z3 accepts

ASSUME NEW S, NEW T \in S
PROVE << T >> \in [ 1..1 -> S ]

But not Isabelle nor CVC3.

--
FL