Event: Start with the library "naturals".

;;; Several Useful Theorems

Theorem: equal-iff ((truep (a) ∨ falsep (a)) ∧ (truep (b) ∨ falsep (b))) → ((a = b) = (a ↔ b))

Event: Disable equal-iff.

Definition: length (list) = if listp (list) then 1 + length (cdr (list))

else 0 endif

Definition: nth (list, n) = if n ≃ 0 then car (list)

else nth (cdr (list), n − 1) endif

Definition: position (prg, e) = if listp (prg)

then if car (prg) = e then 0

else 1 + position (cdr (prg), e) endif else 0 endif

Theorem: nth-member (n < length (list)) → (nth (list, n) ∈ list)

Theorem: listp-not-zero-length (length (list) = 0) = (¬ listp (list))

Theorem: position-zero (e ∉ prg) → (position (prg, e) = length (prg))

Theorem: position-lessp (e ∈ prg) → (position (prg, e) < length (prg))

Theorem: nth-position nth (prg, position (prg, e)) = if e ∈ prg then e

else 0 endif Theorem: position-nth ((e ∈ list) ∧ (nth (list, n) ≠ e)) → ((position (list, e) = n) = f)

Theorem: member-append (e ∈ append (j , k)) = ((e ∈ j ) ∨ (e ∈ k))

Theorem: append-is-associative append (append (x, y), z) = append (x, append (y, z))

;;; The Witness function for the Computation

Definition: mchoose (prg, i) = nth (prg, i mod length (prg))

Definition: mnext (prg, e, i) = (i + if position (prg, e) < (i mod length (prg))

then position (prg, e)

+ (length (prg) − (i mod length (prg))) else position (prg, e) − (i mod length (prg)) endif)

Theorem: mnext-fixes ((e ∈ prg) ∧ (i ∉ N)) → (mnext (prg, e, i) = mnext (prg, e, 0))

Theorem: numberp-mnext (e ∈ prg) → (mnext (prg, e, i) ∈ N)

Theorem: mchoose-chooses listp (prg) → (mchoose (prg, i) ∈ prg)

Theorem: mchoose-fixes (listp (prg) ∧ (i ∉ N)) → (mchoose (prg, i) = mchoose (prg, 0))

Theorem: mnext-choice-1 (e ∈ prg) → (mnext (prg, e, i) ≮ i)

Theorem: mnext-choice-2-simplified (e < n) → (((i + if e < (i mod n) then e + (n − (i mod n))

else e − (i mod n) endif) mod n) = fix (e))

Theorem: mnext-choice-2 (e ∈ prg) → (mchoose (prg, mnext (prg, e, i)) = e)

Theorem: remainder-of-add1 ((x < (a mod b)) ∧ (x < ((1 + a) mod b))) → (((1 + a) mod b) = (1 + (a mod b)))

Theorem: remainder-of-add1-1 ((x ≮ (a mod b)) ∧ (x < ((1 + a) mod b))) → ((a mod b) = fix (x))

Theorem: remainder-of-add1-2 ((x < (a mod b)) ∧ (x ≮ ((1 + a) mod b))) → ((((1 + a) mod b) = 0) ∧ ((a mod b) = (b − 1)))

Theorem: remainder-of-add1-3 ((x ≮ (a mod b)) ∧ (x < b) ∧ (x ∈ N) ∧ (x ≠ (a mod b)) ∧ (x ≮ ((1 + a) mod b))) → (((1 + a) mod b) = (1 + (a mod b)))

Theorem: remainder-of-add1-3-1 ((position (prg, e) ≮ (i mod length (prg))) ∧ (position (prg, e) ≮ ((1 + i) mod length (prg))) ∧ (nth (prg, i mod length (prg)) ≠ e) ∧ (e ∈ prg)) → (((1 + i) mod length (prg)) = (1 + (i mod length (prg))))

Event: Disable mchoose.

Event: Disable mnext.

;;; The Statement Interpreter

Definition: n (old, new, e) = apply$ (car (e), append (list (old, new), cdr (e)))

Definition: exists-successor (old, e) ↔ ∃ new n (old, new, e)

Theorem: exists-successor-implies exists-successor (old, e) → n (old, newx (e, old), e)

Theorem: prove-exists-successor n (old, new, e) → exists-successor (old, e)

Event: Disable exists-successor.

Definition: ms (prg, i) = if i ≃ 0 then nil

elseif n (ms (prg, i − 1), newx (mchoose (prg, i − 1), ms (prg, i − 1)), mchoose (prg, i − 1))

then newx (mchoose (prg, i − 1), ms (prg, i − 1))

else ms (prg, i − 1) endif

Theorem: ms-transition-successful (listp (prg) ∧ n (ms (prg, i), new, mchoose (prg, i))) → n (ms (prg, i), ms (prg, 1 + i), mchoose (prg, i))

Theorem: ms-transition-idle (listp (prg) ∧ (¬ n (ms (prg, i), newx (mchoose (prg, i), ms (prg, i)), mchoose (prg, i)))) → (ms (prg, 1 + i) = ms (prg, i))

;;; Characterizing an Arbitrary Computation

Conservative Axiom: computation (listp (prg) → (choose (prg, i) ∈ prg)) ∧ ((e ∈ prg) → (next (prg, e, i) ≮ i)) ∧ ((e ∈ prg) → (choose (prg, next (prg, e, i)) = e)) ∧ ((listp (prg) ∧ n (s (prg, i), new, choose (prg, i)))

→ n (s (prg, i), s (prg, 1 + i), choose (prg, i))) ∧ ((listp (prg)

∧ (¬ n (s (prg, i), newx (choose (prg, i), s (prg, i)), choose (prg, i)))) → (s (prg, 1 + i) = s (prg, i)))

∧ ((e ∈ prg) → (next (prg, e, i) ∈ N)) ∧ ((listp (prg) ∧ (i ∉ N)) → (s (prg, i) = s (prg, 0))) ∧ ((listp (prg) ∧ (i ∉ N)) → (choose (prg, i) = choose (prg, 0))) ∧ (((e ∈ prg) ∧ (i ∉ N)) → (next (prg, e, i) = next (prg, e, 0)))

Simultaneously, we introduce the new function symbols choose, next, and s. Event: Disable mnext-fixes.

Event: Disable numberp-mnext.

Event: Disable mchoose-chooses.

Event: Disable mchoose-fixes.

Event: Disable mnext-choice-1. Event: Disable mnext-choice-2-simplified. Event: Disable mnext-choice-2. Event: Disable remainder-of-add1. Event: Disable remainder-of-add1-1. Event: Disable remainder-of-add1-2. Event: Disable remainder-of-add1-3. Event: Disable remainder-of-add1-3-1. Event: Disable exists-successor-implies. Event: Disable prove-exists-successor. Event: Disable ms-transition-successful. Event: Disable ms-transition-idle. Event: Disable n.

;;; The Predicate Interpreter

Definition: eval (pred, state) = eval$ (t, pred, list (cons ('state, state))) Theorem: eval-not eval (list ('not, p), state) = (¬ eval (p, state)) Theorem: eval-and eval (list ('and, p, q), state) = (eval (p, state) ∧ eval (q, state))

Theorem: eval-or eval (list ('or, p, q), state) = (eval (p, state) ∨ eval (q, state))

Theorem: eval-implies eval (list ('implies, p, q), state) = (eval (p, state) → eval (q, state))

Theorem: eval-iff eval (list ('iff, p, q), state) = (eval (p, state) ↔ eval (q, state))

Theorem: eval-equal eval (list ('equal, p, q), state) = (eval (p, state) = eval (q, state))

Theorem: eval-true eval ('(true), state) = t

Theorem: eval-false eval ('(false), state) = f

Event: Disable eval.

;;; The Stability Operator:  Unless

Definition: unless (p, q, prg) ↔ ∀ old, new, e (((e ∈ prg)

∧ (n (old, new, e)

∧ eval (list ('and, p, list ('not, q)), old))) → eval (list ('or, p, q), new))

Event: Disable unless.

Theorem: prove-unless (((eu (p, prg, q) ∈ prg) ∧ n (oldu (p, prg, q), newu (p, prg, q), eu (p, prg, q)) ∧ eval (p, oldu (p, prg, q)) ∧ (¬ eval (q, oldu (p, prg, q)))) → (eval (p, newu (p, prg, q)) ∨ eval (q, newu (p, prg, q)))) → unless (p, q, prg)

Theorem: unless-implies (unless (p, q, prg) ∧ (e ∈ prg) ∧ n (old, new, e) ∧ eval (p, old) ∧ (¬ eval (q, old))) → eval (list ('or, p, q), new)

Event: Disable prove-unless.

Event: Disable unless-implies.

;;; The Progress Operator:  Leads-To

Definition: leads-to (p, q, prg) ↔ ∀ i (eval (p, s (prg, i)) → ∃ j ((j ≮ i) ∧ eval (q, s (prg, j ))))

Event: Disable leads-to.

Theorem: prove-leads-to (eval (p, s (prg, ileads (p, prg, q))) → ((j ≮ ileads (p, prg, q)) ∧ eval (q, s (prg, j )))) → leads-to (p, q, prg)

Theorem: leads-to-implies (leads-to (p, q, prg) ∧ eval (p, s (prg, i))) → ((jleads (i, prg, q) ≮ i) ∧ eval (q, s (prg, jleads (i, prg, q))))

Event: Disable prove-leads-to.

Event: Disable leads-to-implies.

;;; The Most Effective Trace

Definition: schedulable (prg) ↔ ∀ i ∃ new n (s (prg, i), new, choose (prg, i))

Event: Disable schedulable.

Theorem: prove-schedulable n (s (prg, is (prg)), new, choose (prg, is (prg))) → schedulable (prg)

Theorem: schedulable-implies schedulable (prg) → n (s (prg, i), news (i, prg), choose (prg, i))

Event: Disable prove-schedulable.

Event: Disable schedulable-implies.

Theorem: schedulable-implies-effective-computation (schedulable (prg) ∧ listp (prg)) → n (s (prg, i), s (prg, 1 + i), choose (prg, i))

Theorem: computation-n (schedulable (prg) ∧ (e ∈ prg)) → n (s (prg, next (prg, e, i)), s (prg, 1 + next (prg, e, i)), e)

Theorem: effective-idle listp (prg) → ((s (prg, 1 + i) = s (prg, i))

∨ n (s (prg, i), s (prg, 1 + i), choose (prg, i)))

Event: Disable effective-idle.

;;; Leads-To Proof Rules

Theorem: leads-to-transitive (leads-to (p, q, prg) ∧ leads-to (q, r, prg)) → leads-to (p, r, prg)

Event: Disable leads-to-transitive.

Theorem: leads-to-transitive-general (leads-to (p-1 , q-1 , prg) ∧ leads-to (q-2 , r-1 , prg) ∧ (eval (q-1 , s (prg, jleads (ileads (p, prg, r), prg, q-1 )))

→ eval (q-2 , s (prg, jleads (ileads (p, prg, r), prg, q-1 )))) ∧ (eval (p, s (prg, ileads (p, prg, r))) → eval (p-1 , s (prg, ileads (p, prg, r)))) ∧ (eval (r-1 , s (prg, jleads (jleads (ileads (p, prg, r), prg, q-1 ), prg, r-1 )))

→ eval (r,

s (prg, jleads (jleads (ileads (p, prg, r), prg, q-1 ), prg, r-1 )))))

→ leads-to (p, r, prg)

Event: Disable leads-to-transitive-general.

Theorem: q-leads-to-q leads-to (q, q, prg)

Event: Disable q-leads-to-q.

Theorem: false-leads-to-anything leads-to ('(false), p, prg)

Event: Disable false-leads-to-anything.

Theorem: p-implies-q-leads-to (eval (p, s (prg, ileads (p, prg, q))) → eval (q, s (prg, ileads (p, prg, q)))) → leads-to (p, q, prg)

Event: Disable p-implies-q-leads-to.

Theorem: leads-to-strengthen-left ((eval (q, s (prg, ileads (q, prg, r))) → eval (p, s (prg, ileads (q, prg, r)))) ∧ leads-to (p, r, prg)) → leads-to (q, r, prg)

Event: Disable leads-to-strengthen-left.

Theorem: leads-to-weaken-right ((eval (q, s (prg, jleads (ileads (p, prg, r), prg, q))) → eval (r, s (prg, jleads (ileads (p, prg, r), prg, q)))) ∧ leads-to (p, q, prg)) → leads-to (p, r, prg)

Event: Disable leads-to-weaken-right.

Theorem: leads-to-modify-both ((eval (p, s (prg, ileads (p, prg, q))) → eval (p-1 , s (prg, ileads (p, prg, q)))) ∧ (eval (q-1 , s (prg, jleads (ileads (p, prg, q), prg, q-1 )))

→ eval (q, s (prg, jleads (ileads (p, prg, q), prg, q-1 )))) ∧ leads-to (p-1 , q-1 , prg)) → leads-to (p, q, prg)

Event: Disable leads-to-modify-both.

Theorem: disjoin-left (leads-to (p, r, prg) ∧ leads-to (q, r, prg)) → leads-to (list ('or, p, q), r, prg)

Event: Disable disjoin-left.

Theorem: disjoin-left-general (leads-to (p-1 , q-1 , prg) ∧ leads-to (p-2 , q-2 , prg) ∧ (eval (p, s (prg, ileads (p, prg, q)))

→ eval (list ('or, p-1 , p-2 ), s (prg, ileads (p, prg, q)))) ∧ (eval (q-1 , s (prg, jleads (ileads (p, prg, q), prg, q-1 )))

→ eval (q, s (prg, jleads (ileads (p, prg, q), prg, q-1 )))) ∧ (eval (q-2 , s (prg, jleads (ileads (p, prg, q), prg, q-2 )))

→ eval (q, s (prg, jleads (ileads (p, prg, q), prg, q-2 ))))) → leads-to (p, q, prg)

Event: Disable disjoin-left-general.

Theorem: cancellation-leads-to (leads-to (p, list ('or, q, b), prg) ∧ leads-to (b, r, prg)) → leads-to (p, list ('or, q, r), prg)

Event: Disable cancellation-leads-to.

Theorem: cancellation-leads-to-general (leads-to (p-1 , d, prg) ∧ leads-to (b, r-1 , prg) ∧ (eval (list ('and, d, list ('not, b)),

s (prg, jleads (ileads (p, prg, r), prg, d))) → eval (r, s (prg, jleads (ileads (p, prg, r), prg, d))))

∧ (eval (r-1 , s (prg, jleads (jleads (ileads (p, prg, r), prg, d), prg, r-1 )))

→ eval (r, s (prg, jleads (jleads (ileads (p, prg, r), prg, d), prg, r-1 )))) ∧ (eval (p, s (prg, ileads (p, prg, r))) → eval (p-1 , s (prg, ileads (p, prg, r))))) → leads-to (p, r, prg)

Event: Disable cancellation-leads-to-general.

Definition: ensures-interval (prg, q, top, i) = if top < i then fix (top)

elseif eval (q, s (prg, i)) then fix (i)

else ensures-interval (prg, q, top, 1 + i) endif

Theorem: ensures-interval-fixes (listp (prg) ∧ (i ∉ N)) → (ensures-interval (prg, q, top, i) = ensures-interval (prg, q, top, 0))

Theorem: ensures-interval-bigger (ensures-interval (prg, q, top, i) < i) = (top < i)

Theorem: psp-proves-something (leads-to (p, q, prg) ∧ unless (r, b, prg)

∧ listp (prg) ∧ (i ∈ N) ∧ eval (p, s (prg, base)) ∧ eval (r, s (prg, i)) ∧ (jleads (base, prg, q) < top) ∧ (jleads (base, prg, q) ≮ i) ∧ (final = list ('or, q, b))) → eval (list ('or, list ('and, q, r), b),

s (prg, ensures-interval (prg, final, top, i)))

Event: Disable psp-proves-something.

Theorem: psp (leads-to (p, q, prg) ∧ unless (r, b, prg) ∧ listp (prg)) → leads-to (list ('and, p, r), list ('or, list ('and, q, r), b), prg)

Event: Disable psp.

Theorem: psp-general (leads-to (p, q, prg) ∧ unless (r, b, prg) ∧ (eval (pr, s (prg, ileads (pr, prg, qb)))

→ eval (list ('and, p, r), s (prg, ileads (pr, prg, qb)))) ∧ (eval (list ('or, list ('and, q, r), b),

s (prg,

jleads (ileads (pr, prg, qb), prg, list ('or, list ('and, q, r), b)))) → eval (qb,

s (prg,

jleads (ileads (pr, prg, qb), prg, list ('or, list ('and, q, r), b)))))

∧ listp (prg)) → leads-to (pr, qb, prg)

Event: Disable psp-general.

Theorem: leads-to-true leads-to (p, '(true), prg)

;;; Initial Condition and Invariants

Definition: initial-condition (ic, prg) = eval (ic, s (prg, 0))

Event: Disable initial-condition.

Definition: invariant (inv, prg) ↔ ∀ i eval (inv, s (prg, i))

Event: Disable invariant.

Theorem: prove-invariant eval (inv, s (prg, ii (inv, prg))) → invariant (inv, prg)

Theorem: invariant-implies invariant (inv, prg) → eval (inv, s (prg, i))

Event: Disable prove-invariant.

Theorem: invariant-consequence (invariant (p, prg) ∧ (eval (p, s (prg, ii (q, prg))) → eval (q, s (prg, ii (q, prg))))) → invariant (q, prg)

Theorem: invariants-persist-general (unless (p, '(false), prg) ∧ eval (p, s (prg, i)) ∧ listp (prg) ∧ (j ≮ i)) → eval (p, s (prg, j ))

Event: Disable invariants-persist-general.

Theorem: unless-proves-invariant (initial-condition (ic, prg) ∧ unless (p, '(false), prg) ∧ (eval (ic, s (prg, 0)) → eval (p, s (prg, 0))) ∧ listp (prg)) → invariant (p, prg)

Theorem: leads-to-false-invariant (leads-to (p, '(false), prg) ∧ (eval (list ('not, p), s (prg, ii (inv, prg)))

→ eval (inv, s (prg, ii (inv, prg))))) → invariant (inv, prg)

;;; Eventual Stability

Definition: eventually-stable (r, prg) ↔ ∃ i ∀ j ((j ≮ i) → eval (r, s (prg, j )))

Event: Disable eventually-stable.

Theorem: prove-eventually-stable ((jes (i, prg, r) ≮ i) → eval (r, s (prg, jes (i, prg, r)))) → eventually-stable (r, prg)

Theorem: eventually-stable-implies (eventually-stable (r, prg) ∧ (j ≮ ies (prg, r))) → eval (r, s (prg, j ))

Event: Disable prove-eventually-stable.

Event: Disable eventually-stable-implies.

Theorem: not-leads-to-proves-eventually-stable ((¬ leads-to (p, not-r, prg)) ∧ ((¬ eval (not-r, s (prg, jes (ileads (p, prg, not-r), prg, r))))

→ eval (r, s (prg, jes (ileads (p, prg, not-r), prg, r))))) → eventually-stable (r, prg)

Event: Disable not-leads-to-proves-eventually-stable.

Theorem: not-eventually-stable-proves-leads-to ((¬ eventually-stable (not-q, prg)) ∧ ((¬ eval (not-q, s (prg, jes (ileads (p, prg, q), prg, not-q))))

→ eval (q, s (prg, jes (ileads (p, prg, q), prg, not-q))))) → leads-to (p, q, prg)

Event: Disable not-eventually-stable-proves-leads-to.

Theorem: true-leads-to-proves-not-eventually-stable (leads-to ('(true), not-r, prg) ∧ (eval (not-r, s (prg, jleads (ies (prg, r), prg, not-r)))

→ (¬ eval (r, s (prg, jleads (ies (prg, r), prg, not-r)))))) → (¬ eventually-stable (r, prg))

Event: Disable true-leads-to-proves-not-eventually-stable.

Theorem: eventually-stable-proves-not-true-leads-to (eventually-stable (not-q, prg) ∧ (eval (not-q, s (prg, jleads (ies (prg, not-q), prg, q)))

→ (¬ eval (q, s (prg, jleads (ies (prg, not-q), prg, q)))))) → (¬ leads-to ('(true), q, prg))

Event: Disable eventually-stable-proves-not-true-leads-to.

Theorem: eventually-stable-weaken (eventually-stable (p, prg) ∧ (eval (p, s (prg, jes (ies (prg, p), prg, r)))

→ eval (r, s (prg, jes (ies (prg, p), prg, r))))) → eventually-stable (r, prg)

Event: Disable eventually-stable-weaken.

Theorem: eventually-stable-conjunction (eventually-stable (p, prg) ∧ eventually-stable (q, prg) ∧ (eval (list ('and, p, q),

s (prg,

jes (if ies (prg, p) < ies (prg, q) then ies (prg, q) else ies (prg, p) endif, prg, r)))

→ eval (r,

s (prg,

jes (if ies (prg, p) < ies (prg, q) then ies (prg, q) else ies (prg, p) endif, prg, r)))))

→ eventually-stable (r, prg)

Event: Disable eventually-stable-conjunction.

Theorem: eventually-stable-false (leads-to (p, q, prg) ∧ (eval (q, s (prg, jleads (ies (prg, p), prg, q)))

→ (¬ eval (p, s (prg, jleads (ies (prg, p), prg, q)))))) → (¬ eventually-stable (p, prg))

Event: Disable eventually-stable-false.

Theorem: stable-occurs-proves-eventually-stable (listp (prg) ∧ unless (p, '(false), prg) ∧ leads-to ('(true), p, prg)) → eventually-stable (p, prg)

Event: Disable stable-occurs-proves-eventually-stable.

;;; The Basic Ensures Operator

Definition: ensures (p, q, prg) ↔ ∃ e ((e ∈ prg)

∧ ∀ old, new ((n (old, new, e) ∧ eval (list ('and, p, list ('not, q)), old)) → eval (q, new)))

Event: Disable ensures.

Theorem: prove-ensures ((e ∈ prg) ∧ ((n (olde (e, p, q), newe (e, p, q), e)

∧ eval (p, olde (e, p, q)) ∧ (¬ eval (q, olde (e, p, q)))) → eval (q, newe (e, p, q))))

→ ensures (p, q, prg)

Theorem: ensures-implies (ensures (p, q, prg) → (ee (p, prg, q) ∈ prg)) ∧ ((ensures (p, q, prg)

∧ n (old, new, ee (p, prg, q)) ∧ eval (p, old) ∧ (¬ eval (q, old))) → eval (q, new))

Event: Disable prove-ensures.

Event: Disable ensures-implies.

Theorem: ensures-proves-something (ensures (p, q, prg) ∧ unless (p, q, prg) ∧ schedulable (prg) ∧ (next (prg, ee (p, prg, q), base) < top) ∧ (next (prg, ee (p, prg, q), base) ≮ i) ∧ (i ≮ base) ∧ (i ∈ N) ∧ eval (p, s (prg, i))) → eval (q, s (prg, ensures-interval (prg, q, top, i)))

Theorem: the-interval-of-ensures (ensures (p, q, prg) ∧ unless (p, q, prg) ∧ schedulable (prg) ∧ eval (p, s (prg, i))) → eval (q, s (prg, ensures-interval (prg, q, 1 + next (prg, ee (p, prg, q), i), i)))

Theorem: ensures-proves-leads-to (schedulable (prg) ∧ unless (p, q, prg) ∧ ensures (p, q, prg)) → leads-to (p, q, prg)

Event: Disable ensures-proves-something.

Event: Disable the-interval-of-ensures.

Event: Disable ensures-proves-leads-to.

;;; Total Programs, Statements are Assignments

Definition: total (prg) ↔ ∀ e ((e ∈ prg) → ∀ old ∃ new n (old, new, e))

Event: Disable total.

Theorem: prove-total ((et (prg) ∈ prg) → n (oldt (prg), new, et (prg))) → total (prg)

Theorem: total-implies (total (prg) ∧ (e ∈ prg)) → n (old, newt (e, old), e)

Event: Disable prove-total.

Event: Disable total-implies.

Theorem: total-implies-schedulable (total (prg) ∧ listp (prg)) → schedulable (prg)

;;; Enabled Transitions

Definition: enabling-condition (c, e, prg) ↔ ((e ∈ prg)

∧ ∀ old, new (n (old, new, e) → eval (c, old)) ∧ ∀ old (eval (c, old) → ∃ new n (old, new, e)))

Event: Disable enabling-condition.

Theorem: prove-enabling-condition ((e ∈ prg) ∧ (n (oldc (c, e), newc (c, e), e) → eval (c, oldc (c, e))) ∧ (eval (c, oldc-1 (c, e)) → n (oldc-1 (c, e), new, e))) → enabling-condition (c, e, prg)

Theorem: enabling-condition-implies (enabling-condition (c, e, prg) → (e ∈ prg)) ∧ ((enabling-condition (c, e, prg) ∧ n (old, new, e)) → eval (c, old)) ∧ ((enabling-condition (c, e, prg) ∧ eval (c, old))

→ n (old, newc-1 (e, old), e))

Event: Disable prove-enabling-condition.

Event: Disable enabling-condition-implies.

;;; Ensures with Enabling

Definition: e-ensures (p, q, c, prg) ↔ ∃ e ((e ∈ prg)

∧ enabling-condition (c, e, prg) ∧ ∀ old, new ((n (old, new, e)

∧ eval (list ('and, p, list ('not, q)), old)) → eval (q, new)))

Event: Disable e-ensures.

Theorem: prove-e-ensures ((e ∈ prg) ∧ enabling-condition (c, e, prg) ∧ ((n (oldee (e, p, q), newee (e, p, q), e)

∧ eval (list ('and, p, list ('not, q)), oldee (e, p, q))) → eval (q, newee (e, p, q))))

→ e-ensures (p, q, c, prg)

Event: Disable prove-e-ensures.

Definition: e-ensures-enabling (p, q, c, prg) ↔ ∃ e ((e ∈ prg)

∧ ∀ old, new ((n (old, new, e) → eval (c, old)) ∧ ((n (old, new, e)

∧ eval (list ('and, p, list ('not, q)),

old))

→ eval (q, new)))

∧ ∀ old (eval (c, old) → ∃ new n (old, new, e)))

Event: Disable e-ensures-enabling.

Theorem: help-prove-e-ensures ((e ∈ prg) ∧ (n (oldeee (c, e, p, q), neweee (c, e, p, q), e)

→ (eval (c, oldeee (c, e, p, q)) ∧ eval (q, neweee (c, e, p, q)))) ∧ (eval (c, oldeee-1 (c, e)) → n (oldeee-1 (c, e), new, e)) ∧ (eval (c, oldeee (c, e, p, q))

→ eval (list ('and, p, list ('not, q)), oldeee (c, e, p, q)))) → e-ensures (p, q, c, prg)

Theorem: e-ensures-implies (e-ensures (p, q, c, prg) → (eee (c, p, prg, q) ∈ prg)) ∧ (e-ensures (p, q, c, prg) → enabling-condition (c, eee (c, p, prg, q), prg)) ∧ ((e-ensures (p, q, c, prg)

∧ n (old, new, eee (c, p, prg, q))

∧ eval (list ('and, p, list ('not, q)), old))

→ eval (q, new))

Event: Disable e-ensures-implies.

Event: Disable help-prove-e-ensures.

;;; Union Theorems

Theorem: total-union-1 total (append (prg-1 , prg-2 )) → (total (prg-1 ) ∧ total (prg-2 ))

Theorem: total-union-2 (total (prg-1 ) ∧ total (prg-2 )) → total (append (prg-1 , prg-2 ))

Theorem: total-union total (append (prg-1 , prg-2 )) = (total (prg-1 ) ∧ total (prg-2 ))

Event: Disable total-union-1.

Event: Disable total-union-2.

Theorem: unless-union-1 unless (p, q, append (prg-1 , prg-2 )) → (unless (p, q, prg-1 ) ∧ unless (p, q, prg-2 ))

Theorem: unless-union-2 (unless (p, q, prg-1 ) ∧ unless (p, q, prg-2 )) → unless (p, q, append (prg-1 , prg-2 ))

Theorem: unless-union unless (p, q, append (prg-1 , prg-2 )) = (unless (p, q, prg-1 ) ∧ unless (p, q, prg-2 ))

Event: Disable unless-union-1.

Event: Disable unless-union-2.

Theorem: ensures-union-1 ensures (p, q, append (prg-1 , prg-2 )) → (ensures (p, q, prg-1 ) ∨ ensures (p, q, prg-2 ))

Theorem: ensures-union-2 (ensures (p, q, prg-1 ) ∨ ensures (p, q, prg-2 )) → ensures (p, q, append (prg-1 , prg-2 ))

Event: Disable ensures-union-1.

Event: Disable ensures-union-2.

Theorem: ensures-union ensures (p, q, append (prg-1 , prg-2 )) = (ensures (p, q, prg-1 ) ∨ ensures (p, q, prg-2 ))

;;; Help Prove Total, Unless, and Ensures.

Definition: total-sufficient (statement, program, old, new) = ((statement ∈ program) → n (old, new, statement))

Theorem: help-prove-total total-sufficient (et (prg), prg, oldt (prg), new) → total (prg)

Definition: unless-sufficient (statement, program, old, new, p, q) = (((statement ∈ program)

∧ n (old, new, statement)

∧ eval (p, old) ∧ (¬ eval (q, old))) → eval (list ('or, p, q), new))

Theorem: help-prove-unless unless-sufficient (eu (p, prg, q), prg, oldu (p, prg, q), newu (p, prg, q), p, q) → unless (p, q, prg)

Definition: ensures-key (statement, program, old, new, p, q) = ((statement ∈ program)

∧ ((n (old, new, statement) ∧ eval (p, old) ∧ (¬ eval (q, old))) → eval (q, new)))

Theorem: help-prove-ensures ensures-key (statement, prg, olde (statement, p, q), newe (statement, p, q), p, q) → ensures (p, q, prg)

Definition: ensures-rest (statement, key, program, old, new, p, q) = (((statement ∈ program)

∧ (statement ≠ key) ∧ n (old, new, statement) ∧ eval (p, old) ∧ (¬ eval (q, old))) → eval (p, new))

Theorem: help-prove-unless-ensures (ensures-key (statement, prg, oldu (p, prg, q), newu (p, prg, q), p, q) ∧ ensures-rest (eu (p, prg, q), statement, prg, oldu (p, prg, q), newu (p, prg, q), p, q))

→ unless (p, q, prg)

;;; Strengthening and Weakening Unless and Ensures

Definition: stronger-p (p, q) ↔ ∀ state (eval (p, state) → eval (q, state))

Event: Disable stronger-p.

Theorem: stronger-p-implies (stronger-p (p, q) ∧ eval (p, state)) → eval (q, state)

Theorem: stronger-p-rewrite stronger-p (p, q) = (eval (p, states (p, q)) → eval (q, states (p, q)))

Event: Disable stronger-p-implies.

Definition: equal-p (p, q) ↔ ∀ state (eval (p, state) = eval (q, state))

Event: Disable equal-p.

Theorem: equal-p-implies equal-p (p, q) → (eval (p, state) = eval (q, state))

Event: Disable equal-p-implies.

Theorem: equal-p-rewrite equal-p (p, q) = (eval (p, statee (p, q)) = eval (q, statee (p, q)))

Theorem: equal-p-commutative equal-p (p, q) = equal-p (q, p)

Theorem: ensures-strengthen-left (ensures (q, r, prg) ∧ stronger-p (p, q)) → ensures (p, r, prg)

Event: Disable ensures-strengthen-left.

Theorem: ensures-weaken-right (ensures (p, q, prg) ∧ stronger-p (q, r)) → ensures (p, r, prg)

Event: Disable ensures-weaken-right.

Theorem: unless-weaken-right (unless (p, q, prg) ∧ stronger-p (q, r)) → unless (p, r, prg)

Event: Disable unless-weaken-right.

Theorem: unless-equal-p equal-p (p, q) → (unless (p, r, prg) = unless (q, r, prg))

Theorem: unless-conjunction (unless (p-1 , q, prg) ∧ unless (p-2 , q, prg) ∧ equal-p (p, list ('and, p-1 , p-2 ))) → unless (p, q, prg)

Theorem: unless-disjunction (unless (p-1 , q, prg) ∧ unless (p-2 , q, prg) ∧ equal-p (p, list ('or, p-1 , p-2 ))) → unless (p, q, prg)

;;; Fairness Theorems

Theorem: unconditional-fairness (unless (p, q, prg) ∧ ensures (p, q, prg) ∧ total (prg)) → leads-to (p, q, prg)

Event: Disable unconditional-fairness.

Theorem: unconditional-fairness-general (unless (p-1 , q-1 , prg) ∧ ensures (p-2 , q-2 , prg) ∧ (eval (p, s (prg, ileads (p, prg, q))) → eval (p-1 , s (prg, ileads (p, prg, q)))) ∧ stronger-p (p-1 , p-2 ) ∧ (eval (q-1 , s (prg, jleads (ileads (p-1 , prg, q), prg, q-1 )))

→ eval (q, s (prg, jleads (ileads (p-1 , prg, q), prg, q-1 )))) ∧ stronger-p (q-2 , q-1 ) ∧ total (prg)) → leads-to (p, q, prg)

Event: Disable unconditional-fairness-general.

Conservative Axiom: strong-fairness (unless (p, q, prg) ∧ e-ensures (p, q, c, prg) ∧ leads-to (p, list ('or, q, c), prg) ∧ strongly-fair (prg)) → leads-to (p, q, prg)

Simultaneously, we introduce the new function symbol strongly-fair. Event: Disable strong-fairness.

Theorem: strong-fairness-general (unless (p-1 , q-1 , prg) ∧ e-ensures (p-2 , q-2 , c, prg) ∧ leads-to (p, list ('or, q, c), prg) ∧ (eval (p, s (prg, ileads (p, prg, q))) → eval (p-1 , s (prg, ileads (p, prg, q)))) ∧ (eval (p-1 , s (prg, ileads (p-1 , prg, list ('or, q-1 , c))))

→ eval (p, s (prg, ileads (p-1 , prg, list ('or, q-1 , c))))) ∧ stronger-p (p-1 , p-2 ) ∧ (eval (q-1 , s (prg, jleads (ileads (p-1 , prg, q), prg, q-1 )))

→ eval (q, s (prg, jleads (ileads (p-1 , prg, q), prg, q-1 )))) ∧ (eval (list ('or, q, c),

s (prg,

jleads (ileads (p, prg, list ('or, q-1 , c)), prg, list ('or, q, c)))) → eval (list ('or, q-1 , c), s (prg,

jleads (ileads (p, prg, list ('or, q-1 , c)), prg, list ('or, q, c)))))

∧ stronger-p (q-2 , q-1 ) ∧ strongly-fair (prg)) → leads-to (p, q, prg)

Event: Disable strong-fairness-general.

Definition: wfw (i, j , p, q, c, prg) = if i < j

then if eval (q, s (prg, i)) then i elseif eval (p, s (prg, i)) then if eval (c, s (prg, i)) then wfw (1 + i, j , p, q, c, prg)

else i endif else i endif

else fix (i) endif Theorem: wfw-bigger wfw (i, j , p, q, c, prg) ≮ i

Theorem: about-wfw (unless (p, q, prg) ∧ listp (prg) ∧ eval (p, s (prg, i)) ∧ (j ≮ i)) → (eval (q, s (prg, wfw (i, j , p, q, c, prg)))

∨ (eval (p, s (prg, wfw (i, j , p, q, c, prg))) ∧ (¬ eval (q, s (prg, wfw (i, j , p, q, c, prg)))) ∧ (¬ eval (c, s (prg, wfw (i, j , p, q, c, prg)))))

∨ ((wfw (i, j , p, q, c, prg) = fix (j )) ∧ (eval (p, s (prg, j )) ∨ eval (q, s (prg, j )))))

Definition: witness (p, q, c, prg) = wfw (ileads (p, prg, q),

next (prg, eee (c, p, prg, q), ileads (p, prg, q)), p, q, c, prg)

Theorem: weak-fairness (unless (p, q, prg) ∧ e-ensures (p, q, c, prg) ∧ (eval (list ('and, p, list ('not, q)), s (prg, witness (p, q, c, prg)))

→ eval (c, s (prg, witness (p, q, c, prg))))) → leads-to (p, q, prg)

Event: Disable weak-fairness.

Theorem: weak-fairness-general (unless (p-1 , q-1 , prg) ∧ e-ensures (p-2 , q-2 , c, prg) ∧ (eval (list ('and, p-1 , list ('not, q-1 )), s (prg, witness (p-1 , q-1 , c, prg)))

→ eval (c, s (prg, witness (p-1 , q-1 , c, prg)))) ∧ (eval (p, s (prg, ileads (p, prg, q))) → eval (p-1 , s (prg, ileads (p, prg, q)))) ∧ stronger-p (p-1 , p-2 ) ∧ (eval (q-1 , s (prg, jleads (ileads (p-1 , prg, q), prg, q-1 )))

→ eval (q, s (prg, jleads (ileads (p-1 , prg, q), prg, q-1 )))) ∧ stronger-p (q-2 , q-1 )) → leads-to (p, q, prg)

Event: Disable weak-fairness-general.

Event: Disable witness.

Theorem: deadlock-freedom-witness (unless (inv, '(false), prg) ∧ enabling-condition (c, e, prg) ∧ (eval (inv, s (prg, next (prg, e, ileads (inv, prg, '(false)))))

→ (¬ eval (c, s (prg, next (prg, e, ileads (inv, prg, '(false))))))) ∧ schedulable (prg)) → leads-to (inv, '(false), prg)

Event: Disable deadlock-freedom-witness.

Conservative Axiom: deadlock-freedom (unless (inv, '(false), prg) ∧ enabling-condition (c, e, prg) ∧ (eval (inv, s (prg, next (prg, e, ileads (inv, prg, '(false)))))

→ (¬ eval (c, s (prg, next (prg, e, ileads (inv, prg, '(false))))))) ∧ deadlock-free (prg)) → leads-to (inv, '(false), prg)

Simultaneously, we introduce the new function symbol deadlock-free.

Theorem: deadlock-freedom-general (unless (inv, '(false), prg) ∧ enabling-condition (c, e, prg) ∧ (eval (inv, s (prg, next (prg, e, ileads (inv, prg, '(false)))))

→ (¬ eval (c, s (prg, next (prg, e, ileads (inv, prg, '(false))))))) ∧ ((¬ eval (inv, s (prg, ii (p, prg)))) → eval (p, s (prg, ii (p, prg)))) ∧ deadlock-free (prg)) → invariant (p, prg)

Event: Enable eval.

Event: Enable n.

;;; Some Helpful Definitions and Theorems

Definition: update-assoc (key, value, alist) = if listp (alist)

then if caar (alist) = key then cons (cons (key, value), cdr (alist))

else cons (car (alist), update-assoc (key, value, cdr (alist))) endif else list (cons (key, value)) endif Theorem: simplify-assoc assoc (key-1 , update-assoc (key-2 , value, alist)) = if key-1 = key-2 then cons (key-1 , value)

else assoc (key-1 , alist) endif

Definition: add1-mod (n, x) = if (1 + x) < n then 1 + x

else 0 endif

Definition: sub1-mod (n, x) = if x < n

then if x ≃ 0 then n − 1 else x − 1 endif

else 0 endif

Definition: uc (old, new, keys, excpt) = if listp (keys)

then if car (keys) ∈ excpt then uc (old, new, cdr (keys), excpt) elseif assoc (car (keys), old) = assoc (car (keys), new) then uc (old, new, cdr (keys), excpt) else f endif

else t endif

Theorem: uc-basic-property (uc (old, new, keys, excpt) ∧ (key ∈ keys) ∧ (key ∉ excpt)) → ((assoc (key, old) = assoc (key, new)) = t)

Theorem: uc-commutative uc (old, new, keys, excpt) = uc (new, old, keys, excpt)

Theorem: uc-reflexive uc (list, list, keys, excpt)

Theorem: uc-of-update-assoc uc (list-1 , update-assoc (key, value, list-2 ), keys, excpt) = if key ∈ excpt then uc (list-1 , list-2 , keys, excpt)

elseif key ∈ keys

then (assoc (key, list-1 ) = cons (key, value))

∧ uc (list-1 , list-2 , keys, cons (key, excpt)) else uc (list-1 , list-2 , keys, excpt) endif

Theorem: strip-cars-append strip-cars (append (a, b)) = append (strip-cars (a), strip-cars (b))

Theorem: uc-append uc (old, new, append (a, b), excpt) = (uc (old, new, a, excpt) ∧ uc (old, new, b, excpt))

Theorem: uc-commutative-2 uc (old, new, append (a, b), excpt) = uc (old, new, append (b, a), excpt)

Event: Disable uc-append.

Theorem: key-not-member-strip-cars (key ∉ strip-cars (alist)) → (assoc (key, alist) = f)

Theorem: uc-property (uc (old, new, append (strip-cars (old), strip-cars (new)), excpt) ∧ (key ∉ excpt)) → ((assoc (key, old) = assoc (key, new)) = t)

Theorem: about-uc (uc (a, b, append (strip-cars (a), strip-cars (b)), excpt) ∧ (key ∉ excpt)) → (assoc (key, a) = assoc (key, b))

Definition: changed (old, new, excpt) = uc (old, new, strip-cars (append (old, new)), excpt)

Event: Make the library "interpreter".

Index

about-uc, 27 about-wfw, 24 add1-mod, 26 append-is-associative, 2

cancellation-leads-to, 10 cancellation-leads-to-general, 10 changed, 27 choose, 4, 7, 8 computation, 4 computation-n, 8

deadlock-free, 25 deadlock-freedom, 25 deadlock-freedom-general, 25 deadlock-freedom-witness, 25 disjoin-left, 9 disjoin-left-general, 9

e-ensures, 17, 18, 23, 24 e-ensures-enabling, 18 e-ensures-implies, 18 ee, 15, 16 eee, 18, 24 effective-idle, 8 enabling-condition, 17, 18, 25 enabling-condition-implies, 17 ensures, 15, 16, 19–22 ensures-implies, 15 ensures-interval, 10, 11, 15, 16 ensures-interval-bigger, 10 ensures-interval-fixes, 10 ensures-key, 20 ensures-proves-leads-to, 16 ensures-proves-something, 15 ensures-rest, 20, 21 ensures-strengthen-left, 21 ensures-union, 19 ensures-union-1, 19 ensures-union-2, 19 ensures-weaken-right, 22 equal-iff, 1 equal-p, 21, 22 equal-p-commutative, 21 equal-p-implies, 21 equal-p-rewrite, 21 et, 16, 20 eu, 6, 20 eval, 5–18, 20–25 eval-and, 5 eval-equal, 6 eval-false, 6 eval-iff, 6 eval-implies, 6 eval-not, 5 eval-or, 6 eval-true, 6 eventually-stable, 12–14 eventually-stable-conjunction, 14 eventually-stable-false, 14 eventually-stable-implies, 13 eventually-stable-proves-not-tr

ue-leads-to, 13 eventually-stable-weaken, 14 exists, 3, 7, 12, 15–18 exists-successor, 3 exists-successor-implies, 3

false-leads-to-anything, 8 forall, 6, 7, 12, 15–18, 21

help-prove-e-ensures, 18 help-prove-ensures, 20 help-prove-total, 20 help-prove-unless, 20 help-prove-unless-ensures, 20

ies, 13, 14 ii, 12, 25 ileads, 7–11, 13, 22–25 initial-condition, 11, 12 invariant, 12, 25 invariant-consequence, 12 invariant-implies, 12 invariants-persist-general, 12 is, 7

jes, 13, 14 jleads, 7–11, 13, 14, 22–24

key-not-member-strip-cars, 27

leads-to, 7–14, 16, 22–25 leads-to-false-invariant, 12 leads-to-implies, 7 leads-to-modify-both, 9 leads-to-strengthen-left, 9 leads-to-transitive, 8 leads-to-transitive-general, 8 leads-to-true, 11 leads-to-weaken-right, 9 length, 1–3 listp-not-zero-length, 1

mchoose, 2, 4 mchoose-chooses, 2 mchoose-fixes, 2 member-append, 2 mnext, 2 mnext-choice-1, 2 mnext-choice-2, 2 mnext-choice-2-simplified, 2 mnext-fixes, 2 ms, 4 ms-transition-idle, 4 ms-transition-successful, 4

n, 3, 4, 6–8, 15–18, 20 newc, 17 newc-1, 17 newe, 15, 20 newee, 17 neweee, 18 news, 7 newt, 16 newu, 6, 20, 21 newx, 3, 4 next, 4, 8, 15, 16, 24, 25 not-eventually-stable-proves-le

ads-to, 13 not-leads-to-proves-eventually-

stable, 13 nth, 1–3 nth-member, 1 nth-position, 1 numberp-mnext, 2

oldc, 17 oldc-1, 17 olde, 15, 20 oldee, 17 oldeee, 18 oldeee-1, 18 oldt, 16, 20 oldu, 6, 20, 21

p-implies-q-leads-to, 9

position, 1–3 position-lessp, 1 position-nth, 2 position-zero, 1 prove-e-ensures, 17 prove-enabling-condition, 17 prove-ensures, 15 prove-eventually-stable, 13 prove-exists-successor, 3 prove-invariant, 12 prove-leads-to, 7 prove-schedulable, 7 prove-total, 16 prove-unless, 6 psp, 11 psp-general, 11 psp-proves-something, 10

q-leads-to-q, 8

remainder-of-add1, 3 remainder-of-add1-1, 3 remainder-of-add1-2, 3 remainder-of-add1-3, 3 remainder-of-add1-3-1, 3

s, 4, 7–16, 22–25 schedulable, 7, 8, 15, 16, 25 schedulable-implies, 7 schedulable-implies-effective-c

omputation, 8 simplify-assoc, 26 stable-occurs-proves-eventually

-stable, 14 statee, 21 states, 21 strip-cars-append, 26 strong-fairness, 23 strong-fairness-general, 23 stronger-p, 21–24 stronger-p-implies, 21 stronger-p-rewrite, 21 strongly-fair, 23 sub1-mod, 26

the-interval-of-ensures, 16 total, 16, 18–20, 22 total-implies, 16 total-implies-schedulable, 16 total-sufficient, 20 total-union, 19 total-union-1, 18 total-union-2, 19 true-leads-to-proves-not-eventu

ally-stable, 13

uc, 26, 27 uc-append, 27 uc-basic-property, 26 uc-commutative, 26 uc-commutative-2, 27 uc-of-update-assoc, 26 uc-property, 27 uc-reflexive, 26 unconditional-fairness, 22 unconditional-fairness-general, 22 unless, 6, 10–12, 14–16, 19–25 unless-conjunction, 22 unless-disjunction, 22 unless-equal-p, 22 unless-implies, 6 unless-proves-invariant, 12 unless-sufficient, 20 unless-union, 19 unless-union-1, 19 unless-union-2, 19 unless-weaken-right, 22 update-assoc, 25, 26

weak-fairness, 24

weak-fairness-general, 24 wfw, 23, 24 wfw-bigger, 24 witness, 24