[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] well-founded induction?
- From: "David N. Jansen" <dnjansen@xxxxxxxxx>
- Date: Thu, 27 Apr 2023 07:22:50 +0000
- Accept-language: nl-NL, zh-CN, en-US
- Thread-index: AQHZeNkTS+vRJqNZNkOQDk1qG9gyIQ==
- Thread-topic: well-founded induction?
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)
<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?
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.