A proof rule for fair termination of guarded commands

We present a proof rule for fairly terminating guarded commands based on a well-foundedness argument. The rule is applied to several examples, and proved to be sound and (semantically) complete w.r.t. an operational semantics of computation trees. The rule is related to another rule suggested by Lehmann, Pnueli, and Stavi (in “Proc. Internat. Colloq. Automata Lang. and Programming, '81,” Acre, July 1981), by showing that the (semantic) completeness of the LPS-rule follows from the completeness or ours