Re: [tlaplus] well-founded induction?

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

> On 27 Apr 2023, at 09:22, David N. Jansen <dnjansen@xxxxxxxxx> wrote:
> 
> 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.

-- 
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/A3FCC1BB-63A8-40C0-A37C-8D6A0AEFC9A3%40gmail.com.