Event: Start with the library "interpreter".

;;; The Program

Definition: status (state, index) = cdr (assoc (cons ('s, index), state))

Definition: thinking (state, index) = (status (state, index) = 'thinking)

Definition: hungry (state, index) = (status (state, index) = 'hungry)

Definition: eating (state, index) = (status (state, index) = 'eating)

Definition: fork (state, index) = cdr (assoc (cons ('f, index), state))

Definition: free (state, index) = (fork (state, index) = 'free)

Definition: owns-left (state, index) = (fork (state, index) = index)

Definition: owns-right (state, index, n) = (fork (state, add1-mod (n, index)) = index)

Definition: thinking-to (old, new, index) = if thinking (old, index)

then (thinking (new, index) ∨ hungry (new, index)) ∧ changed (old, new, list (cons ('s, index)))

else changed (old, new, nil) endif

Definition: hungry-left (old, new, index) = (hungry (old, index)

∧ free (old, index)

∧ owns-left (new, index)

∧ changed (old, new, list (cons ('f, index))))

Definition: hungry-right (old, new, index, n) = (hungry (old, index)

∧ free (old, add1-mod (n, index)) ∧ owns-right (new, index, n) ∧ changed (old, new, list (cons ('f, add1-mod (n, index)))))

Definition: hungry-both (old, new, index, n) = if hungry (old, index)

∧ owns-left (old, index) ∧ owns-right (old, index, n)

then eating (new, index) ∧ changed (old, new, list (cons ('s, index))) else changed (old, new, nil) endif

Definition: eating-to (old, new, index, n) = if eating (old, index)

then thinking (new, index) ∧ free (new, index) ∧ free (new, add1-mod (n, index)) ∧ changed (old,

new,

list (cons ('s, index), cons ('f, index), cons ('f, add1-mod (n, index))))

else changed (old, new, nil) endif

Definition: phil (index, n) = list (list ('thinking-to, index),

list ('hungry-left, index), list ('hungry-right, index, n), list ('hungry-both, index, n), list ('eating-to, index, n))

Definition: ring (index, n) = if index ≃ 0 then nil

else append (phil (index − 1, n), ring (index − 1, n)) endif

Definition: phil-prg (n) = ring (n, n)

Event: Disable phil-prg.

Event: Disable *1*phil-prg.

;;; Correctness

Theorem: member-ring (statement ∈ ring (index, n)) = ((statement ∈ phil (cadr (statement), n))

∧ (cadr (statement) ∈ N) ∧ (cadr (statement) < index))

Theorem: member-phil-prg (statement ∈ phil-prg (n)) = ((statement ∈ phil (cadr (statement), n))

∧ (cadr (statement) ∈ N) ∧ (cadr (statement) < n))

Definition: proper-forks-rec (state, index, n) = if index ≃ 0 then t

else (free (state, index − 1) ∨ (fork (state, index − 1) = (index − 1)) ∨ (fork (state, index − 1) = sub1-mod (n, index − 1))) ∧ proper-forks-rec (state, index − 1, n) endif

Theorem: proper-forks-rec-implies (proper-forks-rec (state, index, n) ∧ (n ≮ index) ∧ (1 < n) ∧ (i < index) ∧ (i ∈ N)) → (free (state, i)

∨ (fork (state, i) = i)

∨ (fork (state, i) = sub1-mod (n, i)))

Definition: proper-forks (state, n) = proper-forks-rec (state, n, n)

Theorem: proper-forks-implies (proper-forks (state, n) ∧ (1 < n) ∧ (i < n) ∧ (i ∈ N)) → (free (state, i)

∨ (fork (state, i) = i)

∨ (fork (state, i) = sub1-mod (n, i)))

Definition: proper-phil (state, phil, right) = ((thinking (state, phil)

→ ((fork (state, phil) ≠ phil)

∧ (fork (state, right) ≠ phil))) ∧ (eating (state, phil)

→ ((fork (state, phil) = phil)

∧ (fork (state, right) = phil)))

∧ (thinking (state, phil) ∨ hungry (state, phil) ∨ eating (state, phil)))

Definition: proper-phils-rec (state, index, n) = if index ≃ 0 then t

else proper-phil (state, index − 1, add1-mod (n, index − 1)) ∧ proper-phils-rec (state, index − 1, n) endif

Theorem: proper-phils-rec-implies-proper-phil (proper-phils-rec (state, index, n) ∧ (1 < n) ∧ (n ≮ index) ∧ (phil < index) ∧ (phil ∈ N) ∧ (right = add1-mod (n, phil))) → proper-phil (state, phil, right)

Theorem: proper-phils-rec-implies (proper-phils-rec (state, index, n) ∧ (n ≮ index) ∧ (1 < n) ∧ (phil < index) ∧ (phil ∈ N)) → ((thinking (state, phil)

→ ((¬ owns-left (state, phil))

∧ (¬ owns-right (state, phil, n)))) ∧ (eating (state, phil)

→ (owns-left (state, phil) ∧ owns-right (state, phil, n))) ∧ (thinking (state, phil)

∨ hungry (state, phil) ∨ eating (state, phil)))

Definition: proper-phils (state, n) = proper-phils-rec (state, n, n)

Theorem: proper-phils-implies-proper-phil (proper-phils (state, n) ∧ (1 < n) ∧ (phil < n) ∧ (phil ∈ N) ∧ (right = add1-mod (n, phil))) → proper-phil (state, phil, right)

Definition: all-lefts (state, index) = if index ≃ 0 then t

else owns-left (state, index − 1)

∧ hungry (state, index − 1)

∧ all-lefts (state, index − 1) endif

Theorem: all-lefts-implies ((i < n) ∧ (i ∈ N) ∧ all-lefts (state, n)) → (hungry (state, i) ∧ owns-left (state, i))

Definition: all-rights-rec (state, index, n) = if index ≃ 0 then t

else owns-right (state, index − 1, n) ∧ hungry (state, index − 1) ∧ all-rights-rec (state, index − 1, n) endif

Theorem: all-rights-rec-implies ((1 < n) ∧ (n ≮ index) ∧ (i < index) ∧ (i ∈ N) ∧ all-rights-rec (state, index, n)) → (hungry (state, i) ∧ owns-right (state, i, n))

Definition: all-rights (state, n) = all-rights-rec (state, n, n)

Theorem: all-rights-implies ((1 < n) ∧ (i < n) ∧ (i ∈ N) ∧ all-rights (state, n)) → (hungry (state, i) ∧ owns-right (state, i, n))

;(defn initial (state n)
;  (and (proper-forks state n)
;       (proper-phils state n)))

Theorem: listp-phil-prg listp (phil-prg (n)) = (n ≄ 0)

Definition: pfusi (index, n, statement) = if index ≃ 0 then t

elseif (index − 1) = cadr (statement) then pfusi (index − 1, n, statement) elseif (index − 1) = add1-mod (n, cadr (statement)) then pfusi (index − 1, n, statement) else pfusi (index − 1, n, statement) endif Theorem: proper-forks-rec-unless-sufficient ((n ≮ index) ∧ (1 < n)) → unless-sufficient (statement,

phil-prg (n),

old, new,

                   `(proper-forks-rec state ',index ',n),
                   '(false))

Definition: proper-triple (state, phil, n) = (proper-phil (state, sub1-mod (n, phil), add1-mod (n, sub1-mod (n, phil)))

∧ proper-phil (state, phil, add1-mod (n, phil))

∧ proper-phil (state, add1-mod (n, phil), add1-mod (n, add1-mod (n, phil))))

Definition: but-triple (state, index, phil, n) = if index ≃ 0 then t

elseif ((index − 1) = sub1-mod (n, phil)) ∨ ((index − 1) = phil) ∨ ((index − 1) = add1-mod (n, phil))

then but-triple (state, index − 1, phil, n)

else proper-phil (state, index − 1, add1-mod (n, index − 1)) ∧ but-triple (state, index − 1, phil, n) endif

Theorem: lessp-1 (1 < n) = ((n ≄ 0) ∧ (n ≠ 1))

Theorem: lessp-2 (x < 2) = ((x = 1) ∨ (x ≃ 0))

Theorem: lessp-2-2 (2 < x) = ((x ≄ 0) ∧ (x ≠ 1) ∧ (x ≠ 2))

Theorem: proper-triple-preserved ((1 < n) ∧ (phil < n) ∧ (phil ∈ N) ∧ (statement ∈ phil (phil, n)) ∧ n (old, new, statement) ∧ proper-triple (old, phil, n)) → proper-triple (new, phil, n)

Theorem: but-triple-preserved ((1 < n) ∧ (n ≮ index) ∧ (phil < n) ∧ (phil ∈ N) ∧ (statement ∈ phil (phil, n)) ∧ n (old, new, statement) ∧ but-triple (old, index, phil, n)) → but-triple (new, index, phil, n)

Theorem: but-triple-and-triple-all ((phil ∈ N) ∧ (n ≮ index)) → (proper-phils-rec (state, index, n)

= (but-triple (state, index, phil, n)

∧ if add1-mod (n, phil) < index then if phil < index

then if sub1-mod (n, phil) < index then proper-triple (state, phil, n) else proper-phil (state,

phil,

add1-mod (n, phil))

∧ proper-phil (state,

add1-mod (n,

phil),

add1-mod (n,

add1-mod (n,

phil))) endif

elseif sub1-mod (n, phil) < index

then proper-phil (state, sub1-mod (n, phil), add1-mod (n, sub1-mod (n, phil)))

∧ proper-phil (state, add1-mod (n, phil), add1-mod (n,

add1-mod (n, phil)))

else proper-phil (state, add1-mod (n, phil), add1-mod (n,

add1-mod (n, phil))) endif

elseif phil < index

then if sub1-mod (n, phil) < index

then proper-phil (state, phil, add1-mod (n, phil))

∧ proper-phil (state, sub1-mod (n, phil), add1-mod (n,

sub1-mod (n, phil)))

else proper-phil (state, phil, add1-mod (n, phil)) endif

elseif sub1-mod (n, phil) < index then proper-phil (state,

sub1-mod (n, phil),

add1-mod (n, sub1-mod (n, phil)))

else t endif))

Theorem: proper-phils-preserved ((1 < n) ∧ (statement ∈ phil-prg (n)) ∧ n (old, new, statement) ∧ proper-phils (old, n)) → proper-phils (new, n)

Event: Disable but-triple-and-triple-all.

Event: Disable but-triple-preserved.

Event: Disable proper-triple-preserved.

Event: Disable proper-phils.

Theorem: proper-phils-unless-sufficient (1 < n) → unless-sufficient (statement,

phil-prg (n),

old, new,

                   `(proper-phils state ',n),
                   '(false))

Theorem: all-lefts-unchanged (all-lefts (old, n) ∧ changed (old, new, nil)) → all-lefts (new, n)

Theorem: all-lefts-unless-sufficient (1 < n) → unless-sufficient (statement,

phil-prg (n),

old, new,

                  `(all-lefts state ',n),
                  '(false))

Event: Disable all-lefts-implies.

Event: Disable all-lefts-unchanged.

Theorem: all-rights-rec-unchanged (all-rights-rec (old, index, n) ∧ changed (old, new, nil) ∧ (n ≮ index)) → all-rights-rec (new, index, n)

Theorem: all-rights-unless-sufficient (1 < n) → unless-sufficient (statement,

phil-prg (n),

old, new,

                  `(all-rights state ',n),
                  '(false))

Event: Disable all-rights-implies.

Event: Disable all-rights-rec-unchanged.

Theorem: proper-forks-rec-inv (1 < n)

→ unless (`(proper-forks-rec state ',n ',n),
          '(false),

phil-prg (n))

Theorem: proper-forks-inv (1 < n)

→ unless (`(proper-forks state ',n), '(false), phil-prg (n))

Theorem: proper-phils-inv (1 < n)

→ unless (`(proper-phils state ',n), '(false), phil-prg (n))

Theorem: all-lefts-inv

(1 < n) → unless (`(all-lefts state ',n), '(false), phil-prg (n))

Theorem: all-rights-inv (1 < n)

→ unless (`(all-rights state ',n), '(false), phil-prg (n))

Theorem: phil-prg-invariant-1 ((1 < n) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ (invariant (`(proper-phils state ',n), phil-prg (n)) ∧ invariant (`(proper-forks state ',n), phil-prg (n)) ∧ invariant (`(and

                  (proper-phils state ',n)
                  (proper-forks state ',n)),

phil-prg (n)))

Theorem: proper-phil-invariant ((index < n) ∧ (index ∈ N) ∧ (1 < n) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ invariant (`(proper-phil state
              ',index
              ',(add1-mod n index)),

phil-prg (n))

Definition: proper-fork (state, index, left) = (free (state, index)

∨ (fork (state, index) = index)

∨ (fork (state, index) = left))

Theorem: proper-fork-invariant ((index < n) ∧ (index ∈ N) ∧ (1 < n) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ invariant (`(proper-fork state
              ',index
              ',(sub1-mod n index)),

phil-prg (n))

Theorem: hungry-unless-owns-left ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ unless (`(hungry state ',index),
          `(owns-left state ',index),

phil-prg (n))

Theorem: hungry-unless-owns-right ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ unless (`(hungry state ',index),
          `(owns-right state ',index ',n),

phil-prg (n))

Theorem: hungry-left-free-e-ensures-owns-left ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ e-ensures (`(hungry state ',index),
             `(owns-left state ',index),
             `(and
               (hungry state ',index)
               (free state ',index)),

phil-prg (n))

Theorem: hungry-right-free-e-ensures-owns-right ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ e-ensures (`(hungry state ',index),
             `(owns-right state ',index ',n),
             `(and
               (hungry state ',index)
               (free state ',(add1-mod n index))),

phil-prg (n))

Theorem: hungry-unless-eating ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ unless (`(hungry state ',index),
          `(eating state ',index),

phil-prg (n))

Theorem: owns-left-unless-sufficient ((1 < n) ∧ (index < n) ∧ (index ∈ N)) → unless-sufficient (statement,

phil-prg (n),

old, new,

                  `(and
                    (proper-phils state ',n)
                    (owns-left state ',index)),
                  `(eating state ',index))

Theorem: owns-right-unless-sufficient ((1 < n) ∧ (index < n) ∧ (index ∈ N)) → unless-sufficient (statement,

phil-prg (n),

old, new,

                  `(and
                    (proper-phils state ',n)
                    (owns-right state ',index ',n)),
                  `(eating state ',index))

Theorem: owns-right-unless-eating ((1 < n) ∧ (index < n) ∧ (index ∈ N)) → unless (`(and

            (proper-phils state ',n)
            (owns-right state ',index ',n)),
          `(eating state ',index),

phil-prg (n))

Theorem: owns-left-unless-eating ((1 < n) ∧ (index < n) ∧ (index ∈ N)) → unless (`(and

            (proper-phils state ',n)
            (owns-left state ',index)),
          `(eating state ',index),

phil-prg (n))

Theorem: owns-both-unless-eating ((1 < n) ∧ (index < n) ∧ (index ∈ N)) → unless (`(and

            (owns-left state ',index)
            (and
             (owns-right state ',index ',n)
             (proper-phils state ',n))),
          `(eating state ',index),

phil-prg (n))

Theorem: owns-both-e-ensures-eating ((1 < n) ∧ (index < n) ∧ (index ∈ N)) → e-ensures (`(and

               (owns-left state ',index)
               (and
                (owns-right state ',index ',n)
                (proper-phils state ',n))),
             `(eating state ',index),

             `(true),

phil-prg (n))

Theorem: owns-both-leads-to-eating ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ leads-to (`(and

              (owns-left state ',index)
              (owns-right state ',index ',n)),
            `(eating state ',index),

phil-prg (n))

Theorem: eating-unless-free ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ unless (`(eating state ',index),
          `(and
            (free state ',index)
            (free state ',(add1-mod n index))),

phil-prg (n))

Theorem: eating-e-ensures-free ((1 < n) ∧ (index < n) ∧ (index ∈ N))

→ e-ensures (`(eating state ',index),
             `(and
               (free state ',index)
               (free state ',(add1-mod n index))),
             '(true),

phil-prg (n))

Theorem: eating-leads-to-free ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ leads-to (`(eating state ',index),
            `(and
              (free state ',index)

             (free state ',(add1-mod n index))),

phil-prg (n))

Theorem: leads-to-expanded-right-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ leads-to (`(true),

           `(or
             (owns-right state ',(sub1-mod n index) ',n)
             (or
              (free state ',index)
              (or
               (eating state ',index)
               (thinking state ',index)))),

phil-prg (n)))

→ leads-to (`(true),

           `(or
             (free state ',index)
             (owns-right state ',(sub1-mod n index) ',n)),

phil-prg (n))

Theorem: leads-to-expanded-left-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ leads-to (`(true),

           `(or
             (owns-left state ',(add1-mod n index))
             (or
              (free state ',(add1-mod n index))
              (or
               (eating state ',index)
               (thinking state ',index)))),

phil-prg (n)))

→ leads-to (`(true),

           `(or
             (free state ',(add1-mod n index))
             (owns-left state ',(add1-mod n index))),

phil-prg (n))

Theorem: true-leads-to-left-free-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ leads-to (`(true),

           `(or
             (free state ',index)
             (owns-left state ',index)),

phil-prg (n)))

→ leads-to (`(hungry state ',index),
           `(owns-left state ',index),

phil-prg (n))

Theorem: true-leads-to-right-free-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ leads-to (`(true),

           `(or
             (free state ',(add1-mod n index))
             (owns-right state ',index ',n)),

phil-prg (n)))

→ leads-to (`(hungry state ',index),
           `(owns-right state ',index ',n),

phil-prg (n))

Theorem: hungry-leads-to-owns-right-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N)

∧ strongly-fair (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ leads-to (`(hungry state ',index),
           `(owns-right state ',index ',n),

phil-prg (n)))

→ leads-to (`(and

             (hungry state ',index)
             (owns-left state ',index)),
           `(eating state ',index),

phil-prg (n))

Theorem: hungry-leads-to-owns-left-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ leads-to (`(hungry state ',index),
           `(owns-left state ',index),

phil-prg (n)))

→ leads-to (`(and

             (hungry state ',index)
             (owns-right state ',index ',n)),
           `(eating state ',index),

phil-prg (n))

Definition: left-chain (i, j , n, state) = if (i ∈ N) ∧ (j ∈ N) ∧ (i < n) ∧ (j < n)

then if i = j then hungry (state, i) ∧ owns-left (state, i)

else hungry (state, i) ∧ owns-left (state, i) ∧ left-chain (sub1-mod (n, i), j , n, state) endif

else f endif

Definition: right-chain (i, j , n, state) = if (i ∈ N) ∧ (j ∈ N) ∧ (i < n) ∧ (j < n)

then if i = j then hungry (state, i) ∧ owns-right (state, i, n) else hungry (state, i)

∧ owns-right (state, i, n)

∧ right-chain (add1-mod (n, i), j , n, state) endif

else f endif

Theorem: break-left-chain ((i < n) ∧ (j < n) ∧ (i ∈ N) ∧ (j ∈ N) ∧ (i < j )) → (left-chain (i, j , n, state)

= (left-chain (i, 0, n, state) ∧ left-chain (n − 1, j , n, state)))

Definition: lcc (i, j , k) = if (i ∈ N)

∧ (j ∈ N) ∧ (k ∈ N) ∧ (i < k) ∧ (j < k) ∧ (i ≠ j ) ∧ (k ≄ 0)

then if (1 + i) = k then lcc (i − 1, j , k − 1) elseif (1 + j ) = k then lcc (i, j − 1, k − 1) else lcc (i, j , k − 1) endif

else t endif

Theorem: left-chain-combine ((i ∈ N) ∧ (j ∈ N) ∧ (k ∈ N) ∧ (k < n) ∧ (i < k) ∧ (j < k)) → ((left-chain (i, 0, n, state) ∧ left-chain (k, 1 + i, n, state))

= (left-chain (j , 0, n, state) ∧ left-chain (k, 1 + j , n, state)))

Theorem: lessp-1-1 (n < 1) = (n ≃ 0)

Event: Disable lessp-1-1.

Theorem: left-chain-canonicalize ((i ∈ N) ∧ (i < n)) → (left-chain (i, add1-mod (n, i), n, state) = left-chain (n − 1, 0, n, state))

Theorem: left-chain-canonicalize-all-lefts ((index ≄ 0) ∧ (n ≮ index)) → (left-chain (index − 1, 0, n, state) = all-lefts (state, index))

Theorem: left-chain-complete ((i ∈ N) ∧ (i < n)) → (left-chain (i, add1-mod (n, i), n, state) = all-lefts (state, n))

Event: Disable left-chain-canonicalize-all-lefts.

Event: Disable left-chain-canonicalize.

Event: Disable left-chain-combine.

Event: Disable break-left-chain.

Theorem: break-right-chain ((i < n) ∧ (j < n) ∧ (i ∈ N) ∧ (j ∈ N) ∧ (j < i)) → (right-chain (i, j , n, state)

= (right-chain (i, n − 1, n, state) ∧ right-chain (0, j , n, state)))

Definition: rcc (i, j , k, n) = if (i < n)

∧ (j < n) ∧ (k ∈ N) ∧ (k < i) ∧ (k < j ) ∧ (i ≠ j ) ∧ (k ≠ n)

then if k = (i − 1) then rcc (1 + i, j , 1 + k, n) elseif k = (j − 1) then rcc (i, 1 + j , 1 + k, n) else rcc (i, j , 1 + k, n) endif

else t endif

Theorem: right-chain-combine ((k ∈ N) ∧ (i < n) ∧ (j < n) ∧ (k < i) ∧ (k < j )) → ((right-chain (i, n − 1, n, state) ∧ right-chain (k, i − 1, n, state))

= (right-chain (j , n − 1, n, state)

∧ right-chain (k, j − 1, n, state)))

Theorem: right-chain-canonicalize ((i ∈ N) ∧ (i < n)) → (right-chain (i, sub1-mod (n, i), n, state)

= right-chain (0, n − 1, n, state))

Theorem: right-chain-extend-right ((i ∈ N) ∧ (j ∈ N) ∧ (i < n) ∧ (j < n) ∧ (i ≠ j )) → (right-chain (i, j , n, state)

= (right-chain (i, sub1-mod (n, j ), n, state)

∧ hungry (state, j )

∧ owns-right (state, j , n)))

Theorem: right-chain-canonicalize-all-rights ((index ≄ 0) ∧ (n ≮ index)) → (right-chain (0, index − 1, n, state) = all-rights-rec (state, index, n))

Theorem: right-chain-complete ((i ∈ N) ∧ (i < n)) → (right-chain (i, sub1-mod (n, i), n, state) = all-rights (state, n))

Event: Disable right-chain-canonicalize-all-rights.

Event: Disable right-chain-extend-right.

Event: Disable right-chain-canonicalize.

Event: Disable right-chain-combine.

Event: Disable break-right-chain.

Theorem: not-eventually-left-implies ((1 < n) ∧ (index < n) ∧ (index ∈ N) ∧ initial-condition (`(and

                     (proper-phils state ',n)
                     (proper-forks state ',n)),

phil-prg (n))

∧ (¬ eventually-stable (`(and

                        (hungry state ',index)
                        (owns-left state ',index)),

phil-prg (n))))

→ leads-to (`(true),

            `(or
              (owns-right state ',(sub1-mod n index) ',n)
              (or
               (free state ',index)
               (or
                (eating state ',index)
                (thinking state ',index)))),

phil-prg (n))

Theorem: not-eventually-right-implies ((1 < n)

∧ (index < n) ∧ (index ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ (¬ eventually-stable (`(and

                       (hungry state ',index)
                       (owns-right state ',index ',n)),

phil-prg (n))))

→ leads-to (`(true),

           `(or
             (owns-left state ',(add1-mod n index))
             (or
              (free state ',(add1-mod n index))
              (or
               (eating state ',index)
               (thinking state ',index)))),

phil-prg (n))

Theorem: right-chain-induction (strongly-fair (phil-prg (n)) ∧ (1 < n) ∧ (i < n) ∧ (j < n) ∧ (i ∈ N) ∧ (j ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ eventually-stable (`(and

                    (hungry state ',j)
                    (owns-right state ',j ',n)),

phil-prg (n)))

→ eventually-stable (`(right-chain ',i ',j ',n state),

phil-prg (n))

Theorem: eventually-stable-right-implies-all-rights ((1 < n) ∧ (j < n) ∧ (j ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ eventually-stable (`(and

                    (hungry state ',j)
                    (owns-right state ',j ',n)),

phil-prg (n)))

→ eventually-stable (`(all-rights state ',n), phil-prg (n))

Theorem: never-all-rights (deadlock-free (phil-prg (n)) ∧ (1 < n))

→ invariant (`(not (all-rights state ',n)), phil-prg (n))

Theorem: not-eventually-owns-right ((1 < n) ∧ (j < n) ∧ (j ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ deadlock-free (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ (¬ eventually-stable (`(and

                       (hungry state ',j)
                       (owns-right state ',j ',n)),

phil-prg (n)))

Theorem: hungry-leads-to-owns-left ((1 < n) ∧ (index ∈ N) ∧ (index < n) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ strongly-fair (phil-prg (n)) ∧ deadlock-free (phil-prg (n)))

→ leads-to (`(hungry state ',index),
           `(owns-left state ',index),

phil-prg (n))

Theorem: left-chain-induction (strongly-fair (phil-prg (n)) ∧ (1 < n)

∧ (i < n) ∧ (j < n) ∧ (i ∈ N) ∧ (j ∈ N) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ eventually-stable (`(and

                    (hungry state ',j)
                    (owns-left state ',j)),

phil-prg (n)))

→ eventually-stable (`(left-chain ',i ',j ',n state),

phil-prg (n))

Theorem: eventually-stable-left-implies-all-lefts ((1 < n) ∧ (j < n) ∧ (j ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ eventually-stable (`(and

                    (hungry state ',j)
                    (owns-left state ',j)),

phil-prg (n)))

→ eventually-stable (`(all-lefts state ',n), phil-prg (n))

Theorem: never-all-lefts (deadlock-free (phil-prg (n)) ∧ (1 < n))

→ invariant (`(not (all-lefts state ',n)), phil-prg (n))

Theorem: not-eventually-owns-left ((1 < n) ∧ (j < n) ∧ (j ∈ N) ∧ strongly-fair (phil-prg (n)) ∧ deadlock-free (phil-prg (n)) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n)))

→ (¬ eventually-stable (`(and

                       (hungry state ',j)
                       (owns-left state ',j)),

phil-prg (n)))

Theorem: hungry-leads-to-owns-right ((1 < n) ∧ (index ∈ N) ∧ (index < n) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ strongly-fair (phil-prg (n)) ∧ deadlock-free (phil-prg (n)))

→ leads-to (`(hungry state ',index),
           `(owns-right state ',index ',n),

phil-prg (n))

Theorem: correctness ((1 < n) ∧ (index ∈ N) ∧ (index < n) ∧ initial-condition (`(and

                    (proper-phils state ',n)
                    (proper-forks state ',n)),

phil-prg (n))

∧ strongly-fair (phil-prg (n)) ∧ deadlock-free (phil-prg (n)))

→ leads-to (`(hungry state ',index),
           `(eating state ',index),

phil-prg (n))

Index

add1-mod, 1, 2, 4–8, 17 all-lefts, 5, 8, 17 all-lefts-implies, 5 all-lefts-inv, 9 all-lefts-unchanged, 8 all-lefts-unless-sufficient, 8 all-rights, 5, 19 all-rights-implies, 5 all-rights-inv, 9 all-rights-rec, 5, 9, 19 all-rights-rec-implies, 5 all-rights-rec-unchanged, 9 all-rights-unless-sufficient, 9

break-left-chain, 17 break-right-chain, 18 but-triple, 6, 7 but-triple-and-triple-all, 7 but-triple-preserved, 7

changed, 1, 2, 8, 9 correctness, 23

deadlock-free, 21–23

e-ensures, 11, 13 eating, 1–4 eating-e-ensures-free, 13 eating-leads-to-free, 13 eating-to, 2 eating-unless-free, 13 eventually-stable, 19–23 eventually-stable-left-implies-

all-lefts, 22 eventually-stable-right-implies

-all-rights, 20

fork, 1, 3, 4, 10 free, 1–3, 10

hungry, 1, 2, 4, 5, 16–18 hungry-both, 2 hungry-leads-to-owns-left, 21 hungry-leads-to-owns-left-implie

s, 16 hungry-leads-to-owns-right, 23 hungry-leads-to-owns-right-implie

s, 15 hungry-left, 1 hungry-left-free-e-ensures-owns

-left, 11 hungry-right, 1 hungry-right-free-e-ensures-own

s-right, 11 hungry-unless-eating, 11 hungry-unless-owns-left, 11 hungry-unless-owns-right, 11

initial-condition, 10, 13–16, 19–23 invariant, 10, 21, 22

lcc, 17

leads-to, 13–16, 19–21, 23

leads-to-expanded-left-implies, 14 leads-to-expanded-right-implies, 14 left-chain, 16, 17 left-chain-canonicalize, 17 left-chain-canonicalize-all-left

s, 17 left-chain-combine, 17 left-chain-complete, 17 left-chain-induction, 21 lessp-1, 6 lessp-1-1, 17 lessp-2, 6 lessp-2-2, 6 listp-phil-prg, 5

member-phil-prg, 3 member-ring, 3

n, 6–8

never-all-lefts, 22 never-all-rights, 21 not-eventually-left-implies, 19 not-eventually-owns-left, 22 not-eventually-owns-right, 21 not-eventually-right-implies, 19

owns-both-e-ensures-eating, 12 owns-both-leads-to-eating, 13 owns-both-unless-eating, 12 owns-left, 1, 2, 4, 5, 16 owns-left-unless-eating, 12 owns-left-unless-sufficient, 11 owns-right, 1, 2, 4, 5, 16–18 owns-right-unless-eating, 12 owns-right-unless-sufficient, 12

pfusi, 5 phil, 2, 3, 6, 7 phil-prg, 2, 3, 5, 6, 8–16, 19–23 phil-prg-invariant-1, 10 proper-fork, 10 proper-fork-invariant, 10 proper-forks, 3 proper-forks-implies, 3 proper-forks-inv, 9 proper-forks-rec, 3 proper-forks-rec-implies, 3 proper-forks-rec-inv, 9 proper-forks-rec-unless-sufficie

nt, 6 proper-phil, 3, 4, 6–8 proper-phil-invariant, 10 proper-phils, 4, 8 proper-phils-implies-proper-phi

l, 4 proper-phils-inv, 9 proper-phils-preserved, 8 proper-phils-rec, 4, 7 proper-phils-rec-implies, 4 proper-phils-rec-implies-proper

-phil, 4 proper-phils-unless-sufficient, 8 proper-triple, 6, 7 proper-triple-preserved, 6

rcc, 18 right-chain, 16–19 right-chain-canonicalize, 18 right-chain-canonicalize-all-ri

ghts, 19 right-chain-combine, 18 right-chain-complete, 19 right-chain-extend-right, 18 right-chain-induction, 20 ring, 2, 3

status, 1

strongly-fair, 15, 16, 20–23 sub1-mod, 3, 6–8, 16, 18, 19

thinking, 1–4 thinking-to, 1 true-leads-to-left-free-implies, 15 true-leads-to-right-free-implie

s, 15

unless, 9, 11–13

unless-sufficient, 6, 8, 9, 11, 12