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

[tlaplus] well-founded induction?

Dear all,

I am trying to apply WFInduction to prove the property below. However, I cannot get TLAPS to succeed with any of the solvers.

LEMMA Red_states_have_a_branching_transition_in_splitter == ...
    <2>1. Block(s, blocks) \subseteq States                               BY DEF Block
    <2>2. IsWellFoundedOn(tau_reversed_Transitions, Block(s, blocks))     BY <2>1, IsWellFoundedOnSubset, TransitionsBasic
    <2>3. ASSUME NEW x \in Block(s, blocks),
                 \A y \in SetLessThan(x, tau_reversed_Transitions, Block(s, blocks)) : HasBranchingTransitionInSplitter(y)
          PROVE  HasBranchingTransitionInSplitter(x)
    <2>4. \A x \in Block(s, blocks): HasBranchingTransitionInSplitter(x)  BY ONLY <2>2, <2>3, WFInduction

Do you know what I can try to change it?
Or is it that I need to (re)install something, as I have recently changed to a new laptop?

Kind regards,

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88DED3AC-04B2-423A-A534-453826B513FB%40ios.ac.cn.