LEMMA InnerSym3 ==
ASSUME NEW p, NEW q, NEW r, NEW Op(_,_),
ASSUME NEW u, NEW v
PROVE Op(u,v) \equiv Op(v,u)
PROVE Op(Op(p,q),r) \equiv Op(Op(q,p),r)
<1>1 ASSUME NEW u, NEW v, u \equiv v
PROVE Op(u,r) \equiv Op(v,r)
OBVIOUS
<1> QED BY <1>1
The proof obligation that is generated for step <1>1 is the following:
ASSUME NEW CONSTANT p,
NEW CONSTANT q,
NEW CONSTANT r,
NEW CONSTANT Op(_, _),
ASSUME NEW CONSTANT u,
NEW CONSTANT v
PROVE Op(u, v) <=> Op(v, u) ,
NEW CONSTANT u,
NEW CONSTANT v
PROVE Op(u, r) <=> Op(v, r)
Notice how the assumption that 'u \equiv v' is missing from the obligation. Replacing OBVIOUS by 'BY u \equiv v', now allows TLAPS to prove step <1>1, and the LEMMA because the missing 'u \equiv v' is now added.
LEMMA InnerSym3 ==
ASSUME NEW p, NEW q, NEW r, NEW Op(_,_),
ASSUME NEW u, NEW v
PROVE Op(u,v) \equiv Op(v,u)
PROVE Op(Op(p,q),r) \equiv Op(Op(q,p),r)
<1>1 ASSUME NEW u, NEW v, u \equiv v
PROVE Op(u,r) \equiv Op(v,r)
BY u \equiv v
<1> QED BY <1>1
Is this expected? If so, why? Otherwise, where is the best place to report the bug?
Best regards,
Erick