[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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.
By the way Z3 accepts
ASSUME NEW S, NEW T \in S
PROVE << T >> \in [ 1..1 -> S ]
But not Isabelle nor CVC3.