Event: Start with the library "interpreter".

Definition: value (alist, key) = cdr (assoc (key, alist))

Definition: ct (i) = cons ('ct, i)

Definition: cf (i) = cons ('cf, i)

Definition: temp (i) = cons ('temp, i)

Definition: c-element (old, new, a, b, c) = if value (old, a) ↔ value (old, b)

then (value (new, c) ↔ value (old, a)) ∧ changed (old, new, list (c)) else changed (old, new, nil) endif

Definition: nor-gate (old, new, a, b, c) = ((value (new, c) ↔ (¬ (value (old, a) ∨ value (old, b))))

∧ changed (old, new, list (c)))

Definition: fifo-node (i) = list (list ('c-element, ct (1 + i), temp (i), ct (i)),

list ('c-element, cf (1 + i), temp (i), cf (i)), list ('nor-gate, ct (i − 1), cf (i − 1), temp (i)))

Definition: empty-node (state, i) = ((¬ value (state, ct (i))) ∧ (¬ value (state, cf (i))))

Definition: true-node (state, i) = (value (state, ct (i)) ∧ (¬ value (state, cf (i))))

Definition: false-node (state, i) = ((¬ value (state, ct (i))) ∧ value (state, cf (i)))

Definition: in-node (old, new, i) = if value (old, temp (i)) ↔ empty-node (old, i)

then if empty-node (old, i)

then changed (old, new, nil)

∨ ((true-node (new, i) ∨ false-node (new, i))

∧ (value (new, 'input) = cons (true-node (new, i),

value (old, 'input))) ∧ changed (old, new, list (ct (i), cf (i), 'input)))

else changed (old, new, nil)

∨ (empty-node (new, i)

∧ changed (old, new, list (ct (i), cf (i)))) endif

else changed (old, new, nil) endif

Definition: out-node (old, new) = ((value (new, ct (0)) ↔ value (old, ct (1)))

∧ (value (new, cf (0)) ↔ value (old, cf (1)))

∧ if empty-node (old, 0) ∧ (¬ empty-node (new, 0))

then value (new, 'output)

= cons (true-node (new, 0), value (old, 'output)) else value (new, 'output) = value (old, 'output) endif

∧ changed (old, new, list (ct (0), cf (0), 'output)))

Definition: internal-nodes (n) = if n ≃ 0 then nil

else append (fifo-node (n), internal-nodes (n − 1)) endif

Definition: external-nodes (n) = list (list ('in-node, n),

       list ('out-node),

list ('nor-gate, ct (n − 1), cf (n − 1), temp (n)))

Definition: fifo-queue (n) = append (external-nodes (n), internal-nodes (n − 1))

Theorem: member-internal-nodes (statement ∈ internal-nodes (n)) = ((statement ∈ fifo-node (cdadddr (statement)))

∧ (n ≮ cdadddr (statement)) ∧ (cdadddr (statement) ≄ 0))

Theorem: member-fifo-queue (1 < n) → ((statement ∈ fifo-queue (n))

= ((statement ∈ internal-nodes (n − 1)) ∨ (statement ∈ external-nodes (n))))

Theorem: listp-fifo-queue listp (fifo-queue (n))

Event: Disable fifo-queue.

Event: Disable *1*fifo-queue.

Definition: proper-node (state, i) = ((((¬ empty-node (state, i)) ∧ empty-node (state, i − 1))

→ value (state, temp (i)))

∧ ((empty-node (state, i) ∧ (¬ empty-node (state, i − 1)))

→ (¬ value (state, temp (i)))) ∧ (true-node (state, i)

∨ false-node (state, i) ∨ empty-node (state, i))

∧ ((¬ empty-node (state, i))

→ (empty-node (state, i − 1)

∨ if true-node (state, i) then true-node (state, i − 1) else false-node (state, i − 1) endif)))

Definition: proper-nodes (state, n) = if n ≃ 0 then t

else proper-node (state, n) ∧ proper-nodes (state, n − 1) endif

Theorem: proper-nodes-implies (proper-nodes (state, n) ∧ (n ≮ i) ∧ (i ≄ 0)) → proper-node (state, i)

Theorem: proper-nodes-preserved-general (n (old, new, statement) ∧ proper-nodes (old, n) ∧ (statement ∈ fifo-queue (n)) ∧ (n ≮ i) ∧ (1 < n)) → proper-nodes (new, i)

Theorem: proper-nodes-preserved (n (old, new, statement) ∧ (statement ∈ fifo-queue (n)) ∧ proper-nodes (old, n) ∧ (1 < n)) → proper-nodes (new, n)

Event: Disable proper-nodes-preserved-general.

Theorem: proper-nodes-unless-false (1 < n)

→ unless (`(proper-nodes state ',n), '(false), fifo-queue (n))

Theorem: proper-nodes-invariant ((1 < n) ∧ initial-condition (`(proper-nodes state ',n), fifo-queue (n))) → invariant (`(proper-nodes state ',n), fifo-queue (n))

Theorem: proper-node-invariant ((1 < n) ∧ (i ≄ 0) ∧ (n ≮ i) ∧ initial-condition (`(proper-nodes state ',n), fifo-queue (n))) → invariant (`(proper-node state ',i), fifo-queue (n))

Definition: queue-values (state, n) = if n ≃ 0 then nil

elseif (¬ empty-node (state, n)) ∧ empty-node (state, n − 1) then cons (true-node (state, n), queue-values (state, n − 1)) else queue-values (state, n − 1) endif

Theorem: empty-empty-empty ((1 < n) ∧ n (old, new, statement) ∧ (statement ∈ fifo-queue (n)) ∧ empty-node (old, 1 + i) ∧ empty-node (old, i) ∧ (i ∈ N) ∧ (i < n)) → empty-node (new, i)

Theorem: full-full-full ((1 < n) ∧ n (old, new, statement) ∧ (statement ∈ fifo-queue (n)) ∧ (¬ empty-node (old, 1 + i)) ∧ (¬ empty-node (old, i)) ∧ ((true-node (old, 1 + i) ↔ true-node (old, i))

∨ (false-node (old, 1 + i) ↔ false-node (old, i))) ∧ (i ∈ N) ∧ (i < n)) → (¬ empty-node (new, i))

Theorem: queue-empty-preserved ((1 < n) ∧ n (old, new, statement) ∧ (statement ∈ fifo-queue (n)) ∧ proper-nodes (old, n) ∧ (queue-values (old, 1 + i) = nil) ∧ (i < n)) → (queue-values (new, i) = nil)

Theorem: value-moves-forward ((1 < n) ∧ n (old, new, statement) ∧ (statement ∈ fifo-queue (n)) ∧ proper-nodes (old, n) ∧ (¬ empty-node (old, 1 + i)) ∧ empty-node (old, i) ∧ (i < n) ∧ (i ≄ 0)) → (((¬ empty-node (new, 1 + i)) ∧ empty-node (new, i))

∨ ((¬ empty-node (new, i)) ∧ empty-node (new, i − 1)))

Theorem: not-listp-queue-values-equals listp (queue-values (state, n)) = (queue-values (state, n) ≠ nil)

Theorem: full-empty-rest-unless-moves-forward ((1 < n) ∧ (i < n) ∧ (i ≄ 0)) → unless (`(and

           (proper-nodes state ',n)
           (and
            (not (empty-node state ',(add1 i)))
            (and
             (empty-node state ',i)
             (not (listp (queue-values state ',i)))))),
         `(and
           (not (empty-node state ',i))
           (and
            (empty-node state ',(sub1 i))
            (not
             (listp (queue-values state ',(sub1 i)))))),

fifo-queue (n))

Theorem: output-only-adds-boolean (1 < n)

→ unless (`(equal (value state 'output) ',k),
         `(or

(equal
(value state 'output)
(cons (true) ',k))
(equal
(value state 'output)
(cons (false) ',k))),

fifo-queue (n))

Theorem: input-only-adds-boolean (1 < n)

→ unless (`(equal (value state 'input) ',k),
`(or
(equal
(value state 'input)
(cons (true) ',k))
(equal
(value state 'input)
(cons (false) ',k))),

fifo-queue (n))

Theorem: output-never-shortens (1 < n)

→ unless (`(equal (length (value state 'output)) ',k),
`(lessp ',k (length (value state 'output))),

fifo-queue (n))

Theorem: total-sufficient-fifo-queue (1 < n) → total-sufficient (statement,

fifo-queue (n),

old,

if car (statement) = 'c-element then if value (old, cadr (statement))

↔ value (old, caddr (statement)) then update-assoc (cadddr (statement),

value (old, cadr (statement)), old)

else old endif elseif car (statement) = 'nor-gate then update-assoc (cadddr (statement),

¬ (value (old, cadr (statement))

∨ value (old,

caddr (statement))),

old)

elseif car (statement) = 'in-node then if (value (old, temp (cadr (statement)))

= empty-node (old, cadr (statement))) ∧ (¬ empty-node (old, cadr (statement)))

then update-assoc (ct (cadr (statement)), f, update-assoc (cf (cadr (statement)), f, old))

else old endif elseif car (statement) = 'out-node then update-assoc (ct (0),

value (old, ct (1)), update-assoc (cf (0),

value (old, cf (1)), if empty-node (old, 0)

∧ (¬ empty-node (old,

1))

then update-assoc ('output,

cons (true-node (old,

1),

value (old,

                                                       'output)),

old)

else old endif))

else old endif)

Theorem: total-fifo-queue (1 < n) → total (fifo-queue (n))

Theorem: output-grows-immediately (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n)) → leads-to (`(and

(not (empty-node state 1))
(and
(empty-node state 0)
(equal (length (value state 'output)) ',k))),
`(lessp ',k (length (value state 'output))),

fifo-queue (n))

Theorem: true-empty-temp-moves (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ≄ 0) ∧ (i < n))

→ leads-to (`(and

             (true-node state ',(add1 i))
             (value state (temp ',i))),
           `(not (empty-node state ',i)),

fifo-queue (n))

Theorem: false-empty-temp-moves (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ≄ 0) ∧ (i < n)) → leads-to (`(and

             (false-node state ',(add1 i))
             (value state (temp ',i))),
           `(not (empty-node state ',i)),

fifo-queue (n))

Theorem: not-empty-empty-temp-moves (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ≄ 0) ∧ (i < n)) → leads-to (`(and

             (not (empty-node state ',(add1 i)))
             (value state (temp ',i))),
           `(not (empty-node state ',i)),

fifo-queue (n))

Theorem: empty-empty-sets-temp (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ∈ N) ∧ (i < n)) → leads-to (`(and

             (empty-node state ',(add1 i))
             (empty-node state ',i)),
           `(value state (temp ',(add1 i))),

fifo-queue (n))

Theorem: full-full-unsets-temp (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ∈ N) ∧ (i < n)) → leads-to (`(and

             (not (empty-node state ',(add1 i)))
             (not (empty-node state ',i))),
           `(not (value state (temp ',(add1 i)))),

fifo-queue (n))

Theorem: empty-true-not-temp-moves (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ≄ 0) ∧ (i < n)) → leads-to (`(and

             (empty-node state ',(add1 i))
             (and
              (true-node state ',i)
              (not (value state (temp ',i))))),
           `(empty-node state ',i),

fifo-queue (n))

Theorem: empty-false-not-temp-moves (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ≄ 0) ∧ (i < n)) → leads-to (`(and

             (empty-node state ',(add1 i))
             (and
              (false-node state ',i)
              (not (value state (temp ',i))))),
           `(empty-node state ',i),

fifo-queue (n))

Theorem: empty-not-temp-moves (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i ≄ 0) ∧ (i < n)) → leads-to (`(and

             (empty-node state ',(add1 i))
             (not (value state (temp ',i)))),
           `(empty-node state ',i),

fifo-queue (n))

Theorem: empty-1-leads-to-empty-0 (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n))

→ leads-to (`(empty-node state ',1),
           `(empty-node state ',0),

fifo-queue (n))

Theorem: full-empty-empty-moves-forward (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (n ≮ (1 + (1 + i))) ∧ (i ∈ N)) → leads-to (`(and

             (not (empty-node state ',(add1 (add1 i))))
             (and
              (empty-node state ',(add1 i))
              (and
               (empty-node state ',i)
               (not
                (listp (queue-values state ',(add1 i))))))),
           `(and
             (not (empty-node state ',(add1 i)))
             (empty-node state ',i)),

fifo-queue (n))

Theorem: full-empty-full-moves-forward (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (n ≮ (1 + (1 + i))) ∧ (i ∈ N)) → leads-to (`(and

             (not (empty-node state ',(add1 (add1 i))))
             (and
              (empty-node state ',(add1 i))
              (and
               (not (empty-node state ',i))
               (not
                (listp (queue-values state ',(add1 i))))))),
           `(and
             (not (empty-node state ',(add1 i)))
             (empty-node state ',i)),

fifo-queue (n))

Theorem: full-empty-moves-forward (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (n ≮ (1 + (1 + i))) ∧ (i ∈ N))

→ leads-to (`(and

(not (empty-node state ',(add1 (add1 i))))
(and
 (empty-node state ',(add1 i))
 (not
  (listp (queue-values state ',(add1 i)))))),
`(and
(not (empty-node state ',(add1 i)))
(empty-node state ',i)),

fifo-queue (n))

Theorem: full-rest-empty-moves-forward (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i < n) ∧ (i ≄ 0)) → leads-to (`(and

(not (empty-node state ',(add1 i)))
(and
 (empty-node state ',i)
 (not (listp (queue-values state ',i))))),
`(and
(not (empty-node state ',i))
(and
 (empty-node state ',(sub1 i))
 (not
  (listp (queue-values state ',(sub1 i)))))),

fifo-queue (n))

Theorem: full-rest-empty-output-grows (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n) ∧ (i < n) ∧ (i ∈ N)) → leads-to (`(and

(not (empty-node state ',(add1 i)))
(and
 (empty-node state ',i)
 (and
  (not (listp (queue-values state ',i)))
  (equal
   (length (value state 'output))
   ',k)))),
`(lessp ',k (length (value state 'output))),

fifo-queue (n))

Definition: first-empty-subqueue (state, n) = if n ≃ 0 then 0

elseif listp (queue-values (state, n))

then first-empty-subqueue (state, n − 1)

else n endif

Theorem: first-empty-subqueue-is-empty ¬ listp (queue-values (state, first-empty-subqueue (state, n)))

Theorem: queue-not-empty-implies listp (queue-values (state, n)) → ((¬ empty-node (state, 1 + first-empty-subqueue (state, n)))

∧ empty-node (state, first-empty-subqueue (state, n)))

Theorem: not-lessp-first-empty-subqueue n ≮ first-empty-subqueue (state, n)

Theorem: lessp-first-empty-subqueue listp (queue-values (state, n)) → (first-empty-subqueue (state, n) < n)

Theorem: output-grows (initial-condition (`(proper-nodes state ',n), fifo-queue (n)) ∧ (1 < n)) → leads-to (`(and

              (listp (queue-values state n))
              (equal (length (value state 'output)) ',k)),
            `(lessp ',k (length (value state 'output))),

fifo-queue (n))

Theorem: in-node-leaves-rest-of-queue-unchanged (n (old, new, list ('in-node, n)) ∧ (1 < n) ∧ (i < n) ∧ (i ∈ N)) → ((value (new, 'output) = value (old, 'output))

∧ (queue-values (new, i) = queue-values (old, i)))

Theorem: in-node-preserves-values (n (old, new, list ('in-node, n)) ∧ proper-node (old, n) ∧ (value (old, 'input)

= append (queue-values (old, n), value (old, 'output))) ∧ (1 < n)) → (value (new, 'input)

= append (queue-values (new, n), value (new, 'output)))

Theorem: out-node-preserves-queue-values (n (old, new, '(out-node)) ∧ (1 < n) ∧ (n ≮ i) ∧ (i ≄ 0)) → ((value (new, 'input) = value (old, 'input))

∧ (append (queue-values (new, i), value (new, 'output)) = append (queue-values (old, i), value (old, 'output))))

Theorem: external-nor-gates-preserves-values (n (old, new, list ('nor-gate, ct (n − 1), cf (n − 1), temp (n))) ∧ (1 < n) ∧ (n ≮ i) ∧ (i ∈ N)) → ((value (new, 'input) = value (old, 'input))

∧ (value (new, 'output) = value (old, 'output)) ∧ (queue-values (new, i) = queue-values (old, i)))

Theorem: internal-nodes-preserves-rest-of-queue (n (old, new, statement) ∧ (statement ∈ fifo-node (i)) ∧ (j ∈ N) ∧ (j < i)) → (queue-values (new, j ) = queue-values (old, j ))

Theorem: internal-nodes-preserve-values (n (old, new, statement) ∧ (statement ∈ fifo-node (i)) ∧ proper-node (old, 1 + i) ∧ proper-node (old, i) ∧ (i ≄ 0) ∧ (i < j )) → ((value (new, 'input) = value (old, 'input))

∧ (value (new, 'output) = value (old, 'output)) ∧ (queue-values (new, j ) = queue-values (old, j )))

Theorem: values-preserved (n (old, new, statement) ∧ proper-nodes (old, n) ∧ (1 < n) ∧ (value (old, 'input)

= append (queue-values (old, n), value (old, 'output))) ∧ (statement ∈ fifo-queue (n))) → (value (new, 'input)

= append (queue-values (new, n), value (new, 'output)))

Theorem: values-invariant (1 < n) → unless (`(and

(proper-nodes state ',n)
(equal
 (value state 'input)
 (append
  (queue-values state ',n)
  (value state 'output)))),
'(false),

fifo-queue (n))

Theorem: queue-values-invariant (initial-condition (`(and

     (proper-nodes state ',n)
     (equal
      (value state 'input)
      (append
       (queue-values state ',n)
       (value state 'output)))),

fifo-queue (n))

∧ (1 < n)) → invariant (`(equal

  (value state 'input)
  (append
   (queue-values state ',n)
   (value state 'output))),

fifo-queue (n))

Index

c-element, 1 cf, 1, 2, 7, 13 changed, 1, 2 ct, 1, 2, 7, 13

empty-1-leads-to-empty-0, 9 empty-empty-empty, 4 empty-empty-sets-temp, 8 empty-false-not-temp-moves, 9 empty-node, 1–5, 7, 12 empty-not-temp-moves, 9 empty-true-not-temp-moves, 9 external-nodes, 2 external-nor-gates-preserves-va

lues, 13

false-empty-temp-moves, 8 false-node, 1, 3, 4 fifo-node, 1, 2, 13 fifo-queue, 2–14 first-empty-subqueue, 12 first-empty-subqueue-is-empty, 12 full-empty-empty-moves-forward, 10 full-empty-full-moves-forward, 10 full-empty-moves-forward, 10 full-empty-rest-unless-moves-fo

rward, 5 full-full-full, 4 full-full-unsets-temp, 8 full-rest-empty-moves-forward, 11 full-rest-empty-output-grows, 11

in-node, 1 in-node-leaves-rest-of-queue-un

changed, 12 in-node-preserves-values, 12 initial-condition, 4, 7–12, 14 input-only-adds-boolean, 6 internal-nodes, 2 internal-nodes-preserve-values, 13 internal-nodes-preserves-rest-o

f-queue, 13 invariant, 4, 14

leads-to, 7–12

lessp-first-empty-subqueue, 12 listp-fifo-queue, 2

member-fifo-queue, 2 member-internal-nodes, 2

n, 3–5, 12, 13 nor-gate, 1 not-empty-empty-temp-moves, 8 not-lessp-first-empty-subqueue, 12 not-listp-queue-values-equals, 5

out-node, 2

out-node-preserves-queue-values, 13 output-grows, 12 output-grows-immediately, 7 output-never-shortens, 6 output-only-adds-boolean, 5

proper-node, 3, 12, 13 proper-node-invariant, 4 proper-nodes, 3, 5, 13 proper-nodes-implies, 3 proper-nodes-invariant, 4 proper-nodes-preserved, 3 proper-nodes-preserved-general, 3 proper-nodes-unless-false, 4

queue-empty-preserved, 5 queue-not-empty-implies, 12 queue-values, 4, 5, 12, 13 queue-values-invariant, 14

temp, 1–3, 7, 13

total, 7

total-fifo-queue, 7 total-sufficient, 7 total-sufficient-fifo-queue, 6 true-empty-temp-moves, 7 true-node, 1–4, 7

unless, 4–6, 14 update-assoc, 6, 7

value, 1–3, 6, 7, 12, 13 value-moves-forward, 5 values-invariant, 13 values-preserved, 13