well-founded induction?

[David N. Jansen]

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.

[Stephan Merz]

These proofs tend to be very brittle. You might try abstracting Block(s, blocks) like so

<2>. DEFINE B == Block(s, blocks)
<2>1. B \subseteq States
(* similarly replace Block(s, blocks) by B in <2>2, <2>3 *)
<2>. HIDE DEF B
<2>4. \A x \in B : HasBranchingTransitionInSplitter(x)

If that doesn't work, could you share (perhaps privately) the module?

Stephan

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88DED3AC-04B2-423A-A534-453826B513FB%40ios.ac.cn.