[tlaplus] well-founded induction?

["David N. Jansen" <dnjansen@xxxxxxxxx>]

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,
David.


-- 
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.