Awesome.
Yeah. The reason why I sent to our group is: I am not confident enough about my understanding about WF and SF and feel that maybe more EYES can discuss it.
Sometimes, WF and SF relation indeed a bit confusing. I feel it is from the word of "weak" and "strong"
Below is my explanation:
Weak Fairness: Need STRONG condition --ALWAYS ENABLED
Strong Fairness: Need Weak condition. --ONLY infinitely many ENABLED.
Hence, if SF(A) is TRUE, then, surely, WF(A) shall be TRUE.
Then, SF(A)--->WF(A) is TRUE.