This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| rely | ⊦ rely(n, m, n', m') ↔ ¬ ¬(m' = m ∧ n' ≤ n ∧ (n ≤ m → n' = n)) | An Axiom |
| inv | ⊦ inv(n0, m0, n, m) ↔ gcd(n0, m0) = gcd(n, m) | An Axiom |
| gcd-loop-partial | inv(n, m, N, M) ⊦ [: N, M | rely(N', M', N'', M''), rely(M, N, M', N'), inv(n, m, N, M), GCD_loop(; N, M)] (N = M ∧ N = gcd(n, m)) | A User Theorem |
| gcd-partial | n = N, m = M ⊦ [: N, M | (N' = N'' ∧ M' = M''), true, true, GCD(; N, M)] (N = M ∧ N = gcd(n, m)) | A User Theorem |