[tlaplus] Derivation of SF_vars(A) Strong Fairness

[Chris Ortiz <zitroomega@xxxxxxxxx>]

Hello,

I am trying to get a set of similar form of formulas between WF_vars(A) and SF_vars(A). In Specifying System book there are 3 formulas for WF_vars(A) which were derived by set of tautologies, namely:

Weak Fairness in Specifying System:

1) []([]ENABLED <<A>>_v => <><<A>>_v)         <--- I called always the case imply form

2) []<>(~ENABLED <<A>>_v) \/ []<><<A>>_v   <--- I called disabled OR form

3) <>[](~ENABLED <<A>>_v) => []<><<A>>_v  <-- I called infinitely often action imply form

Strong Fairness in Specifying System:

2) <>[](~ENABLED <<A>>_v) \/ []<><<A>>_v  <-- I called disabled OR form

3) []<>ENABLED <<A>>_v => []<><<A>>_v       <-- I called infinitely often action imply form

I was searching for the "1) I called always the case imply form" of Strong Fairness and I stumble upon Ron Pressler's informative link: https://pron.github.io/posts/tlaplus_part3

Strong Fairness from Ron Pressler's link:

1) []([]<>ENABLED <<A>>_v => <><<A>>_v)   <-- which I called always the case imply form. The one I am searching for.

What I am then trying to do is find the derivation of this 1) with the other 2) and 3) of Strong Fairness by method of tautologies just like in the Specifying System book. I am having a hard time with my logic.

I appreciate if you can help me with the derivation of equivalence for that Strong Fairness formulas.

Thanks,

Zitro

-- 
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/bf96558c-ca17-4bc5-b551-d9b641d1c655n%40googlegroups.com.