seq package:sbv

A sequence of statements.

Sequence operations. Indexed by the element kind.

Are the two given floats exactly the same. That is, NaN will compare equal to itself, +0 will not compare equal to -0 etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==.)

Less than or equal to.

Check that two floats are the exact same values, i.e., +0/-0 does not compare equal, and NaN's compare equal to themselves.

A sequence is valid upto a bound if it starts at Idle, and follows the mutex rules. That is:

• From Idle it can switch to Ready or stay Idle
• From Ready it can switch to Critical if it's its turn
• From Critical it can either stay in Critical or go back to Idle

The variable me identifies the agent id.

Prove that the sequence 1, 3, S_{k-2} + 2 S_{k-1} is always odd. We have:

>>> oddSequence1
Inductive lemma (strong): oddSequence1
Step: Measure is non-negative         Q.E.D.
Step: 1 (3 way case split)
Step: 1.1                           Q.E.D.
Step: 1.2                           Q.E.D.
Step: 1.3.1                         Q.E.D.
Step: 1.3.2                         Q.E.D.
Step: 1.3.3                         Q.E.D.
Step: 1.Completeness                Q.E.D.
Result:                               Q.E.D.
[Proven] oddSequence1 :: Ɐn ∷ Integer → Bool

Prove that the sequence 1, 3, 2 S_{k-1} - S_{k-2} generates sequence of odd numbers. We have:

>>> oddSequence2
Lemma: oddSequence_0                              Q.E.D.
Lemma: oddSequence_1                              Q.E.D.
Inductive lemma (strong): oddSequence_sNp2
Step: Measure is non-negative                   Q.E.D.
Step: 1                                         Q.E.D.
Step: 2                                         Q.E.D.
Step: 3 (simplify)                              Q.E.D.
Step: 4                                         Q.E.D.
Step: 5 (simplify)                              Q.E.D.
Step: 6                                         Q.E.D.
Result:                                         Q.E.D.
Lemma: oddSequence2
Step: 1 (3 way case split)
Step: 1.1                                     Q.E.D.
Step: 1.2                                     Q.E.D.
Step: 1.3.1                                   Q.E.D.
Step: 1.3.2                                   Q.E.D.
Step: 1.Completeness                          Q.E.D.
Result:                                         Q.E.D.
[Proven] oddSequence2 :: Ɐn ∷ Integer → Bool