Event: Start with the library "c-predefined3".

Theorem: arrays-have-non-zerop-lengths (array-identifierp (x, alist) ∧ mg-alistp (alist)) → (array-length (cadr (assoc (x, alist))) ≄ 0)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                    EXACT-TIME LEMMA MG-INDEX-ARRAY                         ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Enable map-down-values-preserves-length.

Theorem: lessp-plus-transitive (((x + (w − 1)) < z) ∧ (y < w)) → (((x + y) < z) = t)

Event: Disable lessp-plus-transitive.

Theorem: idifference-lessp2 ((x ∈ N) ∧ (x < y)) → (((idifference (y, x) = 0) = f) ∧ (idifference (y, x) ∈ N))

Theorem: zerop-integerp-trichotomy (integerp (x) ∧ (x ∉ N)) → negativep (x)

Event: Disable zerop-integerp-trichotomy.

Theorem: p-object-type-int (p-objectp-type ('int, tag ('int, x), state) = small-integerp (x, p-word-size (state))) ∧ (p-objectp-type ('int, list ('int, x), state)

= small-integerp (x, p-word-size (state)))

Theorem: simple-identifierp-options (int-identifierp (x, alist) ∨ boolean-identifierp (x, alist) ∨ character-identifierp (x, alist)) → simple-identifierp (x, alist)

Theorem: small-integerp-difference (small-integerp (x, n)

∧ small-integerp (y, n) ∧ (x ≄ 0) ∧ (¬ negativep (y))) → small-integerp (idifference (x, y), n)

Theorem: limits-for-small-integerp ((x < maxint) ∧ (x ≄ 0)) → small-integerp (x, 32)

Theorem: simple-typed-identifier-simple-identifierp simple-typed-identifierp (x, type, alist) → simple-identifierp (x, alist)

Theorem: mg-var-ok-array-index-ok3 (mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ mg-alistp (mg-vars) ∧ array-identifierp (x, mg-vars)) → (((untag (value (x, bindings))

+ (array-length (cadr (assoc (x, mg-vars))) − 1))

< length (temp-stk))

= t)

Theorem: idifference-lessp ((¬ negativep (y)) ∧ (idifference (x, y) ≄ 0)) → ((y < x) = t)

Theorem: nat-p-objectp-reduction p-objectp-type ('nat, tag ('nat, x), state) = small-naturalp (x, p-word-size (state))

Theorem: array-index-small-naturalp ((temp-stk-size < mg-max-temp-stk-size) ∧ ((a + (array-size − 1)) < temp-stk-size) ∧ (index < array-size)) → small-naturalp (a + index, 32)

Theorem: mg-index-array-args-have-simple-mg-type-refps

((car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (simple-typed-identifierp (car (call-actuals (stmt)),

array-elemtype (cadr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

mg-alist (mg-state)) ∧ array-identifierp (cadr (call-actuals (stmt)), mg-alist (mg-state)) ∧ int-identifierp (caddr (call-actuals (stmt)), mg-alist (mg-state))

∧ (cadddr (call-actuals (stmt))

= array-length (cadr (assoc (cadr (call-actuals (stmt)), mg-alist (mg-state))))))

Theorem: mg-index-array-args-definedp

((car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (definedp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ definedp (cadr (call-actuals (stmt)), mg-alist (mg-state)) ∧ definedp (caddr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-index-array-arg4-small-integerp

((car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → small-integerp (cadddr (call-actuals (stmt)), 32)

Theorem: not-zerop-mg-index-array-arg4

((car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → ((cadddr (call-actuals (stmt)) ∈ N)

∧ (cadddr (call-actuals (stmt)) ≠ 0))

Theorem: mg-index-array-steps-1-4 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)), code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p-step (p-step (p-step (p-step (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc,

cons (subr,

length (code (cinfo)))),

t-cond-list)))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 4)), ctrl-stk, push (tag ('int, cadddr (call-actuals (stmt))),

push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-step-5 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 4)),

ctrl-stk,

push (tag ('int, cadddr (call-actuals (stmt))),

push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))
    = p-state (tag ('pc, '(mg-index-array . 0)),

push (p-frame (cons (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('i, value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                         cons (cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                              '((temp-i nat 0)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-steps-6-8 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p-step (p-step (p-step (p-state (tag ('pc, '(mg-index-array . 0)), push (p-frame (cons (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                          cons (cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                               '((temp-i
                                  nat

0)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))))
= p-state (tag ('pc, '(mg-index-array . 3)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

 cons ('array-size,

tag ('int, cadddr (call-actuals (stmt)))),

                              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-steps-9-12-neg-index ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

→ (p-step (p-step (p-step (p-step (p-state (tag ('pc,

    '(mg-index-array . 3)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size, 'run)))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)), ctrl-stk, map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c, '(nat 1))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-steps-9-11-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))))

→ (p-step (p-step (p-step (p-state (tag ('pc, '(mg-index-array . 3)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                             cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                             cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))))
= p-state (tag ('pc, '(mg-index-array . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo))

+ 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (tag ('int, cadddr (call-actuals (stmt))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)),

temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; This is the (sub-int) instruction
;; The proof of this could be cleaned up substantially

Theorem: mg-index-array-step-12-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a, value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (tag ('int, cadddr (call-actuals (stmt))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 7)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc, cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('int,

idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-step-13-index-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)), untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≃ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 7)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('int,

idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 16)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i, value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-steps-14-16-index-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≃ 0))

→ (p-step (p-step (p-step (p-state (tag ('pc, '(mg-index-array . 16)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)), ctrl-stk, map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk), translate-proc-list (proc-list), list (list ('c-c, '(nat 1))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-step-13-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 7)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i, value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('int,

idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 8)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-steps-14-15-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-step (p-state (tag ('pc, '(mg-index-array . 8)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)), bindings (top (ctrl-stk)))), cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run)))
= p-state (tag ('pc, '(mg-index-array . 10)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

       cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

       cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)), mg-alist (mg-state)))))), tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-step-16-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 10)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 11)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)), bindings (top (ctrl-stk)))), cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: non-negative-integerp-small-naturalp (integerp (x) ∧ (¬ negativep (x)) ∧ small-integerp (y, n) ∧ (y ∈ N) ∧ (idifference (y, x) ≄ 0)) → small-naturalp (x, n)

Theorem: mg-index-array-step-17-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 11)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)), mg-alist (mg-state)))))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 12)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-index-lessp-temp-stk-length

((car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ signatures-match (mg-alist (mg-state), name-alist) ∧ (¬ negativep (untag (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (((untag (value (cadr (call-actuals (stmt)), bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))

< length (temp-stk))

= t)

Theorem: mg-index-array-step-18-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)),

temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 12)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 13)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-index-array-step-19-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 13)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 14)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-step-20-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, '(mg-index-array . 14)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a, value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-index-array . 15)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), rput (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-steps-21-22-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list)

∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-step (p-state (tag ('pc, '(mg-index-array . 15)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('a,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                       cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                       cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), rput (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

         'run)))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)), ctrl-stk, rput (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-index-array-push-cc ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)),

ctrl-stk, temp-stk, translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 6)), ctrl-stk, push (cc-value, temp-stk), translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-sub1-cc ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist)

∧ normal (mg-state) ∧ (cc-value ∈ list ('(nat 1), '(nat 2)))) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 6)),

ctrl-stk,

push (cc-value, temp-stk), translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 7)), ctrl-stk, push (tag ('nat, untag (cc-value) − 1), temp-stk), translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-index-array-last-step-error-case ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)

∧ (negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))))

∨ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≃ 0)))

→ (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 7)), ctrl-stk, push (tag ('nat, untag ('(nat 1)) − 1),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

'((c-c (nat 1))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)), ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: simple-typed-identifier-type-equivalence simple-typed-identifierp (b, type, alist) → ((cadr (assoc (b, alist)) = type) = t)

Theorem: mg-index-array-step-25-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state))

∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 7)), ctrl-stk, push (tag ('nat,

untag (mg-cond-to-p-nat (cc (mg-state),

t-cond-list)) − 1),

rput (rget (untag (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-index-array-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt, proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-index-array) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;              EXACT-TIME-LEMMA MG-ARRAY-ELEMENT-ASSIGNMENT                 ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; stmt looks like '(mg-predefined-proc-call mg-array-element-assignment (A i x size))

Theorem: mg-array-element-assignment-args-have-simple-mg-type-refps

((car (stmt) = 'predefined-proc-call-mg)

∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (array-identifierp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ int-identifierp (cadr (call-actuals (stmt)), mg-alist (mg-state)) ∧ simple-typed-identifierp (caddr (call-actuals (stmt)),

array-elemtype (cadr (assoc (car (call-actuals (stmt)),

mg-alist (mg-state)))),

mg-alist (mg-state))

∧ (cadddr (call-actuals (stmt))

= array-length (cadr (assoc (car (call-actuals (stmt)), mg-alist (mg-state))))))

Theorem: mg-array-element-assignment-arg3-simple

((car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → simple-identifierp (caddr (call-actuals (stmt)), mg-alist (mg-state))

Theorem: mg-array-element-assignment-args-definedp

((car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (definedp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ definedp (cadr (call-actuals (stmt)), mg-alist (mg-state)) ∧ definedp (caddr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-array-element-assignment-arg4-small-integerp

((car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → small-integerp (cadddr (call-actuals (stmt)), 32)

Theorem: not-zerop-mg-array-element-assignment-arg4

((car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list)

∧ signatures-match (mg-alist (mg-state), name-alist)) → ((cadddr (call-actuals (stmt)) ∈ N)

∧ (cadddr (call-actuals (stmt)) ≠ 0))

Theorem: mg-array-element-assignment-steps-1-4 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p-step (p-step (p-step (p-step (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc,

cons (subr,

length (code (cinfo)))),

t-cond-list)))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 4)), ctrl-stk, push (tag ('int, cadddr (call-actuals (stmt))),

push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-step-5 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 4)),

ctrl-stk,

push (tag ('int, cadddr (call-actuals (stmt))),

push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 0)),

push (p-frame (cons (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                          cons (cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                               '((temp-i nat 0)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-steps-6-8 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p-step (p-step (p-step (p-state (tag ('pc,

                                 '(mg-array-element-assignment
                                   . 0)),

push (p-frame (cons (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons (cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                                        cons (cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                                            '((temp-i
                                                               nat

0)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk), translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

               'run))))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 3)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-steps-9-12-neg-index ((n ≄ 0)

∧ (¬ resources-inadequatep (stmt, proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

→ (p-step (p-step (p-step (p-step (p-state (tag ('pc,

                                       '(mg-array-element-assignment
                                         . 3)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                                   cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                                   cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                                   cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo))

+ 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size, 'run)))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)), ctrl-stk, map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c, '(nat 1))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-steps-9-11-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state))

∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))))

→ (p-step (p-step (p-step (p-state (tag ('pc,

    '(mg-array-element-assignment
      . 3)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 6)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (tag ('int, cadddr (call-actuals (stmt))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-step-12-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))))

→ (p-step (p-state (tag ('pc,

                     '(mg-array-element-assignment . 6)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (tag ('int, cadddr (call-actuals (stmt))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 7)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('int,

idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-step-13-index-error ((n ≄ 0)

∧ (¬ resources-inadequatep (stmt, proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≃ 0))

→ (p-step (p-state (tag ('pc,

                     '(mg-array-element-assignment . 7)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc, cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('int,

idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-array-element-assignment . 16)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-steps-14-16-index-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≃ 0))

→ (p-step (p-step (p-step (p-state (tag ('pc,

                                 '(mg-array-element-assignment
                                   . 16)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                             cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                               cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                               cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

               'run))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)), ctrl-stk, map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c, '(nat 1))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
;; Need 13-15 and 16-17 no-error lemmas

Theorem: mg-array-element-assignment-step-13-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk), p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc,

                     '(mg-array-element-assignment . 7)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('int, idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 8)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-step-14-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc,

                     '(mg-array-element-assignment . 8)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-array-element-assignment . 9)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (value ('value,

list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

           cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                            cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                            cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-step-15-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc,

'(mg-array-element-assignment . 9)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo))

+ 5))),

ctrl-stk), push (value ('value,

list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 10)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-steps-16-17-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-step (p-state (tag ('pc,

                           '(mg-array-element-assignment
                             . 10)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                       cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                       cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                       cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc, cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run)))

= p-state (tag ('pc,

'(mg-array-element-assignment . 12)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

       cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

       cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

       cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-step-18-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc,

                     '(mg-array-element-assignment . 12)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i, value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-array-element-assignment . 13)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

              cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                              cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-step-19-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist)

∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc,

                     '(mg-array-element-assignment . 13)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                 cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                 cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))

= p-state (tag ('pc,

    '(mg-array-element-assignment . 14)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-index-lessp-temp-stk-length

((car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ signatures-match (mg-alist (mg-state), name-alist) ∧ (¬ negativep (untag (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (((untag (value (car (call-actuals (stmt)), bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))

< length (temp-stk))

= t)

Theorem: mg-array-element-assignment-step-20-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc,

    '(mg-array-element-assignment . 14)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), push (tag ('nat,

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

push (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-array-element-assignment . 15)),

push (p-frame (list (cons ('a, value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), rput (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-steps-21-22-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-step (p-state (tag ('pc,

                           '(mg-array-element-assignment
                             . 15)),

push (p-frame (list (cons ('a,

value (car (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

cons ('i,

value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                       cons ('value,

value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk)))),

                                       cons ('array-size,

tag ('int,

cadddr (call-actuals (stmt)))),

                                       cons ('temp-i,

mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 5))),

ctrl-stk), rput (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))), untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

         'run)))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)), ctrl-stk, rput (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-push-cc ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 5)),

ctrl-stk, temp-stk, translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 6)), ctrl-stk, push (cc-value, temp-stk), translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-sub1-cc ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk)

∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state) ∧ (cc-value ∈ list ('(nat 1), '(nat 2)))) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 6)),

ctrl-stk,

push (cc-value, temp-stk), translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 7)), ctrl-stk, push (tag ('nat, untag (cc-value) − 1), temp-stk), translate-proc-list (proc-list), list (list ('c-c, cc-value)), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-array-element-assignment-last-step-error-case ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))))

∨ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≃ 0)))

→ (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 7)), ctrl-stk, push (tag ('nat, untag ('(nat 1)) − 1),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

'((c-c (nat 1))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt,

proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: put-preserves-ok-mg-array-value (ok-mg-array-value (z, type) ∧ simple-typed-literalp (x, array-elemtype (type)) ∧ (i < length (z))) → ok-mg-array-value (put (x, i, z), type)

Theorem: arrays-have-ok-values (mg-alistp (mg-alist) ∧ array-identifierp (a, mg-alist)) → ok-mg-array-value (caddr (assoc (a, mg-alist)), cadr (assoc (a, mg-alist)))

Definition: put-deposit-array-value-induction-hint (lst, nat, temp-stk, index) = if index ≃ 0 then t

else put-deposit-array-value-induction-hint (cdr (lst), add1-nat (nat), deposit-temp (mg-to-p-simple-literal (car (lst)),

nat,

temp-stk),

index − 1) endif

;; I think the splits over whether (nlistp (cdr lst)) are not necessary

Theorem: put-deposit-array-value-rewrite ((index < length (lst)) ∧ ((untag (nat) + (length (lst) − 1)) < length (temp-stk)) ∧ (untag (nat) ∈ N)) → (deposit-array-value (put (value, index, lst), nat, temp-stk)

= rput (mg-to-p-simple-literal (value), untag (nat) + index, deposit-array-value (lst, nat, temp-stk)))

Event: Disable put-deposit-array-value-rewrite.

Theorem: mg-array-element-assignment-deposit-array-value-rewrite (all-cars-unique (mg-vars) ∧ mg-alistp (mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ no-p-aliasing (bindings, mg-vars) ∧ (index < array-length (cadr (assoc (a, mg-vars)))) ∧ array-identifierp (a, mg-vars)) → (deposit-array-value (put (value, index, caddr (assoc (a, mg-vars))),

cdr (assoc (a, bindings)),

map-down-values (mg-vars, bindings, temp-stk))

= rput (mg-to-p-simple-literal (value), untag (cdr (assoc (a, bindings))) + index, map-down-values (mg-vars, bindings, temp-stk)))

Event: Disable mg-array-element-assignment-deposit-array-value-rewrite.

Theorem: mg-array-element-assignment-step-25-no-error ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)), code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state) ∧ (¬ negativep (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))))

∧ (idifference (cadddr (call-actuals (stmt)),

untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))) ≄ 0))

→ (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 7)), ctrl-stk, push (tag ('nat,

untag (mg-cond-to-p-nat (cc (mg-state),

t-cond-list)) − 1),

rput (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))),

untag (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))))

+ untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-array-element-assignment-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt, proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-array-element-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ normal (mg-state)) → (p (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                    EXACT-TIME-LEMMA for PREDEFINED's                      ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: predefined-proc-call-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'predefined-proc-call-mg)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 ) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ cond-subsetp (r-cond-list, t-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ plistp (temp-stk) ∧ listp (ctrl-stk) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state) ∧ all-cars-unique (mg-alist (mg-state)) ∧ (¬ resource-errorp (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))))

→ (p (map-down (mg-state, proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Event: Make the library "c-predefined4".

Index

add1-nat, 83 all-cars-unique, 4–6, 8, 10, 12, 14,

16, 18, 20, 22, 25, 27, 30, 32, 35, 37, 38, 40, 43, 46, 47, 49, 51, 52, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78, 80, 81, 84, 85, 87, 89

array-elemtype, 2, 45, 83 array-identifierp, 1, 2, 45, 83, 84 array-index-small-naturalp, 2 array-length, 1–3, 45, 84 arrays-have-non-zerop-lengths, 1 arrays-have-ok-values, 83

bindings, 4–36, 38–44, 46–79, 81–

83, 85–90 boolean-identifierp, 1

call-actuals, 2–36, 39, 41, 45–79, 82,

85 call-name, 2, 3, 5, 6, 8, 10, 12, 14,

16, 18, 20, 22, 25, 27, 30, 32, 34, 36–38, 40, 43, 45– 47, 49, 51, 52, 54, 57, 59, 61, 63, 65, 68, 70, 72, 75, 77, 79–81, 84, 87

cc, 4–9, 11–17, 19–24, 26, 28, 29, 31–34, 36, 39–42, 44, 47, 48, 50, 52–54, 56, 58, 60, 62, 64, 65, 67, 69–74, 76, 77, 79, 82, 83, 85, 86, 88, 90

character-identifierp, 1 clock, 43, 87, 89 code, 3–44, 46–90 cond-subsetp, 89

definedp, 3, 45 deposit-array-value, 84 deposit-temp, 83

fetch-label, 39, 42, 44, 82, 86, 88, 90 find-label, 39, 42, 44, 83, 86, 88, 90

idifference, 1, 2, 14, 15, 17–20, 23– 25, 27, 28, 30, 32, 35, 39, 41, 56–59, 61–63, 66, 68, 70, 73, 75, 76, 78, 82, 85

idifference-lessp, 2 idifference-lessp2, 1 int-identifierp, 1, 2, 45 integerp, 1, 24

label-alist, 39, 42, 44, 82, 86, 88, 90 length, 2–44, 46–90 lessp-plus-transitive, 1 limits-for-small-integerp, 2

map-down, 4, 43, 46, 87, 89 map-down-values, 4–9, 11–17, 19–

24, 26, 28, 29, 31–36, 39– 42, 44, 47–50, 52–56, 58, 60, 62, 64–67, 69–74, 76, 77, 79, 82–86, 88, 90

maxint, 2 mg-alist, 2–83, 85–90 mg-alistp, 1, 2, 83, 84 mg-array-element-assignment-arg

3-simple, 45

4-small-integerp, 45

s-definedp, 45

s-have-simple-mg-type-refps, 44 mg-array-element-assignment-dep

osit-array-value-rewrite, 84 mg-array-element-assignment-exa

ct-time-lemma, 86 mg-array-element-assignment-inde

x-lessp-temp-stk-length, 75 mg-array-element-assignment-last

-step-error-case, 81 mg-array-element-assignment-pus

h-cc, 79 mg-array-element-assignment-step -12-no-error, 54 -13-index-error, 56 -13-no-error, 60 -14-no-error, 63 -15-no-error, 65 -18-no-error, 70 -19-no-error, 72 -20-no-error, 75 -25-no-error, 84 -5, 47 s-1-4, 46 s-14-16-index-error, 59 s-16-17-no-error, 67 s-21-22-no-error, 77 s-6-8, 48 s-9-11-no-error, 52 s-9-12-neg-index, 50

mg-array-element-assignment-sub

1-cc, 80 mg-cond-to-p-nat, 4–9, 11–17, 19–

24, 26, 28, 29, 31–34, 36, 40–42, 44, 47, 48, 50, 52– 54, 56, 58, 60, 62, 64, 65, 67, 69–74, 76, 77, 79, 83, 85, 86, 88, 90

mg-index-array-arg4-small-intege

rp, 3 mg-index-array-args-definedp, 3 mg-index-array-args-have-simple

-mg-type-refps, 2 mg-index-array-exact-time-lemma, 42 mg-index-array-index-lessp-temp

-stk-length, 27 mg-index-array-last-step-error-

case, 38 mg-index-array-push-cc, 36 mg-index-array-step-12-no-error, 12 mg-index-array-step-13-index-er

ror, 14 mg-index-array-step-13-no-error, 18 mg-index-array-step-16-no-error, 22 mg-index-array-step-17-no-error, 24 mg-index-array-step-18-no-error, 27 mg-index-array-step-19-no-error, 29 mg-index-array-step-20-no-error, 32 mg-index-array-step-25-no-error, 40 mg-index-array-step-5, 4 mg-index-array-steps-1-4, 3 mg-index-array-steps-14-15-no-e

rror, 20 mg-index-array-steps-14-16-inde

x-error, 16 mg-index-array-steps-21-22-no-e

rror, 34 mg-index-array-steps-6-8, 6 mg-index-array-steps-9-11-no-er

ror, 10 mg-index-array-steps-9-12-neg-i

ndex, 8 mg-index-array-sub1-cc, 37 mg-max-ctrl-stk-size, 4–9, 11–24, 26,

28, 29, 31–34, 36–42, 44, 47, 48, 50, 52–54, 56, 58– 60, 62, 64, 65, 67, 69–72, 74, 76, 77, 79–83, 85, 86, 88, 90

mg-max-temp-stk-size, 2, 4–24, 26– 29, 31–34, 36–42, 44, 47, 48, 50, 52–54, 56, 58–60, 62, 64, 65, 67, 69–72, 74, 76, 77, 79–83, 85, 86, 88, 90

mg-meaning-r, 39–44, 82, 83, 85–90 mg-to-p-simple-literal, 8–36, 39, 41, 50–79, 82–85 mg-var-ok-array-index-ok3, 2 mg-vars-list-ok-in-p-state, 2, 4–6, 8,

10, 12, 14, 16, 18, 20, 22, 25, 27, 28, 30, 32, 35, 38, 41, 43, 46, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 68, 70, 73, 75, 78, 81, 84, 85, 87, 89

mg-word-size, 4–24, 26–29, 31–34, 36–42, 44, 47, 48, 50, 52– 54, 56, 58–60, 62, 64, 65, 67, 69–72, 74, 76, 77, 79– 83, 85, 86, 88, 90 nat-p-objectp-reduction, 2 no-p-aliasing, 4–6, 8, 10, 12, 14, 17,

18, 20, 22, 25, 28, 30, 32, 35, 38, 41, 43, 46, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 68, 70, 73, 75, 78, 82, 84, 85, 87, 89

non-negative-integerp-small-nat

uralp, 24 normal, 4–6, 8, 10, 12, 14, 17, 18,

20, 22, 25, 28, 30, 32, 35, 37–39, 41, 43, 46, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 68, 70, 73, 75, 78, 80– 82, 85, 87, 89

not-zerop-mg-array-element-assi

gnment-arg4, 45 not-zerop-mg-index-array-arg4, 3

ok-mg-array-value, 83 ok-mg-def-plistp, 3, 5, 6, 8, 10, 12,

14, 16, 18, 20, 22, 25, 27, 30, 32, 34, 36–38, 40, 43, 46, 47, 49, 51, 52, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78–81, 84, 87, 89

ok-mg-statement, 2, 3, 5, 6, 8, 10, 12, 14, 16, 18, 20, 22, 25, 27, 30, 32, 34, 36–38, 40, 43, 45–47, 49, 51, 52, 54, 57, 59, 61, 63, 65, 68, 70, 72, 75, 77, 79–81, 84, 87, 89

ok-mg-statep, 2, 3, 5, 6, 8, 10, 12, 14, 16, 18, 20, 22, 25, 27, 30, 32, 34, 36–38, 40, 43, 45–47, 49, 51, 52, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78, 80, 81, 84, 87, 89

ok-translation-parameters, 89

p, 43, 87, 89 p-ctrl-stk-size, 3, 4, 6, 8, 10, 12, 14,

16, 18, 20, 22, 24, 27, 29, 32, 34, 36–44, 46, 47, 49, 51, 52, 54, 57, 59, 60, 63, 65, 68, 70, 72, 75, 77, 79– 90

p-frame, 6–9, 11, 13–17, 19, 21–26, 28–31, 33–35, 48–50, 52– 56, 58, 60–62, 64, 66, 67, 69, 71–74, 76–78

p-object-type-int, 1 p-objectp-type, 1, 2 p-state, 4–24, 26–29, 31–34, 36–42,

44, 47, 48, 50, 52–54, 56, 58–60, 62, 64, 65, 67, 69– 72, 74, 76, 77, 79–83, 85, 86, 88, 90

p-step, 4, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 26, 28, 31, 33, 36– 39, 41, 46, 48, 50, 52, 53, 56, 58, 60, 62, 64, 67, 69, 71, 74, 76, 79–82, 85

p-word-size, 1, 2

plistp, 89

predefined-proc-call-exact-time

-lemma, 88 push, 4–9, 11–17, 19–26, 28–35, 37–

39, 41, 47–50, 52–56, 58, 60–62, 64–67, 69–74, 76– 78, 80–82, 85

put, 83, 84

put-deposit-array-value-inducti

on-hint, 83 put-deposit-array-value-rewrite, 84 put-preserves-ok-mg-array-value, 83

resource-errorp, 89

resources-inadequatep, 3, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 27, 29, 32, 34, 36–38, 40, 43, 46, 47, 49, 51, 52, 54, 57, 59, 60, 63, 65, 68, 70, 72, 75, 77, 79–81, 84, 87, 89 rget, 29, 31, 33–36, 41 rput, 34, 36, 41, 77, 79, 84, 85 signatures-match, 2–6, 8, 10, 12, 14,

16, 18, 20, 22, 25, 27, 30, 32, 35, 37, 38, 41, 43, 45– 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78, 80, 81, 85, 87, 89

simple-identifierp, 1, 2, 45 simple-identifierp-options, 1 simple-typed-identifier-simple-i

dentifierp, 2 simple-typed-identifier-type-eq

uivalence, 40 simple-typed-identifierp, 2, 40, 45 simple-typed-literalp, 83 small-integerp, 1–3, 24, 45 small-integerp-difference, 1 small-naturalp, 2, 24

tag, 1, 2, 4–26, 28–39, 41–44, 46–74,

76–83, 85–90 top, 4–36, 38–44, 46–79, 81–83, 85–

90 translate, 3, 5, 6, 8, 10, 12, 14, 16,

18, 20, 22, 25, 27, 30, 32, 34, 37–40, 42–44, 46, 47, 49, 51, 52, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78, 80–84, 86–90

translate-def-body, 3, 5, 6, 8, 10, 12, 14, 16, 18, 20, 22, 25, 27, 30, 32, 34, 36–38, 40, 43, 46, 47, 49, 51, 52, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78, 80, 81, 84, 87, 89

translate-proc-list, 4–9, 11–24, 26, 28, 29, 31–34, 36–42, 44, 47, 48, 50, 52–56, 58, 60, 62, 64–67, 69–74, 76, 77, 79–83, 85, 86, 88, 90

untag, 2, 9, 10, 12, 14, 15, 17–20, 22–36, 38, 39, 41, 51, 53, 55–59, 61–63, 65, 66, 68, 70, 72–79, 81, 82, 84, 85 user-defined-procp, 4–6, 8, 10, 12,

14, 16, 18, 20, 22, 25, 27, 30, 32, 34, 37, 38, 40, 43, 46, 47, 49, 51, 52, 55, 57, 59, 61, 63, 65, 68, 70, 72, 75, 78, 80, 81, 85, 87, 89

value, 2, 4–7, 9–13, 15–36, 41, 46– 51, 53–79, 85

zerop-integerp-trichotomy, 1