[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Problem with TLAPM


I'm trying to prove a lemma with TLAPS.But, I get an error message (see the attached picture)
For information, the lemma used a predicate composed of a disjunction of several formulas. When I comment some formulas of this disjunction, TLAPS succeeds to prove the lemma. Otherwise, I have the error message.
Is this due to the size of my predicate?

Thank you,

Attachment: error.PNG
Description: PNG image